Theorem: Imo1986P1.imo1986_p1' (Compfiles/Imo1986P1.lean)

State before:
d : ℤ
⊢ ¬(IsSquare (2 * d - 1) ∧ IsSquare (5 * d - 1) ∧ IsSquare (d * 13 - 1))
Tactic:
rintro ⟨⟨p, hp⟩, ⟨q, hq⟩, ⟨r, hr⟩⟩
State after:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p * p
q : ℤ
hq : 5 * d - 1 = q * q
r : ℤ
hr : d * 13 - 1 = r * r
⊢ False

State before:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p * p
q : ℤ
hq : 5 * d - 1 = q * q
r : ℤ
hr : d * 13 - 1 = r * r
⊢ False
Tactic:
rw [← pow_two] at hp hq hr
State after:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ False

State before:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ False
Tactic:
have hpodd : Odd p := (Int.odd_pow' two_ne_zero).mp (by use d - 1; rw [← hp]; ring)
State after:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
hpodd : Odd p
⊢ False

State before:
case intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
hpodd : Odd p
⊢ False
Tactic:
cases' hpodd with k hk
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
⊢ False
Tactic:
have hp := hp.symm
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
⊢ False
Tactic:
have hdp : d  = 2*(k + k^2) + 1 := by
  rw [hk, ←(add_left_inj 1), sub_add_cancel _] at hp
  ring_nf at hp
  have h422 : (4 : ℤ) = 2 * 2 := by norm_num
  simp only [h422,  ← mul_assoc] at hp
  nth_rw 1 [← one_mul 2] at hp
  rw [← add_mul, ← add_mul, mul_left_inj' two_ne_zero] at hp
  rw [← hp]
  ring
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
⊢ False
Tactic:
have hdodd : Odd d := by use k + k ^ 2
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ False
Tactic:
have hd_sub_one : Even (d - 1) := by use (k + k ^ 2); rw [hdp]; ring
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ False
Tactic:
have hqeven : Even q := by
  refine (Int.even_pow' two_ne_zero).mp ?_
  have heq : 5 * d - 1 = 5 * (d - 1) + 4 := by ring_nf
  rw [← hq, heq]
  exact Even.add (Even.mul_left hd_sub_one 5) (by use 2; rfl)
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ False
Tactic:
have hreven : Even (r : ℤ) := by
  refine (Int.even_pow' two_ne_zero).mp ?_
  have heq : d * 13 - 1 = 13*(d - 1) + 12 := by
    rw [mul_comm]
    ring_nf
  rw [← hr, heq]
  exact Even.add (Even.mul_left hd_sub_one 13) (by use 6; rfl)
State after:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
hreven : Even r
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
hreven : Even r
⊢ False
Tactic:
cases' hqeven with n hqeven'
State after:
case intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hreven : Even r
n : ℤ
hqeven' : q = n + n
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hreven : Even r
n : ℤ
hqeven' : q = n + n
⊢ False
Tactic:
cases' hreven with m hreven'
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ False
Tactic:
have h8d : d * 8 = 4*m^2 - 4*n^2 := by
  calc d * 8 = (d * 13 - 1) - (5 * d - 1) := by ring
        _ = r^2 - q^2 := by rw [hr, hq]
        _ = (m + m)^2 - (n + n)^2 := by rw [hqeven', hreven']
        _ = 4*m^2 - 4*n^2 := by ring
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ False
Tactic:
have h4d : 4 * (2 * d) = 4 * (m^2 - n^2) := by ring_nf; rw [h8d]; ring_nf
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ False
Tactic:
have hnm' : 2*d = (m + n)*(m - n):= by
  rw [← pow_two_sub_pow_two]
  refine (mul_right_inj' ?_).mp h4d
  decide
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ False
Tactic:
have h2d : Even ((m + n) * (m - n)) := by use d; rw [← two_mul, hnm']
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
⊢ False
Tactic:
have hnm_sub : Even (m - n) := Int.even_sub.mpr hnm_parity
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
⊢ False
Tactic:
have hnm_add : Even (m + n) := Int.even_add.mpr hnm_parity
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
⊢ False
Tactic:
have hdeven : Even d := by
  cases' hnm_sub with v hnm_sub
  cases' hnm_add with w hnm_add
  simp only [hnm_sub, hnm_add, ← two_mul] at hnm'
  rw [mul_assoc,  mul_right_inj' two_ne_zero, ← mul_assoc, mul_comm w, mul_assoc, two_mul] at hnm'
  exact ⟨w * v, hnm'⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
hdeven : Even d
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
hdeven : Even d
⊢ False
Tactic:
exact Int.even_iff_not_odd.mp hdeven hdodd
State after:
no goals

State before:
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ Odd (p ^ 2)
Tactic:
use d - 1
State after:
case h
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ p ^ 2 = 2 * (d - 1) + 1

State before:
case h
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ p ^ 2 = 2 * (d - 1) + 1
Tactic:
rw [← hp]
State after:
case h
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ 2 * d - 1 = 2 * (d - 1) + 1

State before:
case h
d p : ℤ
hp : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
⊢ 2 * d - 1 = 2 * (d - 1) + 1
Tactic:
ring
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
rw [hk, ←(add_left_inj 1), sub_add_cancel _] at hp
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : (2 * k + 1) ^ 2 + 1 = 2 * d
⊢ d = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : (2 * k + 1) ^ 2 + 1 = 2 * d
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
ring_nf at hp
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : 2 + k * 4 + k ^ 2 * 4 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : 2 + k * 4 + k ^ 2 * 4 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
have h422 : (4 : ℤ) = 2 * 2 := by norm_num
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : 2 + k * 4 + k ^ 2 * 4 = d * 2
h422 : 4 = 2 * 2
⊢ d = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : 2 + k * 4 + k ^ 2 * 4 = d * 2
h422 : 4 = 2 * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
simp only [h422,  ← mul_assoc] at hp
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
nth_rw 1 [← one_mul 2] at hp
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 1 * 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 1 * 2 + k * 2 * 2 + k ^ 2 * 2 * 2 = d * 2
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
rw [← add_mul, ← add_mul, mul_left_inj' two_ne_zero] at hp
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ d = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ d = 2 * (k + k ^ 2) + 1
Tactic:
rw [← hp]
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ 1 + k * 2 + k ^ 2 * 2 = 2 * (k + k ^ 2) + 1

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
h422 : 4 = 2 * 2
hp : 1 + k * 2 + k ^ 2 * 2 = d
⊢ 1 + k * 2 + k ^ 2 * 2 = 2 * (k + k ^ 2) + 1
Tactic:
ring
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : 2 + k * 4 + k ^ 2 * 4 = d * 2
⊢ 4 = 2 * 2
Tactic:
norm_num
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
⊢ Odd d
Tactic:
use k + k ^ 2
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ Even (d - 1)
Tactic:
use (k + k ^ 2)
State after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ d - 1 = k + k ^ 2 + (k + k ^ 2)

State before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ d - 1 = k + k ^ 2 + (k + k ^ 2)
Tactic:
rw [hdp]
State after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ 2 * (k + k ^ 2) + 1 - 1 = k + k ^ 2 + (k + k ^ 2)

State before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
⊢ 2 * (k + k ^ 2) + 1 - 1 = k + k ^ 2 + (k + k ^ 2)
Tactic:
ring
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ Even q
Tactic:
refine (Int.even_pow' two_ne_zero).mp ?_
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ Even (q ^ 2)

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ Even (q ^ 2)
Tactic:
have heq : 5 * d - 1 = 5 * (d - 1) + 4 := by ring_nf
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (q ^ 2)

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (q ^ 2)
Tactic:
rw [← hq, heq]
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (5 * (d - 1) + 4)

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even (5 * (d - 1) + 4)
Tactic:
exact Even.add (Even.mul_left hd_sub_one 5) (by use 2; rfl)
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
⊢ 5 * d - 1 = 5 * (d - 1) + 4
Tactic:
ring_nf
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ Even 4
Tactic:
use 2
State after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ 4 = 2 + 2

State before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
heq : 5 * d - 1 = 5 * (d - 1) + 4
⊢ 4 = 2 + 2
Tactic:
rfl
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ Even r
Tactic:
refine (Int.even_pow' two_ne_zero).mp ?_
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ Even (r ^ 2)

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ Even (r ^ 2)
Tactic:
have heq : d * 13 - 1 = 13*(d - 1) + 12 := by
  rw [mul_comm]
  ring_nf
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (r ^ 2)

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (r ^ 2)
Tactic:
rw [← hr, heq]
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (13 * (d - 1) + 12)

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even (13 * (d - 1) + 12)
Tactic:
exact Even.add (Even.mul_left hd_sub_one 13) (by use 6; rfl)
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ d * 13 - 1 = 13 * (d - 1) + 12
Tactic:
rw [mul_comm]
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ 13 * d - 1 = 13 * (d - 1) + 12

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
⊢ 13 * d - 1 = 13 * (d - 1) + 12
Tactic:
ring_nf
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ Even 12
Tactic:
use 6
State after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ 12 = 6 + 6

State before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
hqeven : Even q
heq : d * 13 - 1 = 13 * (d - 1) + 12
⊢ 12 = 6 + 6
Tactic:
rfl
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ d * 8 = 4 * m ^ 2 - 4 * n ^ 2
Tactic:
calc d * 8 = (d * 13 - 1) - (5 * d - 1) := by ring
      _ = r^2 - q^2 := by rw [hr, hq]
      _ = (m + m)^2 - (n + n)^2 := by rw [hqeven', hreven']
      _ = 4*m^2 - 4*n^2 := by ring
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ d * 8 = d * 13 - 1 - (5 * d - 1)
Tactic:
ring
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ d * 13 - 1 - (5 * d - 1) = r ^ 2 - q ^ 2
Tactic:
rw [hr, hq]
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ r ^ 2 - q ^ 2 = (m + m) ^ 2 - (n + n) ^ 2
Tactic:
rw [hqeven', hreven']
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
⊢ (m + m) ^ 2 - (n + n) ^ 2 = 4 * m ^ 2 - 4 * n ^ 2
Tactic:
ring
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
Tactic:
ring_nf
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ d * 8 = m ^ 2 * 4 - n ^ 2 * 4

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ d * 8 = m ^ 2 * 4 - n ^ 2 * 4
Tactic:
rw [h8d]
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ 4 * m ^ 2 - 4 * n ^ 2 = m ^ 2 * 4 - n ^ 2 * 4

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
⊢ 4 * m ^ 2 - 4 * n ^ 2 = m ^ 2 * 4 - n ^ 2 * 4
Tactic:
ring_nf
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 2 * d = (m + n) * (m - n)
Tactic:
rw [← pow_two_sub_pow_two]
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 2 * d = m ^ 2 - n ^ 2

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 2 * d = m ^ 2 - n ^ 2
Tactic:
refine (mul_right_inj' ?_).mp h4d
State after:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 4 ≠ 0

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
⊢ 4 ≠ 0
Tactic:
decide
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ Even ((m + n) * (m - n))
Tactic:
use d
State after:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ (m + n) * (m - n) = d + d

State before:
case h
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
⊢ (m + n) * (m - n) = d + d
Tactic:
rw [← two_mul, hnm']
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
⊢ Even m ↔ Even n
Tactic:
cases' Int.even_mul.mp h2d with hmneven hmneven
State after:
case inl
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m + n)
⊢ Even m ↔ Even n

case inr
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m - n)
⊢ Even m ↔ Even n

State before:
case inl
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m + n)
⊢ Even m ↔ Even n
Tactic:
exact Int.even_add.mp hmneven
State after:
no goals

State before:
case inr
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hmneven : Even (m - n)
⊢ Even m ↔ Even n
Tactic:
exact Int.even_sub.mp hmneven
State after:
no goals

State before:
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_sub : Even (m - n)
hnm_add : Even (m + n)
⊢ Even d
Tactic:
cases' hnm_sub with v hnm_sub
State after:
case intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_add : Even (m + n)
v : ℤ
hnm_sub : m - n = v + v
⊢ Even d

State before:
case intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
hnm_add : Even (m + n)
v : ℤ
hnm_sub : m - n = v + v
⊢ Even d
Tactic:
cases' hnm_add with w hnm_add
State after:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
⊢ Even d

State before:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
hnm' : 2 * d = (m + n) * (m - n)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
⊢ Even d
Tactic:
simp only [hnm_sub, hnm_add, ← two_mul] at hnm'
State after:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : 2 * d = 2 * w * (2 * v)
⊢ Even d

State before:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : 2 * d = 2 * w * (2 * v)
⊢ Even d
Tactic:
rw [mul_assoc,  mul_right_inj' two_ne_zero, ← mul_assoc, mul_comm w, mul_assoc, two_mul] at hnm'
State after:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : d = w * v + w * v
⊢ Even d

State before:
case intro.intro
d p : ℤ
hp✝ : 2 * d - 1 = p ^ 2
q : ℤ
hq : 5 * d - 1 = q ^ 2
r : ℤ
hr : d * 13 - 1 = r ^ 2
k : ℤ
hk : p = 2 * k + 1
hp : p ^ 2 = 2 * d - 1
hdp : d = 2 * (k + k ^ 2) + 1
hdodd : Odd d
hd_sub_one : Even (d - 1)
n : ℤ
hqeven' : q = n + n
m : ℤ
hreven' : r = m + m
h8d : d * 8 = 4 * m ^ 2 - 4 * n ^ 2
h4d : 4 * (2 * d) = 4 * (m ^ 2 - n ^ 2)
h2d : Even ((m + n) * (m - n))
hnm_parity : Even m ↔ Even n
v : ℤ
hnm_sub : m - n = v + v
w : ℤ
hnm_add : m + n = w + w
hnm' : d = w * v + w * v
⊢ Even d
Tactic:
exact ⟨w * v, hnm'⟩
State after:
no goals