rw [h] at H hI
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
h : p = 2
⊢ False
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑2 ∣ a * b * c
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ False