m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
⊢ False
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
⊢ Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
by_contra H
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ Int.natAbs (m ^ 2 - n ^ 2)
hp2 : p ∣ Int.natAbs (m ^ 2 + n ^ 2)
⊢ False
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
⊢ False
obtain ⟨p, hp, hp1, hp2⟩ := Nat.Prime.not_coprime_iff_dvd.mp H
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ False
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ Int.natAbs (m ^ 2 - n ^ 2)
hp2 : p ∣ Int.natAbs (m ^ 2 + n ^ 2)
⊢ False
rw [← Int.coe_nat_dvd_left] at hp1 hp2
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ False
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ False
have h2m : (p : ℤ) ∣ 2 * m ^ 2 := by
  convert dvd_add hp2 hp1 using 1
  ring
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
⊢ False
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ False
have h2n : (p : ℤ) ∣ 2 * n ^ 2 := by
  convert dvd_sub hp2 hp1 using 1
  ring
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
⊢ False
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
⊢ False
have hmc : p = 2 ∨ p ∣ Int.natAbs m := prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2m
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
⊢ False
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
⊢ False
have hnc : p = 2 ∨ p ∣ Int.natAbs n := prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2n
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
⊢ False

case neg
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : ¬p = 2
⊢ False
case intro.intro.intro
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
⊢ False
by_cases h2 : p = 2
case h.e'_4
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ 2 * m ^ 2 = m ^ 2 + n ^ 2 + (m ^ 2 - n ^ 2)
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ ↑p ∣ 2 * m ^ 2
convert dvd_add hp2 hp1 using 1
no goals
case h.e'_4
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
⊢ 2 * m ^ 2 = m ^ 2 + n ^ 2 + (m ^ 2 - n ^ 2)
ring
case h.e'_4
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ 2 * n ^ 2 = m ^ 2 + n ^ 2 - (m ^ 2 - n ^ 2)
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ ↑p ∣ 2 * n ^ 2
convert dvd_sub hp2 hp1 using 1
no goals
case h.e'_4
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ 2 * n ^ 2 = m ^ 2 + n ^ 2 - (m ^ 2 - n ^ 2)
ring
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
⊢ False
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
⊢ False
have h3 : (m ^ 2 + n ^ 2) % 2 = 1 := by field_simp [sq, Int.add_emod, Int.mul_emod, hm, hn]
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
h4 : (m ^ 2 + n ^ 2) % 2 = 0
⊢ False
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
⊢ False
have h4 : (m ^ 2 + n ^ 2) % 2 = 0 := by
  apply Int.emod_eq_zero_of_dvd
  rwa [h2] at hp2
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : 0 = 1
h4 : (m ^ 2 + n ^ 2) % 2 = 0
⊢ False
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
h4 : (m ^ 2 + n ^ 2) % 2 = 0
⊢ False
rw [h4] at h3
no goals
case pos
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : 0 = 1
h4 : (m ^ 2 + n ^ 2) % 2 = 0
⊢ False
exact zero_ne_one h3
no goals
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
⊢ (m ^ 2 + n ^ 2) % 2 = 1
field_simp [sq, Int.add_emod, Int.mul_emod, hm, hn]
case a
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
⊢ 2 ∣ m ^ 2 + n ^ 2
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
⊢ (m ^ 2 + n ^ 2) % 2 = 0
apply Int.emod_eq_zero_of_dvd
no goals
case a
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : p = 2
h3 : (m ^ 2 + n ^ 2) % 2 = 1
⊢ 2 ∣ m ^ 2 + n ^ 2
rwa [h2] at hp2
case neg
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : ¬p = 2
⊢ p ∣ 1
case neg
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : ¬p = 2
⊢ False
apply hp.not_dvd_one
case neg
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : ¬p = 2
⊢ p ∣ Int.gcd m n
case neg
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : ¬p = 2
⊢ p ∣ 1
rw [← h]
no goals
case neg
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
hmc : p = 2 ∨ p ∣ Int.natAbs m
hnc : p = 2 ∨ p ∣ Int.natAbs n
h2 : ¬p = 2
⊢ p ∣ Int.gcd m n
exact Nat.dvd_gcd (Or.resolve_left hmc h2) (Or.resolve_left hnc h2)