ι : Type ?u.371468
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1
this : DecidableEq α
⊢ ∏ x in s, f x = f a
ι : Type ?u.371468
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1
⊢ ∏ x in s, f x = f a
haveI := Classical.decEq α
case refine'_1
ι : Type ?u.371468
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1
this : DecidableEq α
a✝ : α
H : a✝ ∈ {a}
⊢ a✝ ∈ s
case refine'_1
ι : Type ?u.371468
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1
this : DecidableEq α
⊢ {a} ⊆ s
intro _ H
no goals
case refine'_1
ι : Type ?u.371468
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝¹ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1
this : DecidableEq α
a✝ : α
H : a✝ ∈ {a}
⊢ a✝ ∈ s
rwa [mem_singleton.1 H]
no goals
case refine'_2
ι : Type ?u.371468
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
h : a ∈ s
h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1
this : DecidableEq α
⊢ ∀ (x : α), x ∈ s → ¬x ∈ {a} → f x = 1
simpa only [mem_singleton]