awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
this :
  Membership.mem (γ := Filter αᵒᵈ) (𝓝[>] (toDual : (a : α) → αᵒᵈ) a : Filter αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔
    ∃ (u : αᵒᵈ),
      Membership.mem (γ := Set αᵒᵈ) (Ioi ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) u ∧
        Subset (α := Set αᵒᵈ) (Ioc ((toDual : (a : α) → αᵒᵈ) a) u : Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s : Set αᵒᵈ)
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Tactic:
simpa using this
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
h : ∃ (b : α), b < a
⊢ (𝓝[<] a).HasBasis (fun (x : α) ↦ x < a) fun (x : α) ↦ Ioo x a

Tactic:
let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsLT_iff_exists_Ioo_subset' h⟩

Premises used: _private.0.mem_nhdsLT_iff_exists_Ioo_subset.match_1, nhdsWithin, mem_nhdsLT_iff_exists_Ioo_subset', Filter.HasBasis, Filter.HasBasis.mk, LT.lt, Set.Iio, Set.Ioo
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
a : α
⊢ (𝓝[<] a).HasBasis (fun (x : α) ↦ x < a) fun (x : α) ↦ Ioo x a

Tactic:
nhdsLT_basis_of_exists_lt <| exists_lt a

Premises used: nhdsLT_basis_of_exists_lt, NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
⊢ Eq (α := Filter αᵒᵈ) (𝓝[>] (toDual : (a : α) → αᵒᵈ) a : Filter αᵒᵈ) (⊥ : Filter αᵒᵈ) ↔
    IsTop (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ∨ ∃ (b : αᵒᵈ), (toDual : (a : α) → αᵒᵈ) a ⋖ b

Tactic:
nhdsGT_eq_bot_iff (a := OrderDual.toDual a)

Premises used: nhdsGT_eq_bot_iff
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
h : α = αᵒᵈ → ∀ (x : α), x ⋖ a ↔ (toDual : (a : α) → αᵒᵈ) a ⋖ x
⊢ 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a

Tactic:
convert! (config := { preTransparency := .default })
    nhdsGT_eq_bot_iff (a := OrderDual.toDual a) using 4

Premises used: nhdsGT_eq_bot_iff
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
e_1 : α = αᵒᵈ
x : α
⊢ x ⋖ a ↔ (toDual : (a : α) → αᵒᵈ) a ⋖ x

Tactic:
ofDual_covBy_ofDual_iff

Premises used: ofDual_covBy_ofDual_iff
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
e_1 : α = αᵒᵈ
x : α
⊢ x ⋖ a ↔ (toDual : (a : α) → αᵒᵈ) a ⋖ x

Tactic:
exact ofDual_covBy_ofDual_iff

Premises used: ofDual_covBy_ofDual_iff
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[≥] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[Icc a b] a

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
rw rw₁ : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[≥] a
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a

Tactic:
rw [nhdsWithin_Icc_eq_nhdsGE hab]

Premises used: nhdsWithin_Icc_eq_nhdsGE
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a

Tactic:
tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Icc_eq_nhdsGE hab]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[≥] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[Ico a b] a

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a

Tactic:
1 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
rw rw₁ : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[≥] a
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a

Tactic:
rw [nhdsWithin_Ico_eq_nhdsGE hab]

Premises used: nhdsWithin_Ico_eq_nhdsGE
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a

Tactic:
tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ico_eq_nhdsGE hab]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
⊢ s ∈ 𝓝[≥] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
⊢ ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
⊢ s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
1 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
⊢ s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff

Premises used: Filter.HasBasis.mem_iff, nhdsGE_basis_of_exists_gt, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∃ u ∈ Ioc a b, Ico a u ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∃ u ∈ Ioc a b, Ico a u ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∀ (a_1 : ∃ u ∈ Ioi a, Ico a u ⊆ s), ∃ u ∈ Ioc a b, Ico a u ⊆ s

Tactic:
5 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ ∀ (a_1 : ∃ u ∈ Ioi a, Ico a u ⊆ s), ∃ u ∈ Ioc a b, Ico a u ⊆ s

Tactic:
tfae_have 5 → 4
  | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
      (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_5_to_4 : ∀ (a_1 : ∃ u ∈ Ioi a, Ico a u ⊆ s), ∃ u ∈ Ioc a b, Ico a u ⊆ s
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ getElem? (valid := fun (as : List Prop) (i : ℕ) ↦ i < as.length)
      [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s] 0 =
    some (s ∈ 𝓝[≥] a)

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ getElem? (valid := fun (as : List Prop) (i : ℕ) ↦ i < as.length)
      [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s] 3 =
    some (∃ u ∈ Ioc a u', Ico a u ⊆ s)

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ getElem? (valid := fun (as : List Prop) (i : ℕ) ↦ i < as.length)
      [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s] 4 =
    some (∃ u ∈ Ioi a, Ico a u ⊆ s)

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
a : α
s : Set α
⊢ s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s

Tactic:
let ⟨_, hu'⟩ := exists_gt a
  mem_nhdsGE_iff_exists_Ico_subset' hu'

Premises used: Set.Ioi, Set.Ici, nhdsWithin, Membership.mem, Exists, HasSubset.Subset, NoMaxOrder.exists_gt, Set.Ico, And, Iff, _private.0.nhdsGT_basis_of_exists_gt.match_1, mem_nhdsGE_iff_exists_Ico_subset'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
a : α
⊢ (𝓝[≥] a).HasBasis (fun (u : α) ↦ a < u) (Ico a)

Tactic:
⟨fun _ => mem_nhdsGE_iff_exists_Ico_subset⟩

Premises used: mem_nhdsGE_iff_exists_Ico_subset, Filter.HasBasis.mk
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
⊢ (𝓝[≥] a).HasBasis (fun (x : α) ↦ a < x) (Icc a)

Tactic:
(nhdsGE_basis _).to_hasBasis
    (fun _u hu ↦ (exists_between hu).imp fun _v hv ↦ hv.imp_right Icc_subset_Ico_right) fun u hu ↦
    ⟨u, hu, Ico_subset_Icc_self⟩

Premises used: Set.Ico_subset_Icc_self, exists_between, Exists.imp, And.intro, Exists.intro, nhdsGE_basis, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[≥] a ↔ ∃ (u : α), a < u ∧ Icc a u ⊆ s

Tactic:
nhdsGE_basis_Icc.mem_iff

Premises used: Filter.HasBasis.mem_iff, nhdsGE_basis_Icc
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[≤] b, s ∈ 𝓝[Icc a b] b, s ∈ 𝓝[Ioc a b] b, ∃ l ∈ Ico a b, Ioc l b ⊆ s, ∃ l ∈ Iio b, Ioc l b ⊆ s].TFAE

Tactic:
simpa using TFAE_mem_nhdsGE h.dual (ofDual ⁻¹' s)

Premises used: OrderDual.ofDual, TFAE_mem_nhdsGE, Set.preimage, LT.lt.dual, DFunLike.coe
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ getElem? (valid := fun (as : List Prop) (i : ℕ) ↦ i < as.length)
      [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s] 0 =
    some (s ∈ 𝓝[≤] a)

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ getElem? (valid := fun (as : List Prop) (i : ℕ) ↦ i < as.length)
      [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s] 3 =
    some (∃ l ∈ Ico l' a, Ioc l a ⊆ s)

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ getElem? (valid := fun (as : List Prop) (i : ℕ) ↦ i < as.length)
      [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s] 4 =
    some (∃ l ∈ Iio a, Ioc l a ⊆ s)

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
a : α
s : Set α
⊢ s ∈ 𝓝[≤] a ↔ ∃ l ∈ Iio a, Ioc l a ⊆ s

Tactic:
let ⟨_, hl'⟩ := exists_lt a
  mem_nhdsLE_iff_exists_Ioc_subset' hl'

Premises used: Set.Ioc, _private.0.mem_nhdsLT_iff_exists_Ioo_subset.match_1, nhdsWithin, Membership.mem, Exists, HasSubset.Subset, And, Iff, mem_nhdsLE_iff_exists_Ioc_subset', NoMinOrder.exists_lt, Set.Iic, Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
⊢ (∃ (u : α),
      LT.lt (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) u : αᵒᵈ) ∧
        Subset (α := Set αᵒᵈ) (Icc ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) u) : Set αᵒᵈ)
          ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s : Set αᵒᵈ)) ↔
    ∃ l < a, Icc l a ⊆ s

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
inst_4 : DenselyOrdered α
a : α
⊢ (𝓝[≤] a).HasBasis (fun (x : α) ↦ x < a) fun (x : α) ↦ Icc x a

Tactic:
⟨fun _ ↦ mem_nhdsLE_iff_exists_Icc_subset⟩

Premises used: Filter.HasBasis.mk, mem_nhdsLE_iff_exists_Icc_subset
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
simp :
  Eq.{u_1 + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1}) ⊓ ⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
⊢ 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}

Tactic:
simp only [nhds_eq_order, mabs_lt, setOf_and, ← inf_principal, iInf_inf_eq]

Premises used: Set.setOf_and, nhds_eq_order, Filter.inf_principal, mabs_lt, iInf_inf_eq
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ Eq.{u_1 + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1}) ⊓ ⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})

Tactic:
(congr_arg₂ _ ?_ ?_).trans (inf_comm ..)

Premises used: inf_comm, Eq.trans, congr_arg₂
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
refine_1 : Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Iio a, 𝓟 (Ioi b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
refine_2 : Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Ioi a, 𝓟 (Iio b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1})
⊢ Eq.{u_1 + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1}) ⊓ ⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})

Tactic:
refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)

Premises used: inf_comm, Eq.trans, congr_arg₂
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Iio a, 𝓟 (Ioi b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})

Tactic:
(Equiv.divLeft a).iInf_congr fun x => ?_

Premises used: Equiv.divLeft, Equiv.iInf_congr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
refine_1 :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := Filter α)
      (⨅ (_ : GT.gt (α := α) ((Equiv.divLeft a : (a : α) → α) x : α) (1 : α)),
        𝓟 {a_1 : α | a / a_1 < (Equiv.divLeft a : (a : α) → α) x})
      (⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x))
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Iio a, 𝓟 (Ioi b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})

Tactic:
refine (Equiv.divLeft a).iInf_congr fun x => ?_

Premises used: Equiv.divLeft, Equiv.iInf_congr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a x : α
⊢ Eq.{u_1 + 1} (α := Filter α)
    (⨅ (_ : GT.gt (α := α) ((Equiv.divLeft a : (a : α) → α) x : α) (1 : α)),
      𝓟 {a_1 : α | a / a_1 < (Equiv.divLeft a : (a : α) → α) x})
    (⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x))

Tactic:
simp [Ioi]

Premises used: Set.Ioi
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Ioi a, 𝓟 (Iio b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1})

Tactic:
(Equiv.divRight a).iInf_congr fun x => ?_

Premises used: Equiv.divRight, Equiv.iInf_congr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
refine_2 :
  ∀ (x : α),
    Eq.{u_1 + 1} (α := Filter α)
      (⨅ (_ : GT.gt (α := α) ((Equiv.divRight a : (a : α) → α) x : α) (1 : α)),
        𝓟 {a_1 : α | ((Equiv.divRight a : (a : α) → α) x)⁻¹ < a / a_1})
      (⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x))
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Ioi a, 𝓟 (Iio b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1})

Tactic:
refine (Equiv.divRight a).iInf_congr fun x => ?_

Premises used: Equiv.divRight, Equiv.iInf_congr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a x : α
⊢ Eq.{u_1 + 1} (α := Filter α)
    (⨅ (_ : GT.gt (α := α) ((Equiv.divRight a : (a : α) → α) x : α) (1 : α)),
      𝓟 {a_1 : α | ((Equiv.divRight a : (a : α) → α) x)⁻¹ < a / a_1})
    (⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x))

Tactic:
simp [Iio]

Premises used: Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
⊢ OrderTopology α

Tactic:
⟨TopologicalSpace.ext_nhds fun a => ?_⟩

Premises used: OrderTopology.mk, TopologicalSpace.ext_nhds
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
refine : ∀ (a : α), 𝓝 a = 𝓝 a
⊢ OrderTopology α

Tactic:
refine ⟨TopologicalSpace.ext_nhds fun a => ?_⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
a : α
rw : ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r} = 𝓝 a
⊢ 𝓝 a = 𝓝 a

Tactic:
rw [h_nhds]