induction' f using Multiset.induction_on with p f ih
f : Multiset ℤ
⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
case h₁

⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ 0 → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod 0) (Multiset.prod g) → Multiset.Rel Associated 0 g

case h₂
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 ℤ},
    (∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g) → Multiset.Rel Associated (p ::ₘ f) g