awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
exact le_principal_iff.2 (univ_mem' h)

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.univ_mem'
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ta : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {x : β}, x < f a → ∃ b < a, x ≤ f b
H₂ : ∀ {a : α} {x : β}, f a < x → ∃ b > a, f b ≤ x
⊢ OrderTopology α

Tactic:
let _ := induced f ta
  ⟨induced_topology_eq_preorder hf (fun h _ => H₁ h) (fun h _ => H₂ h)⟩

Premises used: OrderTopology.mk, induced_topology_eq_preorder, TopologicalSpace.induced
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
ta : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H : ∀ {x y : β}, x < y → ∃ (a : α), f a ∈ Ioo x y
⊢ OrderTopology α

Tactic:
induced_orderTopology' f (hf)
    (fun xa => let ⟨b, xb, ba⟩ := H xa; ⟨b, hf.1 ba, le_of_lt xb⟩)
    fun ax => let ⟨b, ab, bx⟩ := H ax; ⟨b, hf.1 ab, le_of_lt bx⟩

Premises used: le_of_lt, Exists, induced_orderTopology', _private.0.induced_orderTopology.match_1, LE.le, GT.gt, And, _private.0.induced_orderTopology.match_2, And.intro, LT.lt, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
⊢ induced f t = Preorder.topology α

Tactic:
induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_

Premises used: StrictMono.lt_iff_lt, induced_topology_eq_preorder
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
refine_1 : ∀ {a : α} {b : β} {x : α} (h₁ : b < f a) (h₂ : ¬b < f x), ∃ y < a, b ≤ f y
refine_2 : ∀ {a : α} {b : β} {x : α} (h₁ : f a < b) (h₂ : ¬f x < b), ∃ (y : α), a < y ∧ f y ≤ b
⊢ induced f t = Preorder.topology α

Tactic:
refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a : α
b : β
x : α
h₁ : b < f a
h₂ : ¬b < f x
refine_1 : ∀ (y : α) (h₁ : f y < f a) (h₂ : ¬f y < f x), ∃ y_1 < a, f y ≤ f y_1
⊢ ∃ y < a, b ≤ f y

Tactic:
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩

Premises used: Set.mem_range_self, Set.OrdConnected.out, LT.lt.le, not_lt, And.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a x y : α
h₁ : f y < f a
h₂ : ¬f y < f x
⊢ ∃ y_1 < a, f y ≤ f y_1

Tactic:
⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Premises used: le_rfl, StrictMono.lt_iff_lt, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a x y : α
h₁ : f y < f a
h₂ : ¬f y < f x
⊢ ∃ y_1 < a, f y ≤ f y_1

Tactic:
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a : α
b : β
x : α
h₁ : f a < b
h₂ : ¬f x < b
refine_2 : ∀ (y : α) (h₁ : f a < f y) (h₂ : ¬f x < f y), ∃ (y_1 : α), a < y_1 ∧ f y_1 ≤ f y
⊢ ∃ (y : α), a < y ∧ f y ≤ b

Tactic:
rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩

Premises used: Set.mem_range_self, Set.OrdConnected.out, LT.lt.le, not_lt, And.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a x y : α
h₁ : f a < f y
h₂ : ¬f x < f y
⊢ ∃ (y_1 : α), a < y_1 ∧ f y_1 ≤ f y

Tactic:
⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩

Premises used: le_rfl, StrictMono.lt_iff_lt, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a x y : α
h₁ : f a < f y
h₂ : ¬f x < f y
⊢ ∃ (y_1 : α), a < y_1 ∧ f y_1 ≤ f y

Tactic:
exact ⟨y, hf.lt_iff_lt.1 h₁, le_rfl⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace α
h : OrderTopology α
inst_3 : TopologicalSpace β
inst_4 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
⊢ IsEmbedding f

Tactic:
⟨⟨h.1.trans <| Eq.symm <| hf.induced_topology_eq_preorder hc⟩, hf.injective⟩

Premises used: StrictMono.induced_topology_eq_preorder, StrictMono.injective, Topology.IsInducing.mk, OrderTopology.topology_eq_generate_intervals, Eq.symm, Eq.trans, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α ↪o β
hc : OrdConnected.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))
⊢ IsEmbedding.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
f.strictMono.isEmbedding_of_ordConnected hc

Premises used: OrderEmbedding.strictMono, StrictMono.isEmbedding_of_ordConnected
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
ht : t.OrdConnected
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (ht : OrdConnected.{u} (α := α) (range (ι := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))),
    OrdConnected.{u} (α := α) (range (ι := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))
⊢ OrdConnected.{u} (α := α) (range (ι := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))

Tactic:
rwa [← @Subtype.range_val _ t] at ht

Premises used: Subtype.range_val
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
rw : ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
⊢ 𝓝[≥] a = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
rw [nhdsWithin, nhds_eq_order]

Premises used: nhds_eq_order, nhdsWithin
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf ?_ inf_le_left) inf_le_right)

Premises used: inf_le_right, inf_le_inf_right, le_inf, le_antisymm, inf_le_left
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
refine : (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)

Tactic:
refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf ?_ inf_le_left) inf_le_right)

Premises used: inf_le_right, inf_le_inf_right, le_inf, le_antisymm, inf_le_left
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
⊢ (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)

Tactic:
inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, inf_le_right, le_iInf₂, LE.le.trans, Set.Ici_subset_Ioi
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
⊢ (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)

Tactic:
exact inf_le_right.trans (le_iInf₂ fun l hl => principal_mono.2 <| Ici_subset_Ioi.2 hl)

Premises used: Iff.mpr, Filter.principal_mono, inf_le_right, le_iInf₂, LE.le.trans, Set.Ici_subset_Ioi
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
ha : ∃ (u : α), a < u
⊢ 𝓝[≥] a = ⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Ico a u)

Tactic:
simp only [nhdsGE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Iio_inter_Ici]

Premises used: Filter.inf_principal, biInf_inf, nhdsGE_eq_iInf_inf_principal, Set.Iio_inter_Ici
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : ∃ (u : α), a < u
⊢ (𝓝[≥] a).HasBasis (fun (u : α) ↦ a < u) fun (u : α) ↦ Ico a u

Tactic:
nhdsGE_eq_iInf_principal ha ▸ hasBasis_biInf_principal
    (fun b hb c hc => ⟨min b c, lt_min hb hc, Ico_subset_Ico_right (min_le_left _ _),
      Ico_subset_Ico_right (min_le_right _ _)⟩) ha

Premises used: Filter.hasBasis_biInf_principal, nhdsGE_eq_iInf_principal, Eq.rec, lt_min, min_le_left, And.intro, min_le_right, Exists.intro, Set.Ico_subset_Ico_right, Eq.symm, Min.min
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
a : α
⊢ (𝓝[≥] a).HasBasis (fun (u : α) ↦ a < u) fun (u : α) ↦ Ico a u

Tactic:
nhdsGE_basis_of_exists_gt (exists_gt a)

Premises used: NoMaxOrder.exists_gt, nhdsGE_basis_of_exists_gt
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTop α
inst_3 : OrderTopology α
⊢ Eq.{u + 1} (α := Filter α) (𝓝 ⊤) (⨅ (l : α), ⨅ (_ : l < ⊤), 𝓟 (Ioi l))

Tactic:
simp [nhds_eq_order (⊤ : α)]

Premises used: nhds_eq_order, Top.top
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : OrderTopology α
inst_4 : Nontrivial α
⊢ ∃ (x : α), x < ⊤

Tactic:
have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : OrderTopology α
inst_4 : Nontrivial α
this : ∃ (x : α), x < ⊤
⊢ HasBasis (α := α) (𝓝 ⊤) (fun (a : α) ↦ a < ⊤) fun (a : α) ↦ Ioi a

Tactic:
simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsLE_basis_of_exists_lt this

Premises used: Set.Ioc_top, nhdsWithin_univ, nhdsLE_basis_of_exists_lt, Set.Iic_top
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : OrderTopology α
inst_4 : Nontrivial α
inst_5 : DenselyOrdered α
⊢ HasBasis (𝓝 ⊤) (fun (a : α) ↦ a < ⊤) Ici

Tactic:
nhds_top_basis.to_hasBasis
    (fun _a ha => let ⟨b, hab, hb⟩ := exists_between ha; ⟨b, hb, Ici_subset_Ioi.mpr hab⟩)
    fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩

Premises used: Iff.mpr, Set.Ioi, Set.Ici, Set.Ioi_subset_Ici_self, Exists, _private.0.nhds_top_basis_Ici.match_1, HasSubset.Subset, exists_between, And, And.intro, LT.lt, Exists.intro, nhds_top_basis, Top.top, Filter.HasBasis.to_hasBasis, Set.Ici_subset_Ioi
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hf : Tendsto f l (𝓝 ⊤)
hg : f ≤ᶠ[l] g
simp :
  ∀ (hf : ∀ (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i) (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, g a ∈ Ioi i
⊢ Tendsto g l (𝓝 ⊤)

Tactic:
simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢

Premises used: Filter.tendsto_principal, nhds_top_order, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
a : α
⊢ f a ∈ Ioi x → f a ≤ g a → g a ∈ Ioi x

Tactic:
lt_of_lt_of_le

Premises used: Set.Ioi, Set.Mem, setOf, lt_of_lt_of_le
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α) {x_2 : α | (fun (a : α) ↦ f a ∈ Ioi x) x_2} x_1 →
          Membership.mem (γ := Set α)
            {x_2 : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x_2 →
                Membership.mem (γ := Set α) {x_3 : α | (fun (a : α) ↦ g a ∈ Ioi x) x_3} x_2}
            x_1}
      a
h₁ h₂ : ∀ (a : α), f a ∈ Ioi x → f a ≤ g a → g a ∈ Ioi x
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x

Tactic:
filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hf : Tendsto f l (𝓝 ⊤)
hg : f ≤ g
⊢ Tendsto g l (𝓝 ⊤)

Tactic:
tendsto_nhds_top_mono hf (Eventually.of_forall hg)

Premises used: tendsto_nhds_top_mono, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a₁ a₂ : α
h : a₁ < a₂
⊢ ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂

Tactic:
let ⟨x, hx, y, hy, h⟩ := h.exists_disjoint_Iio_Ioi
  ⟨Iio x, Ioi y, isOpen_gt' _, isOpen_lt' _, hx, hy, h⟩

Premises used: Set.Ioi, Membership.mem, Exists, LT.lt.exists_disjoint_Iio_Ioi, And, isOpen_gt', _private.0.order_separated.match_1, And.intro, Exists.intro, isOpen_lt', IsOpen, Set.Iio
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
h : ∃ (l : α), l < a
⊢ ∃ l < a, Ioc l a ⊆ s

Tactic:
(nhdsLE_basis_of_exists_lt h).mem_iff.mp (nhdsWithin_le_nhds hs)

Premises used: Filter.HasBasis.mem_iff, nhdsLE_basis_of_exists_lt, nhdsWithin_le_nhds, Iff.mp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
l : α
hl : l < a
⊢ ∃ l' ∈ Ico l a, Ioc l' a ⊆ s

Tactic:
let ⟨l', hl'a, hl's⟩ := exists_Ioc_subset_of_mem_nhds hs ⟨l, hl⟩
  ⟨max l l', ⟨le_max_left _ _, max_lt hl hl'a⟩,
    (Ioc_subset_Ioc_left <| le_max_right _ _).trans hl's⟩

Premises used: le_max_right, Set.Ioc, _private.0.exists_Ioc_subset_of_mem_nhds'.match_1, Set.Ioc_subset_Ioc_left, Membership.mem, Exists, exists_Ioc_subset_of_mem_nhds, HasSubset.Subset.trans, HasSubset.Subset, max_lt, Set.Ico, And, Max.max, And.intro, Exists.intro, le_max_left
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
inl : ∀ (ha : IsMax a), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
inr : ∀ (ha : ∃ (b : α), a < b), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)

Premises used: em, Iff.mp, not_isMax_iff, Or.imp_right, IsMax
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : IsMax a
h : a ≤ a ∧ Icc a a ∈ 𝓝[≥] a ∧ Icc a a ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
use a
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : IsMax a
⊢ a ≤ a ∧ Icc a a ∈ 𝓝[≥] a ∧ Icc a a ⊆ s

Tactic:
simpa [ha.Ici_eq] using hs

Premises used: IsMax.Ici_eq
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
inr : ∀ (b : α) (hab : a < b) (hbs : Ico a b ⊆ s), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases (nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩

Premises used: Filter.HasBasis.mem_iff, nhdsGE_basis_of_exists_gt, Iff.mp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
inr : ∀ (H : Ioo a b = ∅), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
inr₁ : ∀ (c : α) (hc : c ∈ Ioo a b), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hc⟩)

Premises used: Set.eq_empty_or_nonempty, Set.Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
rw : Icc a a ∪ Ioo a b = Icc a a
rw₁ : Icc a a ∪ ∅ = Icc a a
rw₂ rw₃ : Icc a a = Icc a a
⊢ Ico a b = Icc a a

Tactic:
rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]

Premises used: le_rfl, Set.union_empty, Set.Icc_union_Ioo_eq_Ico
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ Ico a b = Icc a a

Tactic:
have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
this : Ico a b = Icc a a
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩

Premises used: le_rfl, Eq.rec, And.intro, Exists.intro, Ico_mem_nhdsGE
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
this : Ico a b = Icc a a
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
⟨c, hc.1.le, Icc_mem_nhdsGE hc.1, (Icc_subset_Ico_right hc.2).trans hbs⟩

Premises used: Icc_mem_nhdsGE, HasSubset.Subset.trans, LT.lt.le, And.right, And.left, And.intro, Exists.intro, Set.Icc_subset_Ico_right
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
c : α
hc : c ∈ Ioo a b
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
exact ⟨c, hc.1.le, Icc_mem_nhdsGE hc.1, (Icc_subset_Ico_right hc.2).trans hbs⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
rcases :
  ∀ (b : α) (hba : b ≤ a) (hb_nhds : Icc b a ∈ 𝓝[≤] a) (hbs : Icc b a ⊆ s),
    ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩

Premises used: nhdsWithin_le_nhds, exists_Icc_mem_subset_of_mem_nhdsLE
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
rcases :
  ∀ (c : α) (hac : a ≤ c) (hc_nhds : Icc a c ∈ 𝓝[≥] a) (hcs : Icc a c ⊆ s),
    ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhdsGE (nhdsWithin_le_nhds hs) with
    ⟨c, hac, hc_nhds, hcs⟩

Premises used: exists_Icc_mem_subset_of_mem_nhdsGE, nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
⟨b, c, ⟨hba, hac⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
refine : Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
refine ⟨b, c, ⟨hba, hac⟩, ?_⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
rw : Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s
⊢ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]

Premises used: Set.Icc_union_Icc_eq_Icc, nhdsLE_sup_nhdsGE
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s

Tactic:
⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩

Premises used: Set.union_subset, Filter.union_mem_sup, And.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s

Tactic:
exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
h : s.Nonempty
⊢ ∃ (x : α), x ∈ s

Tactic:
h

Premises used: Set.Nonempty