refine' ⟨a, ha, fun x hx => le_of_not_lt fun hxa => _⟩
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
x : α
hx : x ∈ s
hxa : f x < f a
⊢ False