no goals
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n : ℕ
⊢ 1 * f 0 = f 0 * 1
rw [one_mul, mul_one]
no goals
α✝ α : Type u
inst✝ : Monoid α
f : ℕ → α
n x✝ : ℕ
hd : prod (map f (range (succ x✝))) = f 0 * prod (map (fun i => f (succ i)) (range x✝))
⊢ prod (map f (range (succ (succ x✝)))) = f 0 * prod (map (fun i => f (succ i)) (range (succ x✝)))
rw [List.prod_range_succ, hd, mul_assoc, ← List.prod_range_succ]