case zero
u : PrimeMultiset
⊢ prod (Nat.zero • u) = Pow.pow (prod u) Nat.zero

case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
d : ℕ
u : PrimeMultiset
⊢ prod (d • u) = Pow.pow (prod u) d
induction' d with n ih
no goals
case zero
u : PrimeMultiset
⊢ prod (Nat.zero • u) = Pow.pow (prod u) Nat.zero
rfl
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
this : ∀ (n' : ℕ), Pow.pow (prod u) n' = Monoid.npow n' (prod u)
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
have : ∀ n' : ℕ, Pow.pow (prod u) n' = Monoid.npow n' (prod u) := fun _ ↦ rfl
no goals
case succ
u : PrimeMultiset
n : ℕ
ih : prod (n • u) = Pow.pow (prod u) n
this : ∀ (n' : ℕ), Pow.pow (prod u) n' = Monoid.npow n' (prod u)
⊢ prod (Nat.succ n • u) = Pow.pow (prod u) (Nat.succ n)
rw [succ_nsmul, prod_add, ih, this, this, Monoid.npow_succ, mul_comm]