apply And.intro ha
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ a ∈ s ∧ f a = ⨅ x ∈ s, f x
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a = ⨅ x ∈ s, f x