awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : 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}
h_basis : IsTopologicalBasis basis
a : WithTop ι
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio a)
have inr : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)
Tactic: induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
      -- sets containing it and contained in `Iio a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : 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}
h_basis : IsTopologicalBasis basis
a : WithTop ι
inr : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio a)
have inr₁ : ∀ (a : ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑a : WithTop ι))
Tactic: induction a with
    | top =>
      -- for `a = ⊤`, this is trivial as `Iio ⊤` is in our set by design
      apply isOpen_generateFrom_of_mem
      exact ⟨⊤, by simp [d]⟩
    | coe a =>
      -- for `a : ι`, we consider an element `b ∈ Iio a`, and seek a finite intersection of our
      -- sets containing it and contained in `Iio a`.
      rw [@isOpen_iff_forall_mem_open]
      intro b hb
      induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
⊢ Topology.IsEmbedding.{u_1, u_1} (X := ι) some
have refine : OrdConnected.{u_1} (α := WithTop ι) (range fun (a : ι) ↦ (↑a : WithTop ι))
Tactic: refine WithTop.coe_strictMono.isEmbedding_of_ordConnected (α := ι) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
⊢ OrdConnected.{u_1} (α := WithTop ι) (range fun (a : ι) ↦ (↑a : WithTop ι))
have rw : OrdConnected.{u_1} (α := WithTop ι) (Iio ⊤)
Tactic: rw [WithTop.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (range some)
have rw : IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Iio ⊤)
Tactic: rw [WithTop.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
d : ι
a : WithTop ι
ha : a ≠ ⊤
⊢ Tendsto (untopD d) (𝓝 a) (𝓝 (untopD d a))
have lift : ∀ (a : ι), Tendsto (untopD d) (𝓝 (↑a : WithTop ι)) (𝓝 (untopD d (↑a : WithTop ι)))
Tactic: lift a to ι using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
d a : ι
⊢ Tendsto (untopD d) (𝓝 (↑a : WithTop ι)) (𝓝 (untopD d (↑a : WithTop ι)))
have rw : Tendsto (untopD d ∘ some) (𝓝 a) (𝓝 (untopD d (↑a : WithTop ι)))
Tactic: rw [nhds_coe, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
a : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)
⊢ Tendsto (fun (x : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)) ↦ (↑x : WithTop ι).untop ⋯) (𝓝 a)
    (𝓝 ((↑a : WithTop ι).untop ⋯))
have this : Nonempty ι
Tactic: have : Nonempty ι := ⟨untop a.1 a.2⟩
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
a : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)
this : Nonempty ι
⊢ Tendsto (fun (x : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)) ↦ (↑x : WithTop ι).untop ⋯) (𝓝 a)
    (𝓝 ((↑a : WithTop ι).untop ⋯))
have simp : Tendsto (fun (x : { x : WithTop ι // ¬x = ⊤ }) ↦ (↑x : WithTop ι).untopA) (𝓝 a) (𝓝 (↑a : WithTop ι).untopA)
Tactic: simp only [← untopA_eq_untop, ne_eq, coe_setOf, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
x : WithTop ι
⊢ (fun (x : ι ⊕ Unit) ↦
        (match (motive := ι ⊕ Unit → WithTop ι) x with
          | Sum.inl i => (↑i : WithTop ι)
          | Sum.inr PUnit.unit => ⊤ :
          WithTop ι))
      ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit)) x) =
    x
have top : Eq.{u_1 + 1} (α := WithTop ι)
  ((fun (x : ι ⊕ Unit) ↦
      (match (motive := ι ⊕ Unit → WithTop ι) x with
        | Sum.inl i => (↑i : WithTop ι)
        | Sum.inr PUnit.unit => ⊤ :
        WithTop ι))
    ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit)) ⊤))
  ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
x : WithTop ι
top :
  Eq.{u_1 + 1} (α := WithTop ι)
    ((fun (x : ι ⊕ Unit) ↦
        (match (motive := ι ⊕ Unit → WithTop ι) x with
          | Sum.inl i => (↑i : WithTop ι)
          | Sum.inr PUnit.unit => ⊤ :
          WithTop ι))
      ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit)) ⊤))
    ⊤
⊢ (fun (x : ι ⊕ Unit) ↦
        (match (motive := ι ⊕ Unit → WithTop ι) x with
          | Sum.inl i => (↑i : WithTop ι)
          | Sum.inr PUnit.unit => ⊤ :
          WithTop ι))
      ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit)) x) =
    x
have coe : ∀ (a : ι),
  (fun (x : ι ⊕ Unit) ↦
        (match (motive := ι ⊕ Unit → WithTop ι) x with
          | Sum.inl i => (↑i : WithTop ι)
          | Sum.inr PUnit.unit => ⊤ :
          WithTop ι))
      ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit)) (↑a : WithTop ι)) =
    (↑a : WithTop ι)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
x : ι ⊕ Unit
⊢ (fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit))
      ((fun (x : ι ⊕ Unit) ↦
          (match (motive := ι ⊕ Unit → WithTop ι) x with
            | Sum.inl i => (↑i : WithTop ι)
            | Sum.inr PUnit.unit => ⊤ :
            WithTop ι))
        x) =
    x
have inl : ∀ (val : ι),
  Eq (α := ι ⊕ Unit)
    ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit))
      ((fun (x : ι ⊕ Unit) ↦
          (match (motive := ι ⊕ Unit → WithTop ι) x with
            | Sum.inl i => (↑i : WithTop ι)
            | Sum.inr PUnit.unit => ⊤ :
            WithTop ι))
        (Sum.inl val)))
    (Sum.inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
x : ι ⊕ Unit
inl :
  ∀ (val : ι),
    Eq (α := ι ⊕ Unit)
      ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit))
        ((fun (x : ι ⊕ Unit) ↦
            (match (motive := ι ⊕ Unit → WithTop ι) x with
              | Sum.inl i => (↑i : WithTop ι)
              | Sum.inr PUnit.unit => ⊤ :
              WithTop ι))
          (Sum.inl val)))
      (Sum.inl val)
⊢ (fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit))
      ((fun (x : ι ⊕ Unit) ↦
          (match (motive := ι ⊕ Unit → WithTop ι) x with
            | Sum.inl i => (↑i : WithTop ι)
            | Sum.inr PUnit.unit => ⊤ :
            WithTop ι))
        x) =
    x
have inr : ∀ (val : Unit),
  Eq.{u_1 + 1} (α := ι ⊕ Unit)
    ((fun (x : WithTop ι) ↦ (if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA : ι ⊕ Unit))
      ((fun (x : ι ⊕ Unit) ↦
          (match (motive := ι ⊕ Unit → WithTop ι) x with
            | Sum.inl i => (↑i : WithTop ι)
            | Sum.inr PUnit.unit => ⊤ :
            WithTop ι))
        (Sum.inr val)))
    (Sum.inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
have simp : Eq (α := Set (WithTop ι)) ({⊤} \ interior {⊤}) ∅
Tactic: simp only [frontier, Set.finite_singleton, Set.Finite.isClosed, IsClosed.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Eq (α := Set (WithTop ι)) ({⊤} \ interior {⊤}) ∅
have suffices : Eq (α := Set (WithTop ι)) (interior {⊤}) {⊤}
Tactic: suffices interior ({⊤} : Set (WithTop ι)) = {⊤} by simp [this]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Eq (α := Set (WithTop ι)) (interior {⊤}) {⊤}
have rw : IsOpen[TopologicalSpace.instWithTopOfOrderTopology] {⊤}
Tactic: rw [interior_eq_iff_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))
have h : ∀ (x : WithTop ι),
  Membership.mem (γ := Set (WithTop ι)) {⊤} x ↔ Membership.mem (γ := Set (WithTop ι)) (Ioi (↑⊤ : WithTop ι)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] {⊤}
have this : Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))
Tactic: have : {⊤} = Set.Ioi ((⊤ : ι) : WithTop ι) := by ext; simp
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
this : Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] {⊤}
have rw : IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Ioi (↑⊤ : WithTop ι))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (hypothesis)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Continuous[TopologicalSpace.instWithTopOfOrderTopology, instTopologicalSpaceSum] fun (x : WithTop ι) ↦
    if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA
have h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
Tactic: have h_fr : frontier ({⊤} : Set (WithTop ι)) = ∅ := by
      simp only [frontier, Set.finite_singleton, Set.Finite.isClosed, IsClosed.closure_eq]
      suffices interior ({⊤} : Set (WithTop ι)) = {⊤} by simp [this]
      rw [interior_eq_iff_isOpen]
      have : {⊤} = Set.Ioi ((⊤ : ι) : WithTop ι) := by ext; simp
      rw [this]
      exact isOpen_Ioi
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
⊢ Continuous[TopologicalSpace.instWithTopOfOrderTopology, instTopologicalSpaceSum] fun (x : WithTop ι) ↦
    if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA
have refine : ContinuousOn (Y := ι ⊕ Unit) (fun (x : WithTop ι) ↦ Sum.inl x.untopA) {x : WithTop ι | ¬x = ⊤}
Tactic: refine continuous_if' (by simp [h_fr]) (by simp [h_fr]) (by simp) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
have inl : ∀ (h : IsEmpty ι), Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
Tactic: obtain (h | h) := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
inl : ∀ (h : IsEmpty ι), Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
have inr : ∀ (h : Nonempty ι), Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
Tactic: obtain (h | h) := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
have inr : (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
Tactic: refine nhds_top_basis.tendsto_right_iff.trans ?_
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
⊢ (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
have inr : (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔
  ∀ (a : WithTop ι), Membership.mem (γ := Set (WithTop ι)) (Iio ⊤) a → ∀ᶠ (a_2 : α) in f, a < x a_2
Tactic: rw [← Set.forall_mem_range (p := (∀ᶠ a in f, · < x a)), WithTop.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
⊢ Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
have inl : ∀ (h : IsEmpty ι), Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
Tactic: obtain (h | h) := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
inl : ∀ (h : IsEmpty ι), Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
⊢ Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
have inr : ∀ (h : Nonempty ι), Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
Tactic: obtain (h | h) := isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
h : Nonempty ι
⊢ Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
have inr : ∀ (i : ι), ∀ᶠ (a : ι) in atTop, (↑i : WithTop ι) < (↑a : WithTop ι)
Tactic: rw [tendsto_nhds_top_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
h : Nonempty ι
i : ι
⊢ ∀ᶠ (a : ι) in atTop, (↑i : WithTop ι) < (↑a : WithTop ι)
have h₁ : ∀ a ∈ Ioi i, (↑i : WithTop ι) < (↑a : WithTop ι)
Tactic: filter_upwards [atTop_basis_Ioi.mem_of_mem (i := i) trivial]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ 𝓝 a = ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s
have rw : Eq.{u + 1} (α := Filter α)
  (⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[generateFrom g] s} s), 𝓟 s)
  (⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s)
Tactic: rw [nhds_def]
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[generateFrom g] s} s), 𝓟 s)
    (⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s)
have refine : ∀ (i : Set α) (j : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ IsOpen[generateFrom g] s} i),
  ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 i
Tactic: refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
S : Set (Set α)
h : ∀ s ∈ S, GenerateOpen g s
hS :
  ∀ s ∈ S,
    ∀ (ha : a ∈ s), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
ha : a ∈ ⋃₀ S
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (⋃₀ S)
have sUnion : ∀ (t : Set α) (htS : t ∈ S) (hat : a ∈ t),
  ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (⋃₀ S)
Tactic: let ⟨t, htS, hat⟩ := ha
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen[generateFrom g] s
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
have basic : ∀ (s : Set α) (hs : s ∈ g) (ha : a ∈ s),
  ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
Tactic: induction hs with
  | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
  | univ => exact le_top.trans_eq principal_univ.symm
  | inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
  | sUnion _ _ hS =>
    let ⟨t, htS, hat⟩ := ha
    exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
Cleared hypotheses: ha, hs
-- Lean 4 proof step from Mathlib.Topology.Order (goal)
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen[generateFrom g] s
basic :
  ∀ (s : Set α) (hs : s ∈ g) (ha : a ∈ s),
    ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s
have univ : ∀ (ha : Membership.mem (γ := Set α) univ a),
  LE.le.{u} (α := Filter α)
    (⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s) (𝓟 univ)
Tactic: induction hs with
  | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
  | univ => exact le_top.trans_eq principal_univ.symm
  | inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
  | sUnion _ _ hS =>
    let ⟨t, htS, hat⟩ := ha
    exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)
Cleared hypotheses: ha, hs