-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsClosed.mem_of_ge_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b))
    (ha : a ∈ s) (hab : a ≤ b) (hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty) : b ∈ s

Proof state:
case inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ False

Tactic:
rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩

Result:
case inr.intro.intro.intro
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
x : α
xs : x ∈ s
cx : c < x
xb : x ≤ b
⊢ False

Proof state:
case inr.intro.intro.intro
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
x : α
xs : x ∈ s
cx : c < x
xb : x ≤ b
⊢ False

Tactic:
exact not_lt_of_le (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx

Result:
no goals

Proof state:
case inl
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c = b
⊢ b ∈ s

Tactic:
exact hc ▸ c_mem.1

Result:
no goals

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
⊢ b ∈ s

Tactic:
have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
⊢ b ∈ s

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
⊢ b ∈ s

Tactic:
rcases eq_or_lt_of_le c_le with hc | hc

Result:
case inl
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c = b
⊢ b ∈ s

case inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
⊢ b ∈ s

Tactic:
have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
⊢ b ∈ s

Proof state:
case inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ b ∈ s

Tactic:
exfalso

Result:
case inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c < b
⊢ False

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
⊢ b ∈ s

Tactic:
have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
⊢ b ∈ s

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
⊢ b ∈ s

Tactic:
let S := s ∩ Icc a b

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
⊢ b ∈ s

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
⊢ b ∈ s

Tactic:
replace ha : a ∈ S := ⟨ha, left_mem_Icc.2 hab⟩

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
⊢ b ∈ s

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
⊢ b ∈ s

Tactic:
let c := sSup (s ∩ Icc a b)

Result:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
⊢ b ∈ s