ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
⊢ f x = 1
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
⊢ ∀ (x : α), x ∈ s → f x = 1
intro x hx
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f x = 1

case neg
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
h : ¬x = a
⊢ f x = 1
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
⊢ f x = 1
by_cases h : x = a
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f a = 1
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f x = 1
rw [h]
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
h : x = a
⊢ f a = 1
rw [h] at hx
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : f a = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1
rw [← prod_subset (singleton_subset_iff.2 hx) fun t ht ha => h1 t ht (not_mem_singleton.1 ha),
  prod_singleton] at hp
no goals
case pos
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : f a = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : a ∈ s
h : x = a
⊢ f a = 1
exact hp
no goals
case neg
ι : Type ?u.804263
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
inst✝ : CommMonoid β
s : Finset α
f : α → β
a : α
hp : ∏ x in s, f x = 1
h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1
x : α
hx : x ∈ s
h : ¬x = a
⊢ f x = 1
exact h1 x hx h