α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ False
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
⊢ ∃ x, p x
by_contra H
case H
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ ∀ᶠ (x : α) in f, ¬p x

α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ False
replace H : ∀ᶠ x in f, ¬p x
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False
case H
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ ∀ᶠ (x : α) in f, ¬p x

α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False
exact eventually_of_forall (not_exists.1 H)
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.160311
ι : Sort x
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ∀ᶠ (x : α) in f, ¬p x
⊢ False
exact hp H