awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : TopologicalSpace β
f : β → α
simp_rw :
  (∀ (s : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s → IsOpen[inst_2] (f ⁻¹' s)) ↔
    ∀ (a : α), IsOpen[inst_2] (f ⁻¹' Ioi a) ∧ IsOpen[inst_2] (f ⁻¹' Iio a)
⊢ Continuous[inst_2, ts] f ↔ ∀ (a : α), IsOpen[inst_2] (f ⁻¹' Ioi a) ∧ IsOpen[inst_2] (f ⁻¹' Iio a)

Tactic:
simp_rw +instances [OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff]

Premises used: OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : TopologicalSpace β
f : β → α
⊢ (∀ (s : Set α),
      Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s → IsOpen[inst_2] (f ⁻¹' s)) ↔
    ∀ (a : α), IsOpen[inst_2] (f ⁻¹' Ioi a) ∧ IsOpen[inst_2] (f ⁻¹' Iio a)

Tactic:
aesop
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
s : Set α
rw : IsOpen[Preorder.topology α] s ↔ GenerateOpen {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s
⊢ IsOpen[ts] s ↔ GenerateOpen {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s

Tactic:
rw [t.topology_eq_generate_intervals]

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[Preorder.topology α] s ↔ GenerateOpen {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s

Tactic:
rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ IsOpen[ts] {b : α | a < b}

Tactic:
isOpen_iff_generate_intervals.2 <| .basic _ ⟨a, .inl rfl⟩

Premises used: Iff.mpr, TopologicalSpace.GenerateOpen.basic, isOpen_iff_generate_intervals, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ IsOpen[ts] (Ioi a)

Tactic:
isOpen_lt' a

Premises used: Set.Ioi, isOpen_lt'
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a b : α
h : a < b
⊢ ∀ᶠ (x : α) in 𝓝 b, a < x

Tactic:
(isOpen_lt' _).mem_nhds h

Premises used: Set.Mem, Filter.Eventually, setOf, IsOpen.mem_nhds, isOpen_lt'
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a b : α
h : a < b
⊢ ∀ᶠ (x : α) in 𝓝 b, a ≤ x

Tactic:
(lt_mem_nhds h).mono fun _ => le_of_lt

Premises used: le_of_lt, Filter.Eventually.mono, lt_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
rw :
  Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      ⨅ (_ :
        Membership.mem (γ := Set (Set α))
          {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
        𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
⊢ 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]

Premises used: TopologicalSpace.nhds_generateFrom, OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
simp_rw :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : a ∈ s ∧ ∃ (a : α), s = Ioi a ∨ s = Iio a), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₁ :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : (∃ (a : α), s = Ioi a ∨ s = Iio a) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₂ :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : ((∃ (x : α), s = Ioi x) ∨ ∃ (x : α), s = Iio x) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₃ :
  Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α), ⨅ (_ : (∃ (x : α), s = Ioi x) ∧ a ∈ s ∨ (∃ (x : α), s = Iio x) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₄ :
  Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α), (⨅ (_ : (∃ (x : α), s = Ioi x) ∧ a ∈ s), 𝓟 s) ⊓ ⨅ (_ : (∃ (x : α), s = Iio x) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₅ :
  Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      (⨅ (_ : ∃ (x : α), s = Ioi x), ⨅ (_ : a ∈ s), 𝓟 s) ⊓ ⨅ (_ : ∃ (x : α), s = Iio x), ⨅ (_ : a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₆ :
  Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      (⨅ (i : α), ⨅ (_ : s = Ioi i), ⨅ (_ : a ∈ s), 𝓟 s) ⊓ ⨅ (i : α), ⨅ (_ : s = Iio i), ⨅ (_ : a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₇ :
  Eq.{u + 1} (α := Filter α)
    ((⨅ (x : Set α), ⨅ (i : α), ⨅ (_ : x = Ioi i), ⨅ (_ : a ∈ x), 𝓟 x) ⊓
      ⨅ (x : Set α), ⨅ (i : α), ⨅ (_ : x = Iio i), ⨅ (_ : a ∈ x), 𝓟 x)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₈ :
  Eq.{u + 1} (α := Filter α)
    ((⨅ (j : α), ⨅ (i : Set α), ⨅ (_ : i = Ioi j), ⨅ (_ : a ∈ i), 𝓟 i) ⊓
      ⨅ (j : α), ⨅ (i : Set α), ⨅ (_ : i = Iio j), ⨅ (_ : a ∈ i), 𝓟 i)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₉ :
  Eq.{u + 1} (α := Filter α) ((⨅ (j : α), ⨅ (_ : a ∈ Ioi j), 𝓟 (Ioi j)) ⊓ ⨅ (j : α), ⨅ (_ : a ∈ Iio j), 𝓟 (Iio j))
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₁₀ :
  Eq.{u + 1} (α := Filter α) ((⨅ (j : α), ⨅ (_ : j < a), 𝓟 (Ioi j)) ⊓ ⨅ (j : α), ⨅ (_ : a ∈ Iio j), 𝓟 (Iio j))
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ (b : α), ⨅ (_ : a < b), 𝓟 (Iio b))
⊢ Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      ⨅ (_ :
        Membership.mem (γ := Set (Set α))
          {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
        𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))

Tactic:
simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]

Premises used: exists_or, Set.mem_Iio, Set.mem_Ioi, Set.mem_setOf_eq, and_comm, iInf_and, iInf_iInf_eq_left, iInf_comm, iInf_or, or_and_right, iInf_exists, iInf_inf_eq
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f : β → α
a : α
x : Filter β
simp :
  ((∀ (i : α) (i_1 : i ∈ Iio a), ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧
      ∀ (i : α) (i_1 : i ∈ Ioi a), ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
⊢ Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Tactic:
simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]

Premises used: Filter.tendsto_inf, nhds_eq_order, Filter.tendsto_principal, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ (i : α) (i_1 : i ∈ Iio a), ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧
      ∀ (i : α) (i_1 : i ∈ Ioi a), ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Tactic:
rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
simp :
  TendstoIxxClass.{u} (α := α) Icc
    ((⨅ (x : Subtype (Membership.mem (Iio a))), 𝓟 (Ioi (↑x : α))) ⊓
      ⨅ (x : Subtype (Membership.mem (Ioi a))), 𝓟 (Iio (↑x : α)))
    ((⨅ (x : Subtype (Membership.mem (Iio a))), 𝓟 (Ioi (↑x : α))) ⊓
      ⨅ (x : Subtype (Membership.mem (Ioi a))), 𝓟 (Iio (↑x : α)))
⊢ TendstoIxxClass Icc (𝓝 a) (𝓝 a)

Tactic:
simp only [nhds_eq_order, iInf_subtype']

Premises used: nhds_eq_order, iInf_subtype'
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ TendstoIxxClass.{u} (α := α) Icc
    ((⨅ (x : Subtype (Membership.mem (Iio a))), 𝓟 (Ioi (↑x : α))) ⊓
      ⨅ (x : Subtype (Membership.mem (Ioi a))), 𝓟 (Iio (↑x : α)))
    ((⨅ (x : Subtype (Membership.mem (Iio a))), 𝓟 (Ioi (↑x : α))) ⊓
      ⨅ (x : Subtype (Membership.mem (Ioi a))), 𝓟 (Iio (↑x : α)))

Tactic:
((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_

Premises used: Filter.HasBasis.inf, Set.Mem, Filter.HasBasis.tendstoIxxClass, setOf, Filter.hasBasis_iInf_principal_finite
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
fun :
  ∀ (s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))),
    s.1.Finite ∧ s.2.Finite →
      ∀ (x : α),
        Membership.mem (γ := Set α) ((⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)) x →
          ∀ (y : α),
            Membership.mem (γ := Set α) ((⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)) y →
              Icc x y ⊆ (⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)
⊢ TendstoIxxClass.{u} (α := α) Icc
    ((⨅ (x : Subtype (Membership.mem (Iio a))), 𝓟 (Ioi (↑x : α))) ⊓
      ⨅ (x : Subtype (Membership.mem (Ioi a))), 𝓟 (Iio (↑x : α)))
    ((⨅ (x : Subtype (Membership.mem (Iio a))), 𝓟 (Ioi (↑x : α))) ⊓
      ⨅ (x : Subtype (Membership.mem (Ioi a))), 𝓟 (Iio (↑x : α)))

Tactic:
refine
    ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_

Premises used: Filter.HasBasis.inf, Filter.HasBasis.tendstoIxxClass, Filter.hasBasis_iInf_principal_finite
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
⊢ ∀ (x : α),
    Membership.mem (γ := Set α) ((⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)) x →
      ∀ (y : α),
        Membership.mem (γ := Set α) ((⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)) y →
          Icc x y ⊆ (⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)

Tactic:
((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out

Premises used: Set.OrdConnected.out, Set.ordConnected_biInter, Set.OrdConnected.inter
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
refine_1 : ∀ (i : Subtype (Membership.mem (Iio a))) (hi : i ∈ s.1), (Ioi (↑i : α)).OrdConnected
refine_2 : ∀ (i : Subtype (Membership.mem (Ioi a))) (hi : i ∈ s.2), (Iio (↑i : α)).OrdConnected
⊢ ∀ (x : α),
    Membership.mem (γ := Set α) ((⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)) x →
      ∀ (y : α),
        Membership.mem (γ := Set α) ((⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)) y →
          Icc x y ⊆ (⋂ i ∈ s.1, Ioi (↑i : α)) ∩ ⋂ i ∈ s.2, Iio (↑i : α)

Tactic:
refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out

Premises used: Set.OrdConnected.out, Set.ordConnected_biInter, Set.OrdConnected.inter
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
i : Subtype (Membership.mem (Iio a))
refine_1 : i ∈ s.1 → (Ioi (↑i : α)).OrdConnected
⊢ ∀ (hi : i ∈ s.1), (Ioi (↑i : α)).OrdConnected

Tactic:
_
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
i : Subtype (Membership.mem (Ioi a))
refine_2 : i ∈ s.2 → (Iio (↑i : α)).OrdConnected
⊢ ∀ (hi : i ∈ s.2), (Iio (↑i : α)).OrdConnected

Tactic:
_
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
i : Subtype (Membership.mem (Iio a))
hi : i ∈ s.1
⊢ (Ioi (↑i : α)).OrdConnected

Tactic:
ordConnected_Ioi

Premises used: Set.ordConnected_Ioi
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
i : Subtype (Membership.mem (Ioi a))
hi : i ∈ s.2
⊢ (Iio (↑i : α)).OrdConnected

Tactic:
ordConnected_Iio

Premises used: Set.ordConnected_Iio
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
h : s.1.Finite ∧ s.2.Finite
i : Subtype (Membership.mem (Iio a))
hi : i ∈ s.1
⊢ (Ioi (↑i : α)).OrdConnected

Tactic:
exacts [ordConnected_Ioi, ordConnected_Iio]

Premises used: Set.ordConnected_Ioi, Set.ordConnected_Iio
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ TendstoIxxClass Ico (𝓝 a) (𝓝 a)

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ TendstoIxxClass Ioc (𝓝 a) (𝓝 a)

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ TendstoIxxClass Ioo (𝓝 a) (𝓝 a)

Tactic:
tendstoIxxClass_of_subset fun _ _ => Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, Filter.tendstoIxxClass_of_subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
inl : ∀ (hα : IsEmpty α), ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
inr : ∀ (hα : Nonempty α), ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : IsEmpty α
⊢ Set.Countable.{u} (α := α) ∅

Tactic:
simp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : IsEmpty α
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
exact ⟨∅, by simp, Subsingleton.elim _ _⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
⊢ ∃ t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}, t.Countable ∧ ts = generateFrom t

Tactic:
exists_countable_of_generateFrom OrderTopology.topology_eq_generate_intervals

Premises used: TopologicalSpace.exists_countable_of_generateFrom, OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
inr :
  ∀ (t : Set (Set α)) (t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}) (t_count : t.Countable)
    (ht : ts = generateFrom t),
    ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
obtain ⟨t, t_subs, t_count, ht⟩ : ∃ t ⊆ { s | ∃ a, s = Ioi a ∨ s = Iio a },
      t.Countable ∧ ts = generateFrom t :=
    exists_countable_of_generateFrom OrderTopology.topology_eq_generate_intervals

Premises used: TopologicalSpace.exists_countable_of_generateFrom, OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
⊢ ∀ s ∈ t, ∃ (a : α), s = Ioi a ∨ s = Iio a

Tactic:
have A : ∀ s ∈ t, ∃ a, s = Ioi a ∨ s = Iio a := t_subs
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
A : ∀ s ∈ t, ∃ (a : α), s = Ioi a ∨ s = Iio a
inr :
  ∀ (a : (s : Set α) → α) (ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)),
    ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
choose! a ha using A
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
⟨a '' t, t_count.image _, ?_⟩

Premises used: Set.Countable.image, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
inr : ts = generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
refine ⟨a '' t, t_count.image _, ?_⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
inr : ts ≤ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
inr₁ : generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ ts
⊢ ts = generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
inr : Subset.{u} (α := Set (Set α)) {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} {s : Set α | IsOpen[ts] s}
⊢ ts ≤ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Premises used: Iff.mpr, TopologicalSpace.le_generateFrom_iff_subset_isOpen
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
inr : ∀ (a_1 x : Set α), x ∈ t → a_1 = Ioi (a x) ∨ a_1 = Iio (a x) → IsOpen[ts] a_1
⊢ Subset.{u} (α := Set (Set α)) {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} {s : Set α | IsOpen[ts] s}

Tactic:
simp only [mem_image, exists_exists_and_eq_and, setOf_subset_setOf, forall_exists_index,
      and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, exists_exists_and_eq_and, Set.setOf_subset_setOf
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ ∀ (a_1 x : Set α), x ∈ t → a_1 = Ioi (a x) ∨ a_1 = Iio (a x) → IsOpen[ts] a_1

Tactic:
grind [isOpen_Iio', isOpen_Ioi']

Premises used: isOpen_Iio', isOpen_Ioi'
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
inr : generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ generateFrom t
⊢ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ ts

Tactic:
rw [ht]
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
inr : t ⊆ {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
⊢ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ generateFrom t

Tactic:
apply generateFrom_anti

Premises used: TopologicalSpace.generateFrom_anti
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
t : Set (Set α)
t_subs : t ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
t_count : t.Countable
ht : ts = generateFrom t
a : (s : Set α) → α
ha : ∀ s ∈ t, s = Ioi (a s) ∨ s = Iio (a s)
⊢ t ⊆ {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}

Tactic:
grind
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
c : Set α
h : ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ IsTopologicalBasis.{u} (α := α)
    {s : Set α | ∃ (f : Set α) (g : Set α), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}

Tactic:
IsTopologicalBasis.of_isOpen_of_subset ?_ (isTopologicalBasis_of_subbasis h) ?_

Premises used: TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset, TopologicalSpace.isTopologicalBasis_of_subbasis