fin_cases this
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hodd : p ≠ 2
hprod : a * b * c ≠ 0
habs : p < 5
this : p ∈ Ioo 2 5
⊢ False
case head
p : ℕ
hpri✝ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri : Fact (2 + 1).Prime
hreg : IsRegularPrime (2 + 1)
hI : ¬↑(2 + 1) ∣ a * b * c
H : a ^ (2 + 1) + b ^ (2 + 1) = c ^ (2 + 1)
hodd : 2 + 1 ≠ 2
habs : 2 + 1 < 5
⊢ False

case tail.head
p : ℕ
hpri✝ : Fact p.Prime
Heasy : SlightlyEasier
a b c : ℤ
hprod : a * b * c ≠ 0
hpri : Fact (2 + 1 + 1).Prime
hreg : IsRegularPrime (2 + 1 + 1)
hI : ¬↑(2 + 1 + 1) ∣ a * b * c
H : a ^ (2 + 1 + 1) + b ^ (2 + 1 + 1) = c ^ (2 + 1 + 1)
hodd : 2 + 1 + 1 ≠ 2
habs : 2 + 1 + 1 < 5
⊢ False