obtain rfl | ⟨ap, aodd⟩ := ha <;> obtain rfl | ⟨pp, podd⟩ := hp
a p : ℕ
ha : OddPrimeOrFour a
hp : OddPrimeOrFour p
h : p ∣ a
⊢ p = a
case inl.inl
h : 4 ∣ 4
⊢ 4 = 4

case inl.inr.intro
p : ℕ
h : p ∣ 4
pp : p.Prime
podd : Odd p
⊢ p = 4

case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : Odd a
h : 4 ∣ a
⊢ 4 = a

case inr.intro.inr.intro
a p : ℕ
h : p ∣ a
ap : a.Prime
aodd : Odd a
pp : p.Prime
podd : Odd p
⊢ p = a