no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.140286
ι : Sort x
f : Filter α
t : NeBot f
p : Prop
h : p
⊢ (∀ᶠ (x : α) in f, p) ↔ p
simp [h]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.140286
ι : Sort x
f : Filter α
t : NeBot f
p : Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p) ↔ p
simpa [h] using t.ne