awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
have 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'
Tactic: simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ TendstoIxxClass Icc (𝓝 a) (𝓝 a)
have 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 : α)))
Tactic: simp only [nhds_eq_order, iInf_subtype']
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 : α)))
have 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 : α)
Tactic: refine
    ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 : α)
have refine_1 : ∀ (i : Subtype (Membership.mem (Iio a))) (hi : i ∈ s.1), (Ioi (↑i : α)).OrdConnected
Tactic: refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∀ (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 : α)
have refine_2 : ∀ (i : Subtype (Membership.mem (Ioi a))) (hi : i ∈ s.2), (Iio (↑i : α)).OrdConnected
Tactic: refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
have inl : ∀ (hα : IsEmpty α), ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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}
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
have inr : ∀ (hα : Nonempty α), ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
Tactic: rcases isEmpty_or_nonempty α with hα | hα
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : SecondCountableTopology α
hα : Nonempty α
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
have 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}
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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
have A : ∀ s ∈ t, ∃ (a : α), s = Ioi a ∨ s = Iio a
Tactic: have A : ∀ s ∈ t, ∃ a, s = Ioi a ∨ s = Iio a := t_subs
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (c : Set α), c.Countable ∧ ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
have 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}
Tactic: choose! a ha using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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}
have inr : ts = generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
Tactic: refine ⟨a '' t, t_count.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
⊢ ts = generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
have inr : ts ≤ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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}
⊢ ts = generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
have inr₁ : generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ ts
Tactic: apply le_antisymm