awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
refine_1 :
  ∀ (u : Set α),
    Membership.mem (γ := Set (Set α))
        {s : Set α |
          ∃ (f : Set α) (g : Set α), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
        u →
      IsOpen[ts] u
refine_2 :
  Subset.{u} (α := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}})
    {s : Set α | ∃ (f : Set α) (g : Set α), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, 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:
refine IsTopologicalBasis.of_isOpen_of_subset ?_ (isTopologicalBasis_of_subbasis h) ?_

Premises used: TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset, TopologicalSpace.isTopologicalBasis_of_subbasis
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
refine_1 : IsOpen[ts] (⋂ a ∈ f, Ioi a)
refine_1₁ : IsOpen[ts] (⋂ a ∈ g, Iio a)
⊢ IsOpen[ts] ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a)

Tactic:
apply IsOpen.inter

Premises used: IsOpen.inter
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
apply : ∀ (i : α) (hi : i ∈ f), IsOpen[ts] (Ioi i)
⊢ IsOpen[ts] (⋂ a ∈ f, Ioi a)

Tactic:
apply hf_fin.isOpen_biInter (fun i hi ↦ ?_)

Premises used: Set.Finite.isOpen_biInter
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ f
rw : IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Ioi i)
⊢ IsOpen[ts] (Ioi i)

Tactic:
rw [h]
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ f
⊢ IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Ioi i)

Tactic:
isOpen_generateFrom_of_mem ⟨i, hfc hi, Or.inl rfl⟩

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem, And.intro, Exists.intro, Or.inl, rfl
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ f
⊢ IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Ioi i)

Tactic:
exact isOpen_generateFrom_of_mem ⟨i, hfc hi, Or.inl rfl⟩
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
apply : ∀ (i : α) (hi : i ∈ g), IsOpen[ts] (Iio i)
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)

Tactic:
apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)

Premises used: Set.Finite.isOpen_biInter
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ g
rw : IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Iio i)
⊢ IsOpen[ts] (Iio i)

Tactic:
rw [h]
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ g
⊢ IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Iio i)

Tactic:
isOpen_generateFrom_of_mem ⟨i, hgc hi, Or.inr rfl⟩

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem, And.intro, Exists.intro, Or.inr, rfl
-- 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}
f g : Set α
hfc : f ⊆ c
hgc : g ⊆ c
hf_fin : f.Finite
hg_fin : g.Finite
i : α
hi : i ∈ g
⊢ IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Iio i)

Tactic:
exact isOpen_generateFrom_of_mem ⟨i, hgc hi, Or.inr rfl⟩
-- 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}
refine_2 :
  ∀ (a : Set (Set α)),
    a.Finite →
      a ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a} →
        ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ a = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
⊢ Subset.{u} (α := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}})
    {s : Set α | ∃ (f : Set α) (g : Set α), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}

Tactic:
simp only [exists_and_left, image_subset_iff, preimage_setOf_eq, setOf_subset_setOf, and_imp]

Premises used: and_imp, exists_and_left, Set.preimage_setOf_eq, Set.setOf_subset_setOf, Set.image_subset_iff
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
⊢ ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a

Tactic:
have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
h₁ : ∀ (x : Set α), x ∈ k ↔ x ∈ kl ∪ kr
⊢ k = kl ∪ kr

Tactic:
ext
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
x : Set α
⊢ x ∈ k ↔ x ∈ kl ∪ kr

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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
⊢ k = kl ∪ kr

Tactic:
have k_eq : k = kl ∪ kr := by
    -- this `have` can be removed, but makes `grind` slower
    have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk
    ext
    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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
⊢ kl ⊆ k

Tactic:
simp [k_eq]
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
⊢ Finite.{u + 1} (↑kl : Type u)

Tactic:
have : Finite kl := k_fin.subset (by simp [k_eq])
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this : Finite.{u + 1} (↑kl : Type u)
⊢ kr ⊆ k

Tactic:
simp [k_eq]
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this : Finite.{u + 1} (↑kl : Type u)
⊢ Finite.{u + 1} (↑kr : Type u)

Tactic:
have : Finite kr := k_fin.subset (by simp [k_eq])
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
⊢ ∀ (s : (↑kl : Type u)), ∃ a ∈ c, (↑s : Set α) = Ioi a

