case zero
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ r in range (Nat.zero + 1), f (Nat.zero - r) = ∏ k in range (Nat.zero + 1), f k

case succ
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k
⊢ ∏ r in range (Nat.succ n + 1), f (Nat.succ n - r) = ∏ k in range (Nat.succ n + 1), f k
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
n : ℕ
f : ℕ → β
⊢ ∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k
induction' n with n ih
no goals
case zero
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ r in range (Nat.zero + 1), f (Nat.zero - r) = ∏ k in range (Nat.zero + 1), f k
rw [prod_range_one, prod_range_one]
case succ
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k
⊢ (∏ k in range (n + 1), f (Nat.succ n - (k + 1))) * f (Nat.succ n - 0) =
    (∏ x in range (Nat.succ n), f x) * f (Nat.succ n)
case succ
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k
⊢ ∏ r in range (Nat.succ n + 1), f (Nat.succ n - r) = ∏ k in range (Nat.succ n + 1), f k
rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
no goals
case succ
ι : Type ?u.711041
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
ih : ∏ r in range (n + 1), f (n - r) = ∏ k in range (n + 1), f k
⊢ (∏ k in range (n + 1), f (Nat.succ n - (k + 1))) * f (Nat.succ n - 0) =
    (∏ x in range (Nat.succ n), f x) * f (Nat.succ n)
simp [← ih]