no goals
ι : Type ?u.334765
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x
x : α
⊢ x ∈ s → ¬x ∈ filter p s → f x = 1
classical
  rw [not_imp_comm, mem_filter]
  exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩
ι : Type ?u.334765
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x
x : α
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
ι : Type ?u.334765
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x
x : α
⊢ x ∈ s → ¬x ∈ filter p s → f x = 1
rw [not_imp_comm, mem_filter]
no goals
ι : Type ?u.334765
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x
x : α
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
exact fun h₁ h₂ => ⟨h₁, by simpa using hp _ h₁ h₂⟩
no goals
ι : Type ?u.334765
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x
x : α
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x
simpa using hp _ h₁ h₂