have hℱs : ℱ ≤ 𝓟 s :=
  iInf_le_of_le ⟨ne_s.choose, ne_s.choose_spec⟩ (principal_mono.mpr <| inter_subset_left _ _)
α : 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 ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
α : 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
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x