case h.e'_2.a
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c : α
⊢ ∏ x in Ico a b, f (c + x) = ∏ x in Ico (a + c) (b + c), f x
convert prod_Ico_add' f a b c using 2
no goals
case h.e'_2.a
α : Type u
β : Type v
γ : Type w
s₂ s₁ s : Finset α
a✝¹ : α
g f✝ : α → β
inst✝³ : CommMonoid β
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → β
a b c x✝ : α
a✝ : x✝ ∈ Ico a b
⊢ f (c + x✝) = f (x✝ + c)
rw [add_comm]