rw [even_iff_two_dvd]
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Even p
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ 2 ∣ p