awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : αᵒᵈ
⊢ a ≤ (OrderDual.toDual : (a : α) → αᵒᵈ) (kernel (T := T) (hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)))
have obtain : ∀ (S : Set (↑T : Type u_1)),
  kernel (T := T) S ≤
    (OrderDual.toDual : (a : α) → αᵒᵈ)
      (kernel (T := T) (hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (kernel (T := T) S))))
Tactic: obtain ⟨S, rfl⟩ := hG a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ kernel (T := T) S ≤
    (OrderDual.toDual : (a : α) → αᵒᵈ)
      (kernel (T := T) (hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (kernel (T := T) S))))
have rw : sInf
    (Subtype.val (p := fun (x : α) ↦ x ∈ T) ''
      hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)))) ≤
  (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S))
Tactic: rw [OrderDual.le_toDual, kernel, kernel]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
S : Set (↑T : Type u_1)
c : (↑T : Type u_1)
hcS : c ∈ S
⊢ c ∈ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)))
have rw : (OrderDual.ofDual : (a : αᵒᵈ) → α) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ T) '' S)) ≤ (↑c : α)
Tactic: rw [hull, mem_preimage, mem_Ici]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
| a
have rw : ((OrderDual.ofDual : (a : αᵒᵈ) → α)
    ((OrderDual.toDual : (a : α) → αᵒᵈ)
        (((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ kernel (T := T)) ((hull T ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) a)) :
      αᵒᵈ) :
  α)
Tactic: rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
hG : OrderGenerates T
a : α
⊢ kernel (T := T) (hull T a) = a
have conv_rhs : kernel (T := T) (hull T a) =
  (OrderDual.ofDual : (a : αᵒᵈ) → α)
    ((OrderDual.toDual : (a : α) → αᵒᵈ)
        (((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ kernel (T := T)) ((hull T ∘ (⇑OrderDual.ofDual : (a : αᵒᵈ) → α)) a)) :
      αᵒᵈ)
Tactic: conv_rhs => rw [← OrderDual.ofDual_toDual a, ← (gi hG).l_u_eq a]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set (↑T : Type u_1)
h : IsClosed[instTopologicalSpaceSubtype] C
⊢ hull T (kernel (T := T) C) = C
have obtain : ∀ (a : α) (ha : C = hull T a), hull T (kernel (T := T) C) = C
Tactic: obtain ⟨a, ha⟩ := (isClosed_iff hT).mp h
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set (↑T : Type u_1)
h : IsClosed[instTopologicalSpaceSubtype] C
a : α
ha : C = hull T a
⊢ hull T (kernel (T := T) C) = C
have rw : hull T (kernel (T := T) (hull T a)) = hull T a
Tactic: rw [ha, kernel_hull hG]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
C : Set (↑T : Type u_1)
h : IsClosed[instTopologicalSpaceSubtype] C
a : α
ha : C = hull T a
rw : hull T (kernel (T := T) (hull T a)) = hull T a
⊢ hull T (kernel (T := T) C) = C
have rw₁ : hull T a = hull T a
Tactic: rw [ha, kernel_hull hG]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ (GaloisConnection.closureOperator (u := SetLike.coe) ⋯ : (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1)) S =
    hull T (kernel (T := T) S)
have simp : ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S) ∧
  hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
Tactic: simp only [GaloisConnection.closureOperator_apply, Closeds.coe_closure, closure, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S) ∧
    hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
have left : ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
left : ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S)
⊢ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ≤ hull T (kernel (T := T) S) ∧
    hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
