How to use `exists.elim` in Lean?

Question

This proof is a tactics-based version of the one in "Logic and Proof" by Avigad et al.

import data.nat.prime
open nat

theorem sqrt_two_irrational_V2 {a b : ℕ} (co : gcd a b = 1) : a^2 ≠ 2 * b^2 :=
begin
    intro h,
    have h1 : 2 ∣ a^2, by simp [h],
    have h2 : 2 ∣ a, from prime.dvd_of_dvd_pow prime_two h1,
    cases h2 with c aeq,
    have h3 : 2 * (2 * c^2) = 2 * b^2,
        by simp [eq.symm h, aeq];
            simp [nat.pow_succ, mul_comm, mul_assoc, mul_left_comm],
    have h4 : 2 * c^2 = b^2,
        from eq_of_mul_eq_mul_left dec_trivial h3,
    have h5 : 2 ∣ b^2,
        by simp [eq.symm h4],
    have hb : 2 ∣ b,
        from prime.dvd_of_dvd_pow prime_two h5,
    have h6 : 2 ∣ gcd a b, from dvd_gcd (exists.intro c aeq) hb,
    have habs : 2 ∣ (1:ℕ), by simp * at *,
    exact absurd habs dec_trivial, done
end

which works. I'm trying to work my way backwards in the Lean manual, because tactics mode is much more intuitive for me. When attempting the same without tactics, I have trouble with the exists.elim part, as all the examples in the Lean manual show how to use it only to get the final goal not an intermediary step. Can anyone help me fix this code? Could let or match also be used for the same purpose?

theorem sqrt_two_irrational_V1 {a b : ℕ} (co : gcd a b = 1) : a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
    by simp [h],
have ha : 2 ∣ a,
    from prime.dvd_of_dvd_pow prime_two this,
-- this line below is wrong
exists.elim ha (assume c : ℕ, assume aeq : a = 2 * c), 
-- also tried "let" and "match"
--let ⟨c, aeq⟩ := ha,
-- match ha with ⟨(c : ℕ), (aeq : a = 2 * c)⟩,
have 2 * (2 * c^2) = 2 * b^2,
    by simp [eq.symm h, aeq]; 
       simp [nat.pow_succ, mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
    from eq_of_mul_eq_mul_left dec_trivial this,
have 2 ∣ b^2, 
    by simp [eq.symm this],
have hb : 2 ∣ b,
    from prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
    from dvd_gcd ha hb,
have habs : 2 ∣ (1:ℕ), 
    by simp * at *,
show false, from absurd habs dec_trivial

Answer 1

I moved one bracket to fix the proof. Usually when you use exists.elim the entire rest of the proof should be inside the brackets.

theorem sqrt_two_irrational_V1 {a b : ℕ} (co : gcd a b = 1) : a^2 ≠ 2 * b^2 :=
assume h : a^2 = 2 * b^2,
have 2 ∣ a^2,
    by simp [h],
have ha : 2 ∣ a,
    from prime.dvd_of_dvd_pow prime_two this,
-- this line below is wrong
exists.elim ha (assume c : ℕ, assume aeq : a = 2 * c, 
-- also tried "let" and "match"
--let ⟨c, aeq⟩ := ha,
-- match ha with ⟨(c : ℕ), (aeq : a = 2 * c)⟩,
have 2 * (2 * c^2) = 2 * b^2,
    by simp [eq.symm h, aeq]; 
       simp [nat.pow_succ, mul_comm, mul_assoc, mul_left_comm],
have 2 * c^2 = b^2,
    from eq_of_mul_eq_mul_left dec_trivial this,
have 2 ∣ b^2, 
    by simp [eq.symm this],
have hb : 2 ∣ b,
    from prime.dvd_of_dvd_pow prime_two this,
have 2 ∣ gcd a b,
    from dvd_gcd ha hb,
have habs : 2 ∣ (1:ℕ), 
    by simp * at *,
show false, from absurd habs dec_trivial)

I usually use let instead of exists.elim. The syntax is let ⟨c, aeq⟩ := ha in ... This actually causes an error in your current proof, this is due to a bug that means let introduces a hypothesis called _let_match into your context that causes an error if you use it. simp * at * uses it in your proof, but if you replace it with by clear_aux_decl; simp * at * the proof will work.

You could also write match ha with | ⟨c, aeq⟩ := instead of let ⟨c, aeq⟩ := ha in, but this time you have to put end at the end of the proof. This will have the same bug as happens with let and the fix is the same.