awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
have refine_1 : BddBelow (f '' [[a, b]])
Tactic: refine csInf_le_csSup (nonempty_uIcc.image _) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
refine_1 : BddBelow (f '' [[a, b]])
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
have refine_2 : BddAbove (f '' [[a, b]])
Tactic: refine csInf_le_csSup (nonempty_uIcc.image _) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])
have refine_1 : BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Tactic: rw [h.image_uIcc_eq_Icc]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])
have refine_2 : BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
Tactic: rw [h.image_uIcc_eq_Icc]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ sInf (f '' Icc a b) ≤ f c
have this : f c ∈ f '' Icc a b
Tactic: have := mem_image_of_mem f hc
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ sInf (f '' Icc a b) ≤ f c
have this₁ : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
Tactic: rw [h.image_Icc (hc.1.trans hc.2)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ f c ≤ sSup (f '' Icc a b)
have this : f c ∈ f '' Icc a b
Tactic: have := mem_image_of_mem f hc
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ≤ sSup (f '' Icc a b)
have this₁ : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
Tactic: rw [h.image_Icc (hc.1.trans hc.2)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
⊢ f '' Icc a b = Icc (f a) (f b)
have rw : Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b)) = Icc (f a) (f b)
Tactic: rw [h.image_Icc hab]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
⊢ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b)) = Icc (f a) (f b)
have h₁ : sInf (f '' Icc a b) = f a
Tactic: congr!
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : MonotoneOn f (Icc a b)
h₁ : sInf (f '' Icc a b) = f a
⊢ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b)) = Icc (f a) (f b)
have h₂ : sSup (f '' Icc a b) = f b
Tactic: congr!
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
⊢ Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
have rw : Icc (f b) (f a) = (⇑ofDual : (a : βᵒᵈ) → β) ⁻¹' Icc (f b) (f a)
Tactic: rw [Icc_toDual]
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
⊢ f '' Icc a b = Icc (f b) (f a)
have this : Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
Tactic: have : Icc (f b) (f a) = Icc (toDual (f a)) (toDual (f b)) := by rw [Icc_toDual]; rfl
-- Lean 4 proof step from Mathlib.Topology.Order.Compact (goal)
Goal:
α : Type u_2
β : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : DenselyOrdered α
inst_5 : ConditionallyCompleteLinearOrder β
inst_6 : OrderTopology β
f : α → β
a b : α
hab : a ≤ b
h : ContinuousOn f (Icc a b)
h' : AntitoneOn f (Icc a b)
this : Icc (f b) (f a) = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
⊢ f '' Icc a b = Icc (f b) (f a)
have rw : f '' Icc a b = Icc ((toDual : (a : β) → βᵒᵈ) (f a)) ((toDual : (a : β) → βᵒᵈ) (f b))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s : Set X
⊢ HasCountableSeparatingOn X (fun (x : Set X) ↦ Membership.mem (γ := Set (Set X)) (range Iio) x) s
have exists_countable_separating : ∃ (S : Set (Set X)),
  S.Countable ∧
    (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s : Set X
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
have exists_countable_separating : ∀ (s_1 : Set X) (hsc : s_1.Countable) (hsd : Dense s_1),
  ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
Tactic: rcases TopologicalSpace.exists_countable_dense X with ⟨s, hsc, hsd⟩
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧
        ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
have exists_countable_separating : t.Countable
Tactic: refine ⟨Iio '' t, .image ?_ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
exists_countable_separating : t.Countable
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧
        ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
have exists_countable_separating₁ : ∀ s ∈ Iio '' t, Membership.mem (γ := Set (Set X)) (range Iio) s
Tactic: refine ⟨Iio '' t, .image ?_ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
exists_countable_separating : t.Countable
exists_countable_separating₁ : ∀ s ∈ Iio '' t, Membership.mem (γ := Set (Set X)) (range Iio) s
⊢ ∃ (S : Set (Set X)),
    S.Countable ∧
      (∀ s ∈ S, Membership.mem (γ := Set (Set X)) (range Iio) s) ∧
        ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
have exists_countable_separating₂ : ∀ x ∈ s_1, ∀ y ∈ s_1, (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x = y
Tactic: refine ⟨Iio '' t, .image ?_ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
⊢ x = y
have exists_countable_separating : ∀ (hne : x ≠ y), False
Tactic: by_contra! hne
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
⊢ False
have exists_countable_separating : ∀ (this : ∀ (x y : X) (h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) (hne : x ≠ y) (hlt : x < y), False) (hlt : ¬x < y), False
Tactic: wlog hlt : x < y generalizing x y
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
exists_countable_separating :
  ∀ (this : ∀ (x y : X) (h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) (hne : x ≠ y) (hlt : x < y), False) (hlt : ¬x < y), False
⊢ False
have wlog : ∀ (x y : X) (h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) (hne : x ≠ y) (hlt : x < y), False
Tactic: wlog hlt : x < y generalizing x y
Cleared hypotheses: x, y, h, hne
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X) (h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) (hne : x ≠ y) (hlt : x < y), False
hlt : ¬x < y
⊢ False
have exists_countable_separating : ∀ s ∈ Iio '' t, y ∈ s ↔ x ∈ s
Tactic: refine this y x ?_ hne.symm (hne.lt_or_gt.resolve_left hlt)
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
he : Ioo x y = ∅
⊢ False
have h₁ : x ∈ Iio y ↔ y ∈ Iio y
Tactic: specialize h (Iio y) (mem_image_of_mem _ (.inr ⟨x, hlt, by simpa using Set.ext_iff.mp he⟩))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne_1 : x ≠ y
hlt : x < y
hne : (Ioo x y).Nonempty
⊢ False
have inr : ∀ (z : X) (hzs : z ∈ s) (hxz : x < z) (hzy : z < y), False
Tactic: rcases hsd.inter_open_nonempty _ isOpen_Ioo hne with ⟨z, ⟨hxz, hzy⟩, hzs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.CountableSeparating (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s_1 s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x : X | ∃ (y : X), y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
⊢ False
have x₁ : Ioo x y = ∅ ∨ (Ioo x y).Nonempty
Tactic: cases (Ioo x y).eq_empty_or_nonempty with
    | inl he =>
      specialize h (Iio y) (mem_image_of_mem _ (.inr ⟨x, hlt, by simpa using Set.ext_iff.mp he⟩))
      simp [hlt.not_ge] at h
    | inr hne =>
      rcases hsd.inter_open_nonempty _ isOpen_Ioo hne with ⟨z, ⟨hxz, hzy⟩, hzs⟩
      simpa [hxz, hzy.not_gt] using h (Iio z) (mem_image_of_mem _ (.inl hzs))
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ closure[inst] (Ioi a) = Ici a
have h₁ : closure[inst] (Ioi a) ⊆ Ici a
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
h₁ : closure[inst] (Ioi a) ⊆ Ici a
⊢ closure[inst] (Ioi a) = Ici a
have h₂ : Ici a ⊆ closure[inst] (Ioi a)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure[inst] (Ioi a)
have h₂ : a ∈ closure[inst] (Ioi a)
Tactic: rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hd : Disjoint u (Ioi x)
⊢ IsMax x
have by_contra : ∀ (hx : ¬IsMax x), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hx : ¬IsMax x
⊢ (u ∩ Ioi x).Nonempty
have by_contra : ∀ (h : ¬(u ∩ Ioi x).Nonempty), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst] (Ioo a b) = Icc a b
have h₁ : closure[inst] (Ioo a b) ⊆ Icc a b
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
h₁ : closure[inst] (Ioo a b) ⊆ Icc a b
⊢ closure[inst] (Ioo a b) = Icc a b
have h₂ : Icc a b ⊆ closure[inst] (Ioo a b)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst] (Ioo a b)
have h₂ : ∀ (hab : a < b), Icc a b ⊆ closure[inst] (Ioo a b)
Tactic: rcases hab.lt_or_gt with hab | hab
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
h₂ : ∀ (hab : a < b), Icc a b ⊆ closure[inst] (Ioo a b)
⊢ Icc a b ⊆ closure[inst] (Ioo a b)
have h₃ : ∀ (hab : b < a), Icc a b ⊆ closure[inst] (Ioo a b)
Tactic: rcases hab.lt_or_gt with hab | hab
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : a < b
⊢ Icc a b ⊆ closure[inst] (Ioo a b)
have h₂ : {a, b} ⊆ closure[inst] (Ioo a b)
Tactic: rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : a < b
⊢ {a, b} ⊆ closure[inst] (Ioo a b)
have hab' : (Ioo a b).Nonempty
Tactic: have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : a < b
hab' : (Ioo a b).Nonempty
⊢ {a, b} ⊆ closure[inst] (Ioo a b)
have h₂ : a ∈ closure[inst] (Ioo a b) ∧ b ∈ closure[inst] (Ioo a b)
Tactic: simp only [insert_subset_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : b < a
⊢ Icc a b ⊆ closure[inst] (Ioo a b)
have h₂ : ∅ ⊆ closure[inst] (Ioo a b)
Tactic: rw [Icc_eq_empty_of_lt hab]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst] (Ioc a b) = Icc a b
have h₁ : closure[inst] (Ioc a b) ⊆ Icc a b
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
h₁ : closure[inst] (Ioc a b) ⊆ Icc a b
⊢ closure[inst] (Ioc a b) = Icc a b
have h₂ : Icc a b ⊆ closure[inst] (Ioc a b)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst] (Ioc a b)
have apply : Icc a b ⊆ closure[inst] (Ioo a b)
Tactic: apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst] (Ioo a b)
have rw : Icc a b ⊆ Icc a b
Tactic: rw [closure_Ioo hab]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst] (Ico a b) = Icc a b
have h₁ : closure[inst] (Ico a b) ⊆ Icc a b
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
h₁ : closure[inst] (Ico a b) ⊆ Icc a b
⊢ closure[inst] (Ico a b) = Icc a b
have h₂ : Icc a b ⊆ closure[inst] (Ico a b)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst] (Ico a b)
have apply : Icc a b ⊆ closure[inst] (Ioo a b)
Tactic: apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ interior (Ici a) = Ioi a
have rw : interior (Iio a)ᶜ = Ioi a
Tactic: rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
rw : interior (Iio a)ᶜ = Ioi a
⊢ interior (Ici a) = Ioi a
have rw₁ : (closure[inst] (Iio a))ᶜ = Ioi a
Tactic: rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
rw : interior (Iio a)ᶜ = Ioi a
rw₁ : (closure[inst] (Iio a))ᶜ = Ioi a
⊢ interior (Ici a) = Ioi a
have rw₂ : (Iic a)ᶜ = Ioi a
Tactic: rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
rw : interior (Iio a)ᶜ = Ioi a
rw₁ : (closure[inst] (Iio a))ᶜ = Ioi a
rw₂ : (Iic a)ᶜ = Ioi a
⊢ interior (Ici a) = Ioi a
have rw₃ : Ioi a = Ioi a
Tactic: rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
a b : α
⊢ interior (Icc a b) = Ioo a b
have rw : interior (Ici a ∩ Iic b) = Ioo a b
Tactic: rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
a b : α
rw : interior (Ici a ∩ Iic b) = Ioo a b
⊢ interior (Icc a b) = Ioo a b
have rw₁ : interior (Ici a) ∩ interior (Iic b) = Ioo a b
Tactic: rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]