case zero
ι : Type ?u.441582
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ x in range (n + Nat.zero), f x = (∏ x in range n, f x) * ∏ x in range Nat.zero, f (n + x)

case succ
ι : Type ?u.441582
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n m : ℕ
hm : ∏ x in range (n + m), f x = (∏ x in range n, f x) * ∏ x in range m, f (n + x)
⊢ ∏ x in range (n + Nat.succ m), f x = (∏ x in range n, f x) * ∏ x in range (Nat.succ m), f (n + x)
ι : Type ?u.441582
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n m : ℕ
⊢ ∏ x in range (n + m), f x = (∏ x in range n, f x) * ∏ x in range m, f (n + x)
induction' m with m hm
no goals
case zero
ι : Type ?u.441582
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ x in range (n + Nat.zero), f x = (∏ x in range n, f x) * ∏ x in range Nat.zero, f (n + x)
simp
no goals
case succ
ι : Type ?u.441582
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n m : ℕ
hm : ∏ x in range (n + m), f x = (∏ x in range n, f x) * ∏ x in range m, f (n + x)
⊢ ∏ x in range (n + Nat.succ m), f x = (∏ x in range n, f x) * ∏ x in range (Nat.succ m), f (n + x)
erw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]