-- Mathlib/Topology/Order/Compact.lean
theorem IsCompact.exists_forall_le' [ClosedIicTopology α] [NoMaxOrder α] {f : β → α}
    {s : Set β} (hs : IsCompact s) (hf : ContinuousOn f s) {a : α} (hf' : ∀ b ∈ s, a < f b) :
    ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Proof state:
case inl.intro
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
a' : α
ha' : a < a'
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

Tactic:
exact ⟨a', ha', fun _ a ↦ a.elim⟩

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

Tactic:
obtain ⟨a', ha'⟩ := exists_gt a

Result:
case inl.intro
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
a' : α
ha' : a < a'
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
obtain ⟨x, hx, hx'⟩ := hs.exists_isMinOn hs' hf

Result:
case inr.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
x : β
hx : x ∈ s
hx' : IsMinOn f s x
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs')

Result:
case inl
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

case inr
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Proof state:
case inr.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
x : β
hx : x ∈ s
hx' : IsMinOn f s x
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

Tactic:
exact ⟨f x, hf' x hx, hx'⟩

Result:
no goals