ι : Type ?u.880413
β✝ : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a✝ : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : Subsingleton α
inst✝ : Fintype α
f : α → β
a : α
this : Unique α
⊢ ∏ x : α, f x = f a
ι : Type ?u.880413
β✝ : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a✝ : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : Subsingleton α
inst✝ : Fintype α
f : α → β
a : α
⊢ ∏ x : α, f x = f a
haveI : Unique α := uniqueOfSubsingleton a
no goals
ι : Type ?u.880413
β✝ : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a✝ : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : Subsingleton α
inst✝ : Fintype α
f : α → β
a : α
this : Unique α
⊢ ∏ x : α, f x = f a
rw [prod_unique f, Subsingleton.elim default a]