have right : hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set (↑T : Type u_1)
⊢ hull T (kernel (T := T) S) ≤ ⋂₀ {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
have right : ∀ (t' : Set (↑T : Type u_1)),
  Membership.mem (γ := Set (Set (↑T : Type u_1)))
      {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} t' →
    hull T (kernel (T := T) S) ⊆ t'
Tactic: simp_rw [le_eq_subset, subset_sInter_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.HullKernel (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
T : Set α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set (↑T : Type u_1)
hR :
  Membership.mem (γ := Set (Set (↑T : Type u_1)))
    {t : Set (↑T : Type u_1) | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} R
⊢ hull T (kernel (T := T) S) ⊆ R
have right : (GaloisConnection.closureOperator (u := fun (a : αᵒᵈ) ↦ hull T ((OrderDual.ofDual : (a : αᵒᵈ) → α) a)) sorry :
      (a : Set (↑T : Type u_1)) → Set (↑T : Type u_1))
    S ⊆
  hull T (kernel (T := T) R)
Tactic: rw [← (hull_kernel_of_isClosed hT hG hR.1), ← gc_closureOperator]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
inst_4 : PreconnectedSpace X
a b : X
f g : X → α
hf : Continuous[inst, inst_2] f
hg : Continuous[inst, inst_2] g
ha : f a ≤ g a
hb : g b ≤ f b
⊢ ∃ (x : X), f x = g x
have obtain : ∀ (x : X), Membership.mem (γ := Set X) univ x → ∀ (hfg : f x ≤ g x) (hgf : g x ≤ f x), ∃ (x : X), f x = g x
Tactic: obtain ⟨x, _, hfg, hgf⟩ : (univ ∩ { x | f x ≤ g x ∧ g x ≤ f x }).Nonempty :=
    isPreconnected_closed_iff.1 PreconnectedSpace.isPreconnected_univ _ _ (isClosed_le hf hg)
      (isClosed_le hg hf) (fun _ _ => le_total _ _) ⟨a, trivial, ha⟩ ⟨b, trivial, hb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x
have hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf hg
Cleared hypotheses: hf, hg, ha', he
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
⊢ ∃ x ∈ s, f x = g x
have hg₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf hg
Cleared hypotheses: hf, hg, ha', he
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst_4 : l.NeBot
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x ∈ s, f x = g x
have obtain : ∀ (b : (↑s : Type u)) (h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b),
  ∃ x ∈ s, f x = g x
Tactic: obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
      (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x
have hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf hg
Cleared hypotheses: hf, hg, he₁, he₂
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
hf₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
⊢ ∃ x ∈ s, f x = g x
have hg₁ : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf hg
Cleared hypotheses: hf, hg, he₁, he₂
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
X : Type u
α : Type v
inst : TopologicalSpace X
inst_1 : LinearOrder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst_4 : l₁.NeBot
inst_5 : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) f)
hg : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ α) g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x
have obtain : ∀ (b : (↑s : Type u)) (h : s.restrict (π := fun (a : X) ↦ α) f b = s.restrict (π := fun (a : X) ↦ α) g b),
  ∃ x ∈ s, f x = g x
Tactic: obtain ⟨b, h⟩ :=
    @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
      (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg
      (he₁.comap _) (he₂.comap _)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s = univ
have refine : ∀ (x : α), x ∈ s
Tactic: refine eq_univ_of_forall fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
⊢ x ∈ s
have obtain : ∀ (y : α) (ys : y ∈ s) (hy : y < x), x ∈ s
Tactic: obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, y < x := not_bddBelow_iff.1 hb x
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
⊢ x ∈ s
have obtain : ∀ (z : α) (zs : z ∈ s) (hz : x < z), x ∈ s
Tactic: obtain ⟨z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : PreconnectedSpace α
x y : α
hxy : x < y
⊢ ∃ (a : α), x < a ∧ a < y
have suffices : (Iio y ∩ Ioi x).Nonempty
Tactic: suffices (Iio y ∩ Ioi x).Nonempty by grind [Set.inter_nonempty_iff_exists_left]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have inl : ∀ (hs : IsPreconnected.{u} (α := α) ∅),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}
    ∅
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
inl :
  ∀ (hs : IsPreconnected.{u} (α := α) ∅),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
        Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}
      ∅
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have inr : ∀ (hne : s.Nonempty),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have hs' : IsConnected s
Tactic: have hs' : IsConnected s := ⟨hne, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have pos : ∀ (hb : BddBelow s),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: by_cases hb : BddBelow s
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
pos :
  ∀ (hb : BddBelow s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have neg : ∀ (hb : ¬BddBelow s),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: by_cases hb : BddBelow s
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have pos : ∀ (ha : BddAbove s),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: by_cases ha : BddAbove s
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
pos :
  ∀ (ha : BddAbove s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have neg : ∀ (ha : ¬BddAbove s),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: by_cases ha : BddAbove s
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have pos : ∀ (ha : BddAbove s),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: by_cases ha : BddAbove s
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
pos :
  ∀ (ha : BddAbove s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have neg : ∀ (ha : ¬BddAbove s),
  Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
Tactic: by_cases ha : BddAbove s
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have pos : Subset (α := Set (Set α)) {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s)}
  {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
    Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
Tactic: refine mem_of_subset_of_mem ?_ <| mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset
      (hs'.Ioo_csInf_csSup_subset hb ha) (subset_Icc_csInf_csSup hb ha)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s
have neg : Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: refine Or.inr <| Or.inr <| Or.inr <| Or.inr ?_
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have neg : ∀ (hs : s = Ici (sInf s)),
  Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: rcases mem_Ici_Ioi_of_subset_of_subset (hs.Ioi_csInf_subset hb ha) fun x hx ↦
      csInf_le hb hx with hs | hs