awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.CountableSeparating
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

Tactic:
this y x ?_ hne.symm (hne.lt_or_gt.resolve_left hlt)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Topology.Order.CountableSeparating
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
exists_countable_separating : ∀ s ∈ Iio '' t, y ∈ s ↔ x ∈ s
⊢ False

Tactic:
refine this y x ?_ hne.symm (hne.lt_or_gt.resolve_left hlt)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Topology.Order.CountableSeparating
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
⊢ ∀ s ∈ Iio '' t, y ∈ s ↔ x ∈ s

Tactic:
simpa only [iff_comm] using h

Premises used: iff_comm
-- Module: Mathlib.Topology.Order.CountableSeparating
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 = ∅
⊢ ∀ ⦃c : X⦄, x < c → ¬c < y

Tactic:
simpa using Set.ext_iff.mp he

Premises used: Iff.mp, Set.ext_iff
-- Module: Mathlib.Topology.Order.CountableSeparating
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 = ∅
⊢ 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⟩))

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro, Set.Iio, Or.inr
-- Module: Mathlib.Topology.Order.CountableSeparating
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
hne : x ≠ y
hlt : x < y
he : Ioo x y = ∅
h : x ∈ Iio y ↔ y ∈ Iio y
⊢ False

Tactic:
simp [hlt.not_ge] at h

Premises used: LT.lt.not_ge
-- Module: Mathlib.Topology.Order.CountableSeparating
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
inr : ∀ (z : X) (hzs : z ∈ s) (hxz : x < z) (hzy : z < y), False
⊢ False

Tactic:
rcases hsd.inter_open_nonempty _ isOpen_Ioo hne with ⟨z, ⟨hxz, hzy⟩, hzs⟩

Premises used: isOpen_Ioo, Dense.inter_open_nonempty
-- Module: Mathlib.Topology.Order.CountableSeparating
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
z : X
hzs : z ∈ s
hxz : x < z
hzy : z < y
⊢ False

Tactic:
simpa [hxz, hzy.not_gt] using h (Iio z) (mem_image_of_mem _ (.inl hzs))

Premises used: Set.mem_image_of_mem, LT.lt.not_gt, Or.inl, Set.Iio
-- Module: Mathlib.Topology.Order.CountableSeparating
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
⊢ 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))

Premises used: Set.eq_empty_or_nonempty, Set.mem_image_of_mem, And.intro, Exists.intro, LT.lt.not_ge, Set.Iio, Set.Ioo, Or.inr
-- Module: Mathlib.Topology.Order.CountableSeparating
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 Ioi) x) s

Tactic:
.range_Iio (X := Xᵒᵈ)

Premises used: Set.Ioi, Set.Mem, setOf, HasCountableSeparatingOn.range_Iio, OrderDual
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s : Set X
t : Set (Set X)
htc : t.Countable
ht_sub : ∀ s ∈ t, Membership.mem (γ := Set (Set X)) (range Ioi) s
ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ s ∈ compl '' t, Membership.mem (γ := Set (Set X)) (range Iic) s

Tactic:
simpa [← compl_inj_iff (x := Ioi _)] using ht_sub

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
s : Set X
t : Set (Set X)
htc : t.Countable
ht_sub : ∀ s ∈ t, Membership.mem (γ := Set (Set X)) (range Ioi) s
ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ compl '' t, x ∈ s ↔ y ∈ s) → x = y

Tactic:
simpa [not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.Order.CountableSeparating
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 Ici) x) s

Tactic:
range_Iic (X := Xᵒᵈ)

Premises used: Set.Ici, Set.Mem, setOf, OrderDual, HasCountableSeparatingOn.range_Iic
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
α : Type u_2
l : Filter α
inst_4 : CountableInterFilter l
f g : α → X
h : ∀ (x : X), ∀ᶠ (a : α) in l, f a < x ↔ g a < x
⊢ f =ᶠ[l] g

Tactic:
of_forall_separating_preimage (· ∈ range Iio) <| forall_mem_range.2 <| fun x ↦ .set_eq (h x)

Premises used: Iff.mpr, Set.forall_mem_range, Filter.Eventually.set_eq, Membership.mem, Filter.EventuallyEq.of_forall_separating_preimage, Set.range, Set.Iio
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
α : Type u_2
l : Filter α
inst_4 : CountableInterFilter l
f g : α → X
h : ∀ (x : X), ∀ᶠ (a : α) in l, f a ≤ x ↔ g a ≤ x
⊢ f =ᶠ[l] g

Tactic:
of_forall_separating_preimage (· ∈ range Iic) <| forall_mem_range.2 <| fun x ↦ .set_eq (h x)

Premises used: Iff.mpr, Set.forall_mem_range, Filter.Eventually.set_eq, Membership.mem, Filter.EventuallyEq.of_forall_separating_preimage, Set.Iic, Set.range
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
α : Type u_2
l : Filter α
inst_4 : CountableInterFilter l
f g : α → X
h : ∀ (x : X), ∀ᶠ (a : α) in l, x < f a ↔ x < g a
⊢ f =ᶠ[l] g

