m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
⊢ False
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ Int.natAbs (m ^ 2 - n ^ 2)
hp2 : p ∣ Int.natAbs (2 * m * n)
⊢ False
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * 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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ Int.natAbs (m ^ 2 - n ^ 2)
hp2 : p ∣ Int.natAbs (2 * m * n)
⊢ 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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m 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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ False
have hnp : ¬(p : ℤ) ∣ Int.gcd m n := by
  rw [h]
  norm_cast
  exact mt Nat.dvd_one.mp (Nat.Prime.ne_one hp)
case intro.intro.intro.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs (2 * m)
⊢ False

case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hpn : 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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
⊢ False
cases' Int.Prime.dvd_mul hp hp2 with hp2m hpn
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ False
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hpn : p ∣ Int.natAbs n
⊢ False
rw [Int.gcd_comm] at hnp
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ False
apply mt (Int.dvd_gcd (Int.coe_nat_dvd_left.mpr hpn)) hnp
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m ∨ ↑p ∣ m
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m
apply (or_self_iff _).mp
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m * m
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m ∨ ↑p ∣ m
apply Int.Prime.dvd_mul' hp
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m ^ 2 - n ^ 2 + n * n
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m * m
rw [(by ring : m * m = m ^ 2 - n ^ 2 + n * n)]
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ n * n
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ m ^ 2 - n ^ 2 + n * n
apply dvd_add hp1
no goals
case intro.intro.intro.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ ↑p ∣ n * n
exact (Int.coe_nat_dvd_left.mpr hpn).mul_right n
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ ¬↑p ∣ ↑1
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ ¬↑p ∣ ↑(Int.gcd m n)
rw [h]
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ ¬p ∣ 1
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ ¬↑p ∣ ↑1
norm_cast
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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
⊢ ¬p ∣ 1
exact mt Nat.dvd_one.mp (Nat.Prime.ne_one hp)
case intro.intro.intro.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
⊢ False
case intro.intro.intro.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs (2 * m)
⊢ False
rw [Int.natAbs_mul] at hp2m
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
⊢ False

case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ False
case intro.intro.intro.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
⊢ False
cases' (Nat.Prime.dvd_mul hp).mp hp2m with hp2 hpm
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ n
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ False
apply mt (Int.dvd_gcd (Int.coe_nat_dvd_left.mpr hpm)) hnp
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ n ∨ ↑p ∣ n
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ n
apply (or_self_iff _).mp
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ n * n
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ n ∨ ↑p ∣ n
apply Int.Prime.dvd_mul' hp
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ -(m ^ 2 - n ^ 2) + m * m
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ n * n
rw [(by ring : n * n = -(m ^ 2 - n ^ 2) + m * m)]
no goals
case intro.intro.intro.inl.inr
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ ↑p ∣ -(m ^ 2 - n ^ 2) + m * m
exact hp1.neg_right.add ((Int.coe_nat_dvd_left.2 hpm).mul_right _)
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ False
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
⊢ False
have hp2' : p = 2 := (Nat.le_of_dvd zero_lt_two hp2).antisymm hp.two_le
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ↑p ∣ m ^ 2 - n ^ 2 → False
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ False
revert hp1
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ↑2 ∣ m ^ 2 - n ^ 2 → False
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ↑p ∣ m ^ 2 - n ^ 2 → False
rw [hp2']
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ¬(m ^ 2 - n ^ 2) % ↑2 = 0
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ↑2 ∣ m ^ 2 - n ^ 2 → False
apply mt Int.emod_eq_zero_of_dvd
no goals
case intro.intro.intro.inl.inl
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp2✝ : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hp2 : p ∣ Int.natAbs 2
hp2' : p = 2
⊢ ¬(m ^ 2 - n ^ 2) % ↑2 = 0
field_simp [sq, Int.sub_emod, Int.mul_emod, hm, hn]
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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd m n)
hp2m : p ∣ Int.natAbs 2 * Int.natAbs m
hpm : p ∣ Int.natAbs m
⊢ n * n = -(m ^ 2 - n ^ 2) + m * m
ring
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) (2 * m * n) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ 2 * m * n
hnp : ¬↑p ∣ ↑(Int.gcd n m)
hpn : p ∣ Int.natAbs n
⊢ m * m = m ^ 2 - n ^ 2 + n * n
ring