α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = ∅ → ∀ (x : α), x ∈ s → ¬p x
α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
refine' ⟨_, filter_false_of_mem⟩
α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
hs : filter p s = ∅
⊢ ∀ (x : α), x ∈ s → ¬p x
α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = ∅ → ∀ (x : α), x ∈ s → ¬p x
intro hs
α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
hs' : Multiset.filter p s.val = 0
⊢ ∀ (x : α), x ∈ s → ¬p x
α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
hs : filter p s = ∅
⊢ ∀ (x : α), x ∈ s → ¬p x
injection hs with hs'
no goals
α : Type u_1
β : Type ?u.323706
γ : Type ?u.323709
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
hs' : Multiset.filter p s.val = 0
⊢ ∀ (x : α), x ∈ s → ¬p x
rwa [filter_eq_nil] at hs'