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 α
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 : Subset.{u} (α := Set (Set α)) {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} {s : Set α | IsOpen[ts] s}
Tactic: apply le_generateFrom_iff_subset_isOpen.2
-- 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)
⊢ Subset.{u} (α := Set (Set α)) {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} {s : Set α | IsOpen[ts] s}
have inr : ∀ (a_1 x : Set α), x ∈ t → a_1 = Ioi (a x) ∨ a_1 = Iio (a x) → IsOpen[ts] a_1
Tactic: simp only [mem_image, exists_exists_and_eq_and, setOf_subset_setOf, forall_exists_index,
      and_imp]
-- 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)
⊢ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ ts
have inr : generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ generateFrom t
Tactic: rw [ht]
-- 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)
⊢ generateFrom {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1} ≤ generateFrom t
have inr : t ⊆ {s : Set α | ∃ a_1 ∈ a '' t, s = Ioi a_1 ∨ s = Iio a_1}
Tactic: apply generateFrom_anti
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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}
have 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
Tactic: refine IsTopologicalBasis.of_isOpen_of_subset ?_ (isTopologicalBasis_of_subbasis h) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ 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}
have 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}
Tactic: refine IsTopologicalBasis.of_isOpen_of_subset ?_ (isTopologicalBasis_of_subbasis h) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ IsOpen[ts] ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a)
have refine_1 : IsOpen[ts] (⋂ a ∈ f, Ioi a)
Tactic: apply IsOpen.inter
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
⊢ IsOpen[ts] ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a)
have refine_1₁ : IsOpen[ts] (⋂ a ∈ g, Iio a)
Tactic: apply IsOpen.inter
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ IsOpen[ts] (⋂ a ∈ f, Ioi a)
have apply : ∀ (i : α) (hi : i ∈ f), IsOpen[ts] (Ioi i)
Tactic: apply hf_fin.isOpen_biInter (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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[ts] (Ioi i)
have rw : IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Ioi i)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ IsOpen[ts] (⋂ a ∈ g, Iio a)
have apply : ∀ (i : α) (hi : i ∈ g), IsOpen[ts] (Iio i)
Tactic: apply hg_fin.isOpen_biInter (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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[ts] (Iio i)
have rw : IsOpen[generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}] (Iio i)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
c : Set α
h : ts = generateFrom {s : Set α | ∃ a ∈ c, s = Ioi a ∨ s = 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}
have 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
Tactic: simp only [exists_and_left, image_subset_iff, preimage_setOf_eq, setOf_subset_setOf, and_imp]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
have this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
Tactic: have : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a := hk
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ k = kl ∪ kr
have h₁ : ∀ (x : Set α), x ∈ k ↔ x ∈ kl ∪ kr
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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}
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have k_eq : 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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have this : Finite.{u + 1} (↑kl : Type u)
Tactic: have : Finite kl := k_fin.subset (by simp [k_eq])
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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)
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have this₁ : Finite.{u + 1} (↑kr : Type u)
Tactic: have : Finite kr := k_fin.subset (by simp [k_eq])
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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)
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have Al : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have 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
Tactic: choose al alc hal using Al
Cleared hypotheses: Al
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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)
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have Ar : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have 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
Tactic: choose ar arc har using Ar
Cleared hypotheses: Ar
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
have refine_2 : ⋂₀ k = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a
Tactic: refine ⟨range al, by simp [range_subset_iff, alc], range ar,
    by simp [range_subset_iff, arc], finite_range _, finite_range _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
⊢ ⋂₀ k = (⋂ a ∈ range al, Ioi a) ∩ ⋂ a ∈ range ar, Iio a
have 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))
Tactic: rw [k_eq, sInter_eq_biInter, biInter_union, biInter_range, biInter_range, biInter_eq_iInter,
    biInter_eq_iInter]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
⊢ 𝓝 a = ⨅ (l : α), ⨅ (_ : l < a), ⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Ioo l u)
have 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))
Tactic: simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_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 β
hu : ∃ (u : α), a < u
hl : ∃ (l : α), l < a
h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u
⊢ Tendsto f x (𝓝 a)
have simp : ∀ (i : α) (i_1 : i < a) (i_2 : α) (i_3 : a < i_2), ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2
Tactic: simp only [nhds_order_unbounded hu hl, tendsto_iInf, tendsto_principal]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ TendstoIxxClass Icc (𝓝 f) (𝓝 f)
have tendsto_Ixx : Tendsto (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f) (𝓝 f).smallSets
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
| (𝓝 f).smallSets
have rw : smallSets (⨅ (i : ι), comap (eval (β := α) i) (𝓝 (f i)))
Tactic: rw [nhds_pi, Filter.pi]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f) (𝓝 f).smallSets
have 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))))
Tactic: conv in (𝓝 f).smallSets => rw [nhds_pi, Filter.pi]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 (β := Set ((i : ι) → α i)) (fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (smallSets (⨅ (i : ι), comap (eval (β := α) i) (𝓝 (f i))))
have tendsto_Ixx : ∀ (i : ι),
  Tendsto (image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (𝓝 (f i)).smallSets
Tactic: simp only [smallSets_iInf, smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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 (image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (𝓝 (f i)).smallSets
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
⊢ Tendsto (image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (𝓝 (f i)).smallSets
have tendsto_Ixx : ∀ᶠ (x : ((i : ι) → α i) × ((i : ι) → α i)) in 𝓝 f ×ˢ 𝓝 f,
  Subset.{u_2} (α := Set (α i))
    ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
    (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x))
Tactic: refine (this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
⊢ ∀ᶠ (x : ((i : ι) → α i) × ((i : ι) → α i)) in 𝓝 f ×ˢ 𝓝 f,
    Subset.{u_2} (α := Set (α i))
      ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
      (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x))
have tendsto_Ixx : ∀ (a : ((i : ι) → α i) × ((i : ι) → α i)),
  Membership.mem (γ := Set (((i : ι) → α i) × ((i : ι) → α i)))
    {x : ((i : ι) → α i) × ((i : ι) → α i) |
      (fun (x : ((i : ι) → α i) × ((i : ι) → α i)) ↦
          Subset.{u_2} (α := Set (α i))
            ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
            (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x)))
        x}
    a
Tactic: filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
tendsto_Ixx :
  ∀ (a : ((i : ι) → α i) × ((i : ι) → α i)),
    Membership.mem (γ := Set (((i : ι) → α i) × ((i : ι) → α i)))
      {x : ((i : ι) → α i) × ((i : ι) → α i) |
        (fun (x : ((i : ι) → α i) × ((i : ι) → α i)) ↦
            Subset.{u_2} (α := Set (α i))
              ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
              (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x)))
          x}
      a
⊢ ∀ᶠ (x : ((i : ι) → α i) × ((i : ι) → α i)) in 𝓝 f ×ˢ 𝓝 f,
    Subset.{u_2} (α := Set (α i))
      ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
      (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x))
have tendsto_Ixx₁ : ∀ (a : ((i : ι) → α i) × ((i : ι) → α i)),
  Subset.{u_2} (α := Set (α i))
    ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) a)
    (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) a) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) a))
Tactic: filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x : TopologicalSpace α := Preorder.topology α
⊢ induced f inst_2 ≤ Preorder.topology α
have this : OrderTopology α
Tactic: have : OrderTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst_2 ≤ Preorder.topology α
have refine : ∀ (x : α), 𝓝 x ≤ 𝓝 x
Tactic: refine le_of_nhds_le_nhds fun x => ?_