Theorem: factors_unique_prod' (Flt/OddPrimeOrFour.lean)

State before:
⊢ ∀ {f g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
Tactic:
intro f
State after:
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

State before:
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
Tactic:
induction' f using Multiset.induction_on with p f ih
State after:
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

State before:
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
Tactic:
rintro g - hg h
State after:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated (Multiset.prod 0) (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g

State before:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated (Multiset.prod 0) (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
Tactic:
rw [Multiset.prod_zero] at h
State after:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g

State before:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
Tactic:
rw [Multiset.rel_zero_left]
State after:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ g = 0

State before:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ g = 0
Tactic:
apply Multiset.eq_zero_of_forall_not_mem
State after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ ∀ (x : ℤ), ¬x ∈ g

State before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ ∀ (x : ℤ), ¬x ∈ g
Tactic:
intro x hx
State after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ False

State before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ False
Tactic:
apply (hg x hx).not_unit
State after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ IsUnit x

State before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ IsUnit x
Tactic:
rw [isUnit_iff_dvd_one]
State after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ x ∣ 1

State before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ x ∣ 1
Tactic:
exact dvd_trans (Multiset.dvd_prod hx) h.symm.dvd
State after:
no goals

State before:
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
Tactic:
intro g hf hg hfg
State after:
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 ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
⊢ Multiset.Rel Associated (p ::ₘ f) g

State before:
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 ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
have hp := hf p (Multiset.mem_cons_self _ _)
State after:
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 ℤ
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
⊢ Multiset.Rel Associated (p ::ₘ f) g

State before:
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 ℤ
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
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
have hdvd : p ∣ g.prod :=
  by
  rw [← hfg.dvd_iff_dvd_right, Multiset.prod_cons]
  exact dvd_mul_right _ _
State after:
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 ℤ
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
⊢ Multiset.Rel Associated (p ::ₘ f) g

State before:
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 ℤ
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
⊢ Multiset.Rel Associated (p ::ₘ f) g
Tactic:
obtain ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod'' hp hg hdvd
State after:
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 (p ::ₘ f) g

State before:
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 (p ::ₘ f) g
Tactic:
rw [← Multiset.cons_erase hbg]
State after:
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 (p ::ₘ f) (b ::ₘ Multiset.erase g b)

State before:
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 (p ::ₘ f) (b ::ₘ Multiset.erase g b)
Tactic:
apply Multiset.Rel.cons hb
State after:
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)

State before:
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)
Tactic:
apply ih _ _ _
State after:
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))

State before:
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
⊢ p ∣ Multiset.prod g
Tactic:
rw [← hfg.dvd_iff_dvd_right, Multiset.prod_cons]
State after:
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
⊢ p ∣ p * Multiset.prod f

State before:
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
⊢ p ∣ p * Multiset.prod f
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
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
Tactic:
exact fun q hq => hf _ (Multiset.mem_cons_of_mem hq)
State after:
no goals

State before:
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
Tactic:
exact fun q (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq)
State after:
no goals

State before:
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))
Tactic:
apply Associated.of_mul_left _ hb hp.ne_zero
State after:
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 (p * Multiset.prod f) (b * Multiset.prod (Multiset.erase g b))

State before:
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 (p * Multiset.prod f) (b * Multiset.prod (Multiset.erase g b))
Tactic:
rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]
State after:
no goals