rw [← even_iff_two_dvd, ← Int.odd_iff_not_even] at hI
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
⊢ 2 ∣ c
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ 2 ∣ c