case zero
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ j in range zero, f (zero - 1 - j) = ∏ j in range zero, f j

case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ j in range (succ n✝), f (succ n✝ - 1 - j) = ∏ j in range (succ n✝), f j
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ j in range n, f (n - 1 - j) = ∏ j in range n, f j
cases n
no goals
case zero
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
⊢ ∏ j in range zero, f (zero - 1 - j) = ∏ j in range zero, f j
simp
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ x in Ico 0 (succ n✝), f (n✝ - x) = ∏ x in Ico 0 (succ n✝), f x
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ j in range (succ n✝), f (succ n✝ - 1 - j) = ∏ j in range (succ n✝), f j
simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ j in Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x in Ico 0 (succ n✝), f x
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ x in Ico 0 (succ n✝), f (n✝ - x) = ∏ x in Ico 0 (succ n✝), f x
rw [prod_Ico_reflect _ _ le_rfl]
no goals
case succ
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a : α
g f✝ : α → β
inst✝ : CommMonoid β
f : ℕ → β
n✝ : ℕ
⊢ ∏ j in Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x in Ico 0 (succ n✝), f x
simp