Theorem: factors_unique_prod' (FltRegular/FltThree/OddPrimeOrFour.lean)

State before:
⊢ ∀ {f g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
Tactic:
intro f
State after:
f : Multiset ℕ
⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g

State before:
f : Multiset ℕ
⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
Tactic:
induction' f using Multiset.induction_on with p f ih
State after:
case empty

⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ 0, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → Multiset.prod 0 = g.prod → 0 = g

case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
⊢ ∀ {g : Multiset ℕ},
    (∀ x ∈ p ::ₘ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → (p ::ₘ f).prod = g.prod → p ::ₘ f = g

State before:
case empty

⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ 0, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → Multiset.prod 0 = g.prod → 0 = g
Tactic:
rintro g - hg h
State after:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : Multiset.prod 0 = g.prod
⊢ 0 = g

State before:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : Multiset.prod 0 = g.prod
⊢ 0 = g
Tactic:
rw [Multiset.prod_zero] at h
State after:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ 0 = g

State before:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ 0 = g
Tactic:
symm
State after:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ g = 0

State before:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ g = 0
Tactic:
apply Multiset.eq_zero_of_forall_not_mem
State after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ ∀ (x : ℕ), x ∉ g

State before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ ∀ (x : ℕ), x ∉ g
Tactic:
intro x hx
State after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ False

State before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ False
Tactic:
apply (hg x hx).not_unit
State after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ IsUnit x

State before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ IsUnit x
Tactic:
rw [isUnit_iff_dvd_one]
State after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ x ∣ 1

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

State before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
⊢ ∀ {g : Multiset ℕ},
    (∀ x ∈ p ::ₘ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → (p ::ₘ f).prod = g.prod → p ::ₘ f = g
Tactic:
intro g hf hg hfg
State after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
⊢ p ::ₘ f = g

State before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
⊢ p ::ₘ f = g
Tactic:
have hp := hf p (Multiset.mem_cons_self _ _)
State after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ::ₘ f = g

State before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ::ₘ f = g
Tactic:
have hdvd : p ∣ g.prod :=
  by
  rw [← hfg, Multiset.prod_cons]
  exact dvd_mul_right _ _
State after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
⊢ p ::ₘ f = g

State before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
⊢ p ::ₘ f = g
Tactic:
have hbg := mem_of_dvd_prod hp hg hdvd
State after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = g

State before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = g
Tactic:
rw [← Multiset.cons_erase hbg]
State after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = p ::ₘ g.erase p

State before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = p ::ₘ g.erase p
Tactic:
congr
State after:
case cons.e_s
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f = g.erase p

State before:
case cons.e_s
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f = g.erase p
Tactic:
apply ih _ _ _
State after:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ f, OddPrimeOrFour x

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

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

State before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ∣ g.prod
Tactic:
rw [← hfg, Multiset.prod_cons]
State after:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ∣ p * f.prod

State before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ∣ p * f.prod
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ 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 ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ g.erase p, OddPrimeOrFour x
Tactic:
exact fun q hq => hg q (Multiset.mem_of_mem_erase hq)
State after:
no goals

State before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f.prod = (g.erase p).prod
Tactic:
apply mul_left_cancel₀ hp.ne_zero
State after:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p * f.prod = p * (g.erase p).prod

State before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p * f.prod = p * (g.erase p).prod
Tactic:
rwa [Multiset.prod_erase hbg, ← Multiset.prod_cons]
State after:
no goals