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

case inl.inr.intro
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ Associated p 4

case inr.intro.inl
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ Associated 4 a

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