no goals
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : ∏ x in s, f x ≠ 1
⊢ ∃ a, a ∈ s ∧ f a ≠ 1
classical
  rw [← prod_filter_ne_one] at h
  rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩
  exact ⟨x, (mem_filter.1 hx).1, by simpa using (mem_filter.1 hx).2⟩
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h✝ : ∏ x in s, f x ≠ 1
h : ∏ x in filter (fun x => f x ≠ 1) s, f x ≠ 1
⊢ ∃ a, a ∈ s ∧ f a ≠ 1
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h : ∏ x in s, f x ≠ 1
⊢ ∃ a, a ∈ s ∧ f a ≠ 1
rw [← prod_filter_ne_one] at h
case intro
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h✝ : ∏ x in s, f x ≠ 1
h : ∏ x in filter (fun x => f x ≠ 1) s, f x ≠ 1
x : α
hx : x ∈ filter (fun x => f x ≠ 1) s
⊢ ∃ a, a ∈ s ∧ f a ≠ 1
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h✝ : ∏ x in s, f x ≠ 1
h : ∏ x in filter (fun x => f x ≠ 1) s, f x ≠ 1
⊢ ∃ a, a ∈ s ∧ f a ≠ 1
rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩
no goals
case intro
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h✝ : ∏ x in s, f x ≠ 1
h : ∏ x in filter (fun x => f x ≠ 1) s, f x ≠ 1
x : α
hx : x ∈ filter (fun x => f x ≠ 1) s
⊢ ∃ a, a ∈ s ∧ f a ≠ 1
exact ⟨x, (mem_filter.1 hx).1, by simpa using (mem_filter.1 hx).2⟩
no goals
ι : Type ?u.430162
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
h✝ : ∏ x in s, f x ≠ 1
h : ∏ x in filter (fun x => f x ≠ 1) s, f x ≠ 1
x : α
hx : x ∈ filter (fun x => f x ≠ 1) s
⊢ f x ≠ 1
simpa using (mem_filter.1 hx).2