awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
⊢ s ∈ 𝓝[>] z
have this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z
Tactic: have : tᶜ ∩ Ioc z y ∈ 𝓝[>] z := by
    rw [← nhdsWithin_Ioc_eq_nhdsGT hz.2]
    exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z
⊢ s ∈ 𝓝[>] z
have apply : tᶜ ∩ Ioc z y ⊆ s
Tactic: apply mem_of_superset this
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b x y : α
s t : Set α
hxy : x ≤ y
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
hx : x ∈ Icc a b ∩ s
hy : y ∈ Icc a b ∩ t
xyab : Icc x y ⊆ Icc a b
hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty
z : α
zs : z ∈ s
hz : z ∈ Ico x y
zt : z ∈ tᶜ
this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z
⊢ tᶜ ∩ Ioc z y ⊆ s
have this₁ : Ioc z y ⊆ s ∪ t
Tactic: have : Ioc z y ⊆ s ∪ t := fun w hw => hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
⊢ (Icc a b ∩ (s ∩ t)).Nonempty
have inl : ∀ (h : x ≤ y), (Icc a b ∩ (s ∩ t)).Nonempty
Tactic: rcases le_total x y with h | h
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
inl : ∀ (h : x ≤ y), (Icc a b ∩ (s ∩ t)).Nonempty
⊢ (Icc a b ∩ (s ∩ t)).Nonempty
have inr : ∀ (h : y ≤ x), (Icc a b ∩ (s ∩ t)).Nonempty
Tactic: rcases le_total x y with h | h
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (s ∩ t)).Nonempty
have inr : (Icc a b ∩ (t ∩ s)).Nonempty
Tactic: rw [inter_comm s t]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty
have inr : ∀ (hab : Icc a b ⊆ t ∪ s) (x : α) (hx : x ∈ Icc a b ∩ s) (y : α) (hy : y ∈ Icc a b ∩ t) (h : y ≤ x),
  (Icc a b ∩ (t ∩ s)).Nonempty
Tactic: rw [union_comm s t] at hab
Cleared hypotheses: hab, x, hx, y, hy, h
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
⊢ Eq (α := Set (Set α)) {s : Set α | IsPreconnected s}
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
have refine : Subset (α := Set (Set α))
  (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
    (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
  {s : Set α | IsPreconnected s}
Tactic: refine Subset.antisymm setOf_isPreconnected_subset_of_ordered ?_
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
⊢ IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
have simp : (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
Tactic: simp only [IsTotallyDisconnected, isPreconnected_iff_ordConnected, ← not_nontrivial_iff,
    nontrivial_iff_exists_lt, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
⊢ (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
have refine_1 : ∀ (h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x < y),
  ∃ z ∉ s, z ∈ Ioo x y
Tactic: refine ⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht x hx y hy hxy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
refine_1 :
  ∀ (h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s)
    (hxy : x < y), ∃ z ∉ s, z ∈ Ioo x y
⊢ (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
have refine_2 : ∀ (h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y) (t : Set α) (hts : t ⊆ s) (ht : t.OrdConnected) (x : α)
  (hx : x ∈ t) (y : α) (hy : y ∈ t) (hxy : x < y), False
Tactic: refine ⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht x hx y hy hxy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∉ s, z ∈ Ioo x y
have refine_1 : ¬(s ∩ Icc x y).OrdConnected
Tactic: simp_rw [← not_ordConnected_inter_Icc_iff hx hy]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
t : Set α
hts : t ⊆ s
ht : t.OrdConnected
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : x < y
⊢ False
have refine_2 : ∀ (z : α) (h1z : z ∉ s) (h2z : z ∈ Ioo x y), False
Tactic: obtain ⟨z, h1z, h2z⟩ := h x (hts hx) y (hts hy) hxy
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
⊢ [[f a, f b]] ⊆ f '' [[a, b]]
have inl : f a ≤ f b → [[f a, f b]] ⊆ f '' [[a, b]]
Tactic: cases le_total (f a) (f b)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
inl : f a ≤ f b → [[f a, f b]] ⊆ f '' [[a, b]]
⊢ [[f a, f b]] ⊆ f '' [[a, b]]
have inr : f b ≤ f a → [[f a, f b]] ⊆ f '' [[a, b]]
Tactic: cases le_total (f a) (f b)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ SurjOn f s [[f a, f b]]
have inl : ∀ (hab : f a ≤ f b), SurjOn f s [[f a, f b]]
Tactic: rcases le_total (f a) (f b) with hab | hab
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
s : Set α
hs : s.OrdConnected
f : α → δ
hf : ContinuousOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
inl : ∀ (hab : f a ≤ f b), SurjOn f s [[f a, f b]]
⊢ SurjOn f s [[f a, f b]]
have inr : ∀ (hab : f b ≤ f a), SurjOn f s [[f a, f b]]
Tactic: rcases le_total (f a) (f b) with hab | hab
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
⊢ f a < f b
have by_contra! : ∀ (h : f b ≤ f a), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
⊢ False
have H : f b < f a
Tactic: have H : f b < f a := lt_of_le_of_ne h <| hf_i.ne hab.ne'
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
⊢ False
have pos : ∀ (ha : f a ≤ f ⊥), False
Tactic: by_cases! ha : f a ≤ f ⊥
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
pos : ∀ (ha : f a ≤ f ⊥), False
⊢ False
have neg : ∀ (ha : f ⊥ < f a), False
Tactic: by_cases! ha : f a ≤ f ⊥
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f a ≤ f ⊥
⊢ False
have pos : ∀ (u : α) (hu : u ∈ Ioc b ⊤ ∧ f u = f ⊥), False
Tactic: obtain ⟨u, hu⟩ := intermediate_value_Ioc le_top hf_c.continuousOn ⟨H.trans_le ha, hf⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f a ≤ f ⊥
u : α
hu : u ∈ Ioc b ⊤ ∧ f u = f ⊥
⊢ False
have this : u = ⊥
Tactic: have : u = ⊥ := hf_i hu.2
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
⊢ False
have pos : ∀ (hb : f ⊥ < f b), False
Tactic: by_cases! hb : f ⊥ < f b
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
pos : ∀ (hb : f ⊥ < f b), False
⊢ False
have neg : ∀ (hb : f b ≤ f ⊥), False
Tactic: by_cases! hb : f ⊥ < f b
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
⊢ False
have pos : ∀ (u : α) (hu : u ∈ Ioo ⊥ a ∧ f u = f b), False
Tactic: obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f ⊥ < f b
u : α
hu : u ∈ Ioo ⊥ a ∧ f u = f b
⊢ False
have hu₁ : b ∈ Ioo ⊥ a ∧ f b = f b
Tactic: rw [hf_i hu.2] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b ≤ f ⊥
⊢ False
have hb₁ : f b < f ⊥
Tactic: replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b < f ⊥
⊢ False
have neg : ∀ (u : α) (hu : u ∈ Ioo a b ∧ f u = f ⊥), False
Tactic: obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
inst_7 : BoundedOrder α
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b < f ⊥
u : α
hu : u ∈ Ioo a b ∧ f u = f ⊥
⊢ False
have this : u = ⊥
Tactic: have : u = ⊥ := hf_i hu.2
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
⊢ f x < f y
have hsa : s ≤ a
Tactic: have hsa : s ≤ a := min_le_left a x
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
⊢ f x < f y
have hbt : b ≤ t
Tactic: have hbt : b ≤ t := le_max_left b y
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
have this : Fact (s ≤ t)
Tactic: have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : Fact (s ≤ t)
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
have this₁ : StrictMono ((Icc s t).restrict (π := fun (a : α) ↦ δ) f) ∨ StrictAnti ((Icc s t).restrict (π := fun (a : α) ↦ δ) f)
Tactic: have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.restrict (Icc s t) f)
      hf_c.continuousOn.restrict hf_i.injOn.injective
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
⊢ f x < f y
have hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
Tactic: have hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t) := by
    have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
    have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.restrict (Icc s t) f)
      hf_c.continuousOn.restrict hf_i.injOn.injective
    exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
⊢ False
have this : Icc a b ⊆ Icc s t
Tactic: have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : Icc a b ⊆ Icc s t
⊢ False
have this₁ : StrictAntiOn f (Icc a b)
Tactic: replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
this : StrictAntiOn f (Icc a b)
⊢ False
have this₁ : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Icc a b)
Tactic: replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst, inst_5] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
⊢ f x < f y
have this : ∀ (h : StrictAntiOn f (Icc s t)), False
Tactic: have (h : StrictAntiOn f (Icc s t)) : False := by
    have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
    replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
    replace : IsAntichain (· ≤ ·) (Icc a b) :=
      IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
    exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab