-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsClosed.Icc_subset_of_forall_exists_gt {a b : α} {s : Set α} (hs : IsClosed (s ∩ Icc a b))
    (ha : a ∈ s) (hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty) : Icc a 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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ (Icc a b ∩ Icc a y)

Tactic:
congr

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

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

Tactic:
exact
  IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx =>
    hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2

Result:
no goals

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

Tactic:
suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y by
  rw [this]
  exact IsClosed.inter hs isClosed_Icc

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

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

Tactic:
exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm

Result:
no goals

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

Tactic:
rw [this]

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

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

Tactic:
intro y hy

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

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

Tactic:
have : IsClosed (s ∩ Icc a y) := by
  suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y by
    rw [this]
    exact IsClosed.inter hs isClosed_Icc
  rw [inter_assoc]
  congr
  exact (inter_eq_self_of_subset_right <| Icc_subset_Icc_right hy.2).symm

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

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

Tactic:
rw [inter_assoc]

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

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

Tactic:
exact IsClosed.inter hs isClosed_Icc

Result:
no goals