ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
⊢ (∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop, p x
refine ⟨fun h ↦ h.mono fun x hx ↦ hx x le_rfl, fun h ↦ ?_⟩
case intro.intro
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
hS : ∀ ⦃x : α⦄, (x ∈ ⋂ (i : α) (_ : i ∈ S), Ici i) → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩
case intro.intro
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
hS : ∀ ⦃x : α⦄, (x ∈ ⋂ (i : α) (_ : i ∈ S), Ici i) → p x
x : α
hx : x ∈ ⋂ (i : ↑S), (fun x => Ici ↑x) i
y : α
hy : x ≤ y
⊢ p y
case intro.intro
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
hS : ∀ ⦃x : α⦄, (x ∈ ⋂ (i : α) (_ : i ∈ S), Ici i) → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
refine mem_iInf_of_iInter hSf (V := fun x ↦ Ici x.1) (fun _ ↦ Subset.rfl) fun x hx y hy ↦ ?_
case intro.intro
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ (i : α), i ∈ S → x ∈ Ici i) → p x
hx : ∀ (i : ↑S), x ∈ Ici ↑i
⊢ p y
case intro.intro
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
hS : ∀ ⦃x : α⦄, (x ∈ ⋂ (i : α) (_ : i ∈ S), Ici i) → p x
x : α
hx : x ∈ ⋂ (i : ↑S), (fun x => Ici ↑x) i
y : α
hy : x ≤ y
⊢ p y
simp only [mem_iInter] at hS hx
no goals
case intro.intro
ι : Type ?u.17904
ι' : Type ?u.17907
α : Type u_1
β : Type ?u.17913
γ : Type ?u.17916
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : Set.Finite S
x y : α
hy : x ≤ y
hS : ∀ ⦃x : α⦄, (∀ (i : α), i ∈ S → x ∈ Ici i) → p x
hx : ∀ (i : ↑S), x ∈ Ici ↑i
⊢ p y
exact hS fun z hz ↦ le_trans (hx ⟨z, hz⟩) hy