case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ Int.natAbs m

case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p = 2 ∨ p ∣ Int.natAbs m
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
⊢ p = 2 ∨ p ∣ Int.natAbs m
cases' Int.Prime.dvd_mul hp h with hp2 hpp
case inl.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2
case inl
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ Int.natAbs m
apply Or.intro_left
no goals
case inl.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2
exact le_antisymm (Nat.le_of_dvd zero_lt_two hp2) (Nat.Prime.two_le hp)
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p ∣ Int.natAbs m
case inr
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p = 2 ∨ p ∣ Int.natAbs m
apply Or.intro_right
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs m * Int.natAbs m
⊢ p ∣ Int.natAbs m
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs (m ^ 2)
⊢ p ∣ Int.natAbs m
rw [sq, Int.natAbs_mul] at hpp
no goals
case inr.h
m : ℤ
p : ℕ
hp : Nat.Prime p
h : ↑p ∣ 2 * m ^ 2
hpp : p ∣ Int.natAbs m * Int.natAbs m
⊢ p ∣ Int.natAbs m
exact (or_self_iff _).mp ((Nat.Prime.dvd_mul hp).mp hpp)