apply ih _ _ _
case h₂.intro.intro
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Multiset.Rel Associated f (Multiset.erase g b)
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x

p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ ∀ (x : ℤ), x ∈ Multiset.erase g b → OddPrimeOrFour x

p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
hp : OddPrimeOrFour p
hdvd : p ∣ Multiset.prod g
b : ℤ
hbg : b ∈ g
hb : Associated p b
⊢ Associated (Multiset.prod f) (Multiset.prod (Multiset.erase g b))