-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_mul (n m : ℕ+) :
    factorMultiset (n * m) = factorMultiset n + factorMultiset m

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset

Tactic:
rw [this]

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ u + v = u + v.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Result:
no goals

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset

Tactic:
have : m = v.prod := (prod_factorMultiset m).symm

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
repeat' rw [PrimeMultiset.factorMultiset_prod]

Result:
no goals

Proof state:
n m : ℕ+
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
let u := factorMultiset n

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
have : n = u.prod := (prod_factorMultiset n).symm

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
rw [this]

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this : n = u.prod
⊢ (u.prod * m).factorMultiset = u.prod.factorMultiset + m.factorMultiset

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u.prod * v.prod).factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Tactic:
rw [← PrimeMultiset.prod_add]

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
this✝ : n = u.prod
this : m = v.prod
⊢ (u + v).prod.factorMultiset = u.prod.factorMultiset + v.prod.factorMultiset

Proof state:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
let v := factorMultiset m

Result:
n m : ℕ+
u : PrimeMultiset := n.factorMultiset
v : PrimeMultiset := m.factorMultiset
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset