n m : ℕ+
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
n m : ℕ+
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
let u := factorMultiset n
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
n m : ℕ+
u : PrimeMultiset := factorMultiset n
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
let v := factorMultiset m
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
have : n = u.prod := (prod_factorMultiset n).symm
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (n * m) = factorMultiset n + factorMultiset m
rw [this]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this : n = PrimeMultiset.prod u
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
have : m = v.prod := (prod_factorMultiset m).symm
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * PrimeMultiset.prod v) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * m) = factorMultiset (PrimeMultiset.prod u) + factorMultiset m
rw [this]
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod (u + v)) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod u * PrimeMultiset.prod v) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
rw [← PrimeMultiset.prod_add]
no goals
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ factorMultiset (PrimeMultiset.prod (u + v)) =
    factorMultiset (PrimeMultiset.prod u) + factorMultiset (PrimeMultiset.prod v)
repeat' rw [PrimeMultiset.factorMultiset_prod]
no goals
n m : ℕ+
u : PrimeMultiset := factorMultiset n
v : PrimeMultiset := factorMultiset m
this✝ : n = PrimeMultiset.prod u
this : m = PrimeMultiset.prod v
⊢ u + v = u + factorMultiset (PrimeMultiset.prod v)
rw [PrimeMultiset.factorMultiset_prod]