Tactic:
of_forall_eventually_lt_iff (X := Xᵒᵈ) h

Premises used: Filter.EventuallyEq.of_forall_eventually_lt_iff, OrderDual
-- Module: Mathlib.Topology.Order.CountableSeparating
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LinearOrder X
inst_2 : OrderTopology X
inst_3 : SecondCountableTopology X
α : Type u_2
l : Filter α
inst_4 : CountableInterFilter l
f g : α → X
h : ∀ (x : X), ∀ᶠ (a : α) in l, x ≤ f a ↔ x ≤ g a
⊢ f =ᶠ[l] g

Tactic:
of_forall_eventually_le_iff (X := Xᵒᵈ) h

Premises used: Filter.EventuallyEq.of_forall_eventually_le_iff, OrderDual
-- Module: Mathlib.Topology.Order.DenselyOrdered
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
h₂ : Ici a ⊆ closure[inst] (Ioi a)
⊢ closure[inst] (Ioi a) = Ici a

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
closure_minimal Ioi_subset_Ici_self isClosed_Ici

Premises used: closure_minimal, Set.Ioi_subset_Ici_self, isClosed_Ici
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
exact closure_minimal Ioi_subset_Ici_self isClosed_Ici

Premises used: closure_minimal, Set.Ioi_subset_Ici_self, isClosed_Ici
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
h₂ : a ∈ closure[inst] (Ioi a)
⊢ Ici a ⊆ closure[inst] (Ioi a)

Tactic:
rw [← diff_subset_closure_iff, Ici_diff_Ioi_same, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, diff_subset_closure_iff, Set.Ici_diff_Ioi_same
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ a ∈ closure[inst] (Ioi a)

Tactic:
isGLB_Ioi.mem_closure h

Premises used: isGLB_Ioi, Set.Mem, IsGLB.mem_closure
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ a ∈ closure[inst] (Ioi a)

Tactic:
exact isGLB_Ioi.mem_closure h

Premises used: isGLB_Ioi, IsGLB.mem_closure
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
inst_4 : NoMaxOrder α
⊢ closure[inst] (Ioi a) = Ici a

Tactic:
closure_Ioi' nonempty_Ioi

Premises used: Set.nonempty_Ioi, closure_Ioi'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
h : (Iio a).Nonempty
⊢ closure[inst] (Iio a) = Iic a

Tactic:
closure_Ioi' (α := αᵒᵈ) h

Premises used: setOf, closure_Ioi', Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
inst_4 : NoMinOrder α
⊢ closure[inst] (Iio a) = Iic a

Tactic:
closure_Iio' nonempty_Iio

Premises used: closure_Iio', Set.nonempty_Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
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)
by_contra : ∀ (hx : ¬IsMax x), False
⊢ IsMax x

Tactic:
by_contra hx
-- Module: Mathlib.Topology.Order.DenselyOrdered
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)
hx : ¬IsMax x
⊢ False

Tactic:
(mem_closure_iff_nhds.mp (closure_Ioi' (not_isMax_iff.mp hx) ▸ self_mem_Ici) u hu).ne_empty
    (disjoint_iff.mp hd)

Premises used: mem_closure_iff_nhds, Set.Nonempty.ne_empty, disjoint_iff, Iff.mp
-- Module: Mathlib.Topology.Order.DenselyOrdered
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)
hx : ¬IsMax x
⊢ False

Tactic:
exact (mem_closure_iff_nhds.mp (closure_Ioi' (not_isMax_iff.mp hx) ▸ self_mem_Ici) u hu).ne_empty
    (disjoint_iff.mp hd)

Premises used: mem_closure_iff_nhds, Set.Nonempty.ne_empty, disjoint_iff, Iff.mp
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hd : Disjoint u (Iio x)
⊢ IsMin x

Tactic:
IsMax.of_disjoint_nhds_Ioi (α := αᵒᵈ) hu hd

Premises used: IsMax.of_disjoint_nhds_Ioi, OrderDual, IsMin
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hx : ¬IsMax x
by_contra : ∀ (h : ¬(u ∩ Ioi x).Nonempty), False
⊢ (u ∩ Ioi x).Nonempty

Tactic:
by_contra h
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hx : ¬IsMax x
h : ¬(u ∩ Ioi x).Nonempty
⊢ False

Tactic:
hx (IsMax.of_disjoint_nhds_Ioi hu (Set.disjoint_iff_inter_eq_empty.mpr
    (Set.not_nonempty_iff_eq_empty.mp h)))

Premises used: Iff.mpr, Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty, Iff.mp, IsMax.of_disjoint_nhds_Ioi
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hx : ¬IsMax x
h : ¬(u ∩ Ioi x).Nonempty
⊢ False

Tactic:
exact hx (IsMax.of_disjoint_nhds_Ioi hu (Set.disjoint_iff_inter_eq_empty.mpr
    (Set.not_nonempty_iff_eq_empty.mp h)))

Premises used: Iff.mpr, Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty, Iff.mp, IsMax.of_disjoint_nhds_Ioi
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hx : ¬IsMin x
⊢ (u ∩ Iio x).Nonempty

Tactic:
nonempty_nhds_inter_Ioi (α := αᵒᵈ) hu hx

Premises used: setOf, nonempty_nhds_inter_Ioi, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
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
h₂ : Icc a b ⊆ closure[inst] (Ioo a b)
⊢ closure[inst] (Ioo a b) = Icc a b

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
closure_minimal Ioo_subset_Icc_self isClosed_Icc

Premises used: Set.Ioo_subset_Icc_self, closure_minimal, isClosed_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
exact closure_minimal Ioo_subset_Icc_self isClosed_Icc

Premises used: Set.Ioo_subset_Icc_self, closure_minimal, isClosed_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
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)
h₃ : ∀ (hab : b < a), Icc a b ⊆ closure[inst] (Ioo a b)
⊢ Icc a b ⊆ closure[inst] (Ioo a b)

Tactic:
rcases hab.lt_or_gt with hab | hab

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : a < b
h₂ : {a, b} ⊆ closure[inst] (Ioo a b)
⊢ Icc a b ⊆ closure[inst] (Ioo a b)

Tactic:
rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le]

Premises used: diff_subset_closure_iff, LT.lt.le, Set.Icc_diff_Ioo_same
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : a < b
⊢ (Ioo a b).Nonempty

Tactic:
have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
-- Module: Mathlib.Topology.Order.DenselyOrdered
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
h₂ : a ∈ closure[inst] (Ioo a b) ∧ b ∈ closure[inst] (Ioo a b)
⊢ {a, b} ⊆ closure[inst] (Ioo a b)

Tactic:
simp only [insert_subset_iff, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Topology.Order.DenselyOrdered
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 ∈ closure[inst] (Ioo a b) ∧ b ∈ closure[inst] (Ioo a b)

Tactic:
⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩

Premises used: IsGLB.mem_closure, isGLB_Ioo, isLUB_Ioo, IsLUB.mem_closure, And.intro
-- Module: Mathlib.Topology.Order.DenselyOrdered
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 ∈ closure[inst] (Ioo a b) ∧ b ∈ closure[inst] (Ioo a b)

Tactic:
exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : b < a
h₂ : ∅ ⊆ closure[inst] (Ioo a b)
⊢ Icc a b ⊆ closure[inst] (Ioo a b)

Tactic:
rw [Icc_eq_empty_of_lt hab]

Premises used: Set.Icc_eq_empty_of_lt
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure[inst] (Ioo a b)

Tactic:
empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab_1 : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure[inst] (Ioo a b)

Tactic:
exact empty_subset _

Premises used: Set.empty_subset
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst] (uIoo a b) = uIcc a b

Tactic:
simp [uIoo, uIcc, hab]

Premises used: Set.uIoo, Set.uIcc
-- Module: Mathlib.Topology.Order.DenselyOrdered
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
h₂ : Icc a b ⊆ closure[inst] (Ioc a b)
⊢ closure[inst] (Ioc a b) = Icc a b

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
closure_minimal Ioc_subset_Icc_self isClosed_Icc

Premises used: closure_minimal, Set.Ioc_subset_Icc_self, isClosed_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
exact closure_minimal Ioc_subset_Icc_self isClosed_Icc

Premises used: closure_minimal, Set.Ioc_subset_Icc_self, isClosed_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
apply : Icc a b ⊆ closure[inst] (Ioo a b)
⊢ Icc a b ⊆ closure[inst] (Ioc a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)

Premises used: Set.Subset.trans, closure_mono, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
rw rw₁ : Icc a b ⊆ Icc a b
⊢ Icc a b ⊆ closure[inst] (Ioo a b)

Tactic:
rw [closure_Ioo hab]

Premises used: closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst] (uIoc a b) = uIcc a b

Tactic:
simp [uIoc, uIcc, hab]

Premises used: Set.uIoc, Set.uIcc
-- Module: Mathlib.Topology.Order.DenselyOrdered
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
h₂ : Icc a b ⊆ closure[inst] (Ico a b)
⊢ closure[inst] (Ico a b) = Icc a b

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
closure_minimal Ico_subset_Icc_self isClosed_Icc

Premises used: Set.Ico_subset_Icc_self, closure_minimal, isClosed_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
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

Tactic:
exact closure_minimal Ico_subset_Icc_self isClosed_Icc

Premises used: Set.Ico_subset_Icc_self, closure_minimal, isClosed_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
hab : a ≠ b
apply : Icc a b ⊆ closure[inst] (Ioo a b)
⊢ Icc a b ⊆ closure[inst] (Ico a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)

Premises used: Set.Subset.trans, closure_mono, Set.Ioo_subset_Ico_self
-- Module: Mathlib.Topology.Order.DenselyOrdered
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
rw₃ rw₄ : Ioi a = Ioi a
⊢ interior (Ici a) = Ioi a

Tactic:
rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]

Premises used: closure_Iio', Set.compl_Iic, Set.compl_Iio, interior_compl
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a : α
⊢ interior (Ici a) = Ioi a

Tactic:
interior_Ici' nonempty_Iio

Premises used: Set.nonempty_Iio, interior_Ici'