Tactic:
have Al : ∀ s : kl, ∃ a ∈ c, s = Ioi a := fun s ↦ s.2.2
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
Al : ∀ (s : (↑kl : Type u)), ∃ a ∈ c, (↑s : Set α) = Ioi a
refine_2 :
  ∀ (al : (s : (↑kl : Type u)) → α) (alc : ∀ (s : (↑kl : Type u)), al s ∈ c)
    (hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)),
    ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
choose al alc hal using Al
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
⊢ ∀ (s : (↑kr : Type u)), ∃ a ∈ c, (↑s : Set α) = Iio a

Tactic:
have Ar : ∀ s : kr, ∃ a ∈ c, s = Iio a := fun s ↦ s.2.2
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
Ar : ∀ (s : (↑kr : Type u)), ∃ a ∈ c, (↑s : Set α) = Iio a
refine_2 :
  ∀ (ar : (s : (↑kr : Type u)) → α) (arc : ∀ (s : (↑kr : Type u)), ar s ∈ c)
    (har : ∀ (s : (↑kr : Type u)), (↑s : Set α) = Iio (ar s)),
    ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
choose ar arc har using Ar
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
ar : (s : (↑kr : Type u)) → α
arc : ∀ (s : (↑kr : Type u)), ar s ∈ c
har : ∀ (s : (↑kr : Type u)), (↑s : Set α) = Iio (ar s)
⊢ range al ⊆ c

Tactic:
simp [range_subset_iff, alc]

Premises used: Set.range_subset_iff
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
ar : (s : (↑kr : Type u)) → α
arc : ∀ (s : (↑kr : Type u)), ar s ∈ c
har : ∀ (s : (↑kr : Type u)), (↑s : Set α) = Iio (ar s)
⊢ range ar ⊆ c

Tactic:
simp [range_subset_iff, arc]

Premises used: Set.range_subset_iff
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
ar : (s : (↑kr : Type u)) → α
arc : ∀ (s : (↑kr : Type u)), ar s ∈ c
har : ∀ (s : (↑kr : Type u)), (↑s : Set α) = Iio (ar s)
refine_2 : ⋂₀ k = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
refine ⟨range al, by simp [range_subset_iff, alc], range ar,
    by simp [range_subset_iff, arc], finite_range _, finite_range _, ?_⟩
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
ar : (s : (↑kr : Type u)) → α
arc : ∀ (s : (↑kr : Type u)), ar s ∈ c
har : ∀ (s : (↑kr : Type u)), (↑s : Set α) = Iio (ar s)
refine_2 :
  Eq.{u + 1} (α := Set α) ((⋂ (x : (↑kl : Type u)), (↑x : Set α)) ∩ ⋂ (x : (↑kr : Type u)), (↑x : Set α))
    ((⋂ (y : (↑kl : Type u)), Ioi (al y)) ∩ ⋂ (y : (↑kr : Type u)), Iio (ar y))
⊢ ⋂₀ k = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a

Tactic:
rw [k_eq, sInter_eq_biInter, biInter_union, biInter_range, biInter_range, biInter_eq_iInter,
    biInter_eq_iInter]

Premises used: Set.biInter_union, Set.biInter_eq_iInter, Set.sInter_eq_biInter, Set.biInter_range
-- 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}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s : Set α | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this_1 : Finite.{u + 1} (↑kl : Type u)
this : Finite.{u + 1} (↑kr : Type u)
al : (s : (↑kl : Type u)) → α
alc : ∀ (s : (↑kl : Type u)), al s ∈ c
hal : ∀ (s : (↑kl : Type u)), (↑s : Set α) = Ioi (al s)
ar : (s : (↑kr : Type u)) → α
arc : ∀ (s : (↑kr : Type u)), ar s ∈ c
har : ∀ (s : (↑kr : Type u)), (↑s : Set α) = Iio (ar s)
⊢ Eq.{u + 1} (α := Set α) ((⋂ (x : (↑kl : Type u)), (↑x : Set α)) ∩ ⋂ (x : (↑kr : Type u)), (↑x : Set α))
    ((⋂ (y : (↑kl : Type u)), Ioi (al y)) ∩ ⋂ (y : (↑kr : Type u)), Iio (ar y))

Tactic:
simp [hal, har]
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f g h : β → α
b : Filter β
a : α
hg : Tendsto g b (𝓝 a)
hh : Tendsto h b (𝓝 a)
hgf : ∀ᶠ (b : β) in b, g b ≤ f b
hfh : ∀ᶠ (b : β) in b, f b ≤ h b
⊢ Tendsto f b (𝓝 a)

Tactic:
(hg.Icc hh).of_smallSets <| hgf.and hfh

Premises used: Filter.Tendsto.Icc, Filter.Eventually.and, Filter.Tendsto.of_smallSets
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f g h : β → α
b : Filter β
a : α
hg : Tendsto g b (𝓝 a)
hh : Tendsto h b (𝓝 a)
hgf : g ≤ f
hfh : f ≤ h
⊢ Tendsto f b (𝓝 a)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le' hg hh (Eventually.of_forall hgf)
    (Eventually.of_forall hfh)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
simp :
  Eq.{u + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (i : α), ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ (i : α), ⨅ (_ : a < i), 𝓟 (Iio i))
⊢ 𝓝 a = ⨅ (l : α), ⨅ (_ : l < a), ⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Ioo l u)

Tactic:
simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_Iio]

Premises used: inf_biInf, nhds_eq_order, Filter.inf_principal, Set.Ioi_inter_Iio, biInf_inf
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
⊢ Eq.{u + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (i : α), ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ (i : α), ⨅ (_ : a < i), 𝓟 (Iio i))

Tactic:
rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
simp : ∀ (i : α) (i_1 : i < a) (i_2 : α) (i_3 : a < i_2), ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2
⊢ Tendsto f x (𝓝 a)

Tactic:
simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]

Premises used: nhds_order_unbounded, 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 β
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ ∀ (i : α) (i_1 : i < a) (i_2 : α) (i_3 : a < i_2), ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2

Tactic:
fun l hl u => h l u hl

Premises used: Set.Mem, setOf, Set.Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
f : β → α
a : α
x : Filter β
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ ∀ (i : α) (i_1 : i < a) (i_2 : α) (i_3 : a < i_2), ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2

Tactic:
exact fun l hl u => h l u hl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
Ixx : α → α → Set α
inst_1 : TendstoIxxClass Ixx (𝓝 a) (𝓝 a)
inst_2 : TendstoIxxClass Ixx (𝓟 s) (𝓟 t)
⊢ TendstoIxxClass Ixx (𝓝[s] a) (𝓝[t] a)

Tactic:
Filter.tendstoIxxClass_inf

Premises used: nhdsWithin, Filter.tendstoIxxClass_inf
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
tendsto_Ixx : Tendsto (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f) (𝓝 f).smallSets
⊢ TendstoIxxClass Icc (𝓝 f) (𝓝 f)

Tactic:
constructor
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
rw : smallSets (⨅ (i : ι), comap (eval (β := α) i) (𝓝 (f i)))
| (𝓝 f).smallSets

Tactic:
rw [nhds_pi, Filter.pi]

Premises used: nhds_pi, Filter.pi
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
tendsto_Ixx :
  Tendsto (β := Set ((i : ι) → α i)) (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (smallSets (⨅ (i : ι), comap (eval (β := α) i) (𝓝 (f i))))
⊢ Tendsto (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f) (𝓝 f).smallSets

Tactic:
conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi]

Premises used: Filter.smallSets, nhds_pi, nhds, Filter.pi
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
tendsto_Ixx :
  ∀ (i : ι),
    Tendsto (image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
      (𝓝 (f i)).smallSets
⊢ Tendsto (β := Set ((i : ι) → α i)) (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (smallSets (⨅ (i : ι), comap (eval (β := α) i) (𝓝 (f i))))

Tactic:
simp only [smallSets_iInf, smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff]

Premises used: Filter.smallSets_comap_eq_comap_image, Filter.tendsto_comap_iff, Filter.smallSets_iInf, Filter.tendsto_iInf
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
i : ι
⊢ Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))

Tactic:
have : Tendsto (fun g : ∀ i, α i => g i) (𝓝 f) (𝓝 (f i)) := (continuous_apply i).tendsto f