cases' h3 with H₁ H₂
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
h3 : p = 1 ∨ p = 3
⊢ False
case inl
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₁ : p = 1
⊢ False

case inr
p : ℕ
a b c : ℤ
hpri : p.Prime
hp : p ≠ 3
this : Fact p.Prime := { out := hpri }
hbc : ↑b = -↑c
hab : ↑a = ↑b
h : ↑c = 0 ∨ 3 = 0
H₂ : p = 3
⊢ False