awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : Nonempty ι
⊢ ContinuousOn.{u_1, u_1} (X := WithTop ι) untopA {a : WithTop ι | a ≠ ⊤}

Tactic:
continuousOn_untopD _

Premises used: WithTop.continuousOn_untopD
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
a : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)
⊢ Nonempty ι

Tactic:
have : Nonempty ι := ⟨untop a.1 a.2⟩
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
a : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)
this : Nonempty ι
simp : Tendsto (fun (x : { x : WithTop ι // ¬x = ⊤ }) ↦ (↑x : WithTop ι).untopA) (𝓝 a) (𝓝 (↑a : WithTop ι).untopA)
⊢ Tendsto (fun (x : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)) ↦ (↑x : WithTop ι).untop ⋯) (𝓝 a)
    (𝓝 ((↑a : WithTop ι).untop ⋯))

Tactic:
simp only [← untopA_eq_untop, ne_eq, coe_setOf, mem_setOf_eq]

Premises used: WithTop.untopA_eq_untop, Set.mem_setOf_eq, ne_eq, Set.coe_setOf
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
a : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)
this : Nonempty ι
⊢ Tendsto (fun (x : { x : WithTop ι // ¬x = ⊤ }) ↦ (↑x : WithTop ι).untopA) (𝓝 a) (𝓝 (↑a : WithTop ι).untopA)

Tactic:
(tendsto_untopA a.2).comp <| tendsto_subtype_rng.mp tendsto_id

Premises used: Filter.tendsto_id, WithTop.tendsto_untopA, Iff.mp, tendsto_subtype_rng, WithTop.untopD, Filter.Tendsto.comp, WithTop.recTopCoe, Subtype.property
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
a : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)
this : Nonempty ι
⊢ Tendsto (fun (x : { x : WithTop ι // ¬x = ⊤ }) ↦ (↑x : WithTop ι).untopA) (𝓝 a) (𝓝 (↑a : WithTop ι).untopA)

Tactic:
exact (tendsto_untopA a.2).comp <| tendsto_subtype_rng.mp tendsto_id

Premises used: Filter.tendsto_id, WithTop.tendsto_untopA, Iff.mp, tendsto_subtype_rng, Filter.Tendsto.comp, Subtype.property
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
⊢ Continuous[instTopologicalSpaceSubtype, inst_1] fun (x : (↑{a : WithTop ι | a ≠ ⊤} : Type u_1)) ↦
    (↑x : WithTop ι).untop ⋯

Tactic:
continuous_iff_continuousAt.mpr tendsto_untop

Premises used: Iff.mpr, WithTop.tendsto_untop, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Order.WithTop
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)) ⊤))
    ⊤
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 ι)
⊢ (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

Tactic:
cases x
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ 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:
simp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
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:
simp
-- Module: Mathlib.Topology.Order.WithTop
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)
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)
⊢ (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

Tactic:
cases x
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
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:
simp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
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:
simp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
simp : Eq (α := Set (WithTop ι)) ({⊤} \ interior {⊤}) ∅
⊢ Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅

Tactic:
simp only [frontier, Set.finite_singleton, Set.Finite.isClosed, IsClosed.closure_eq]

Premises used: frontier, IsClosed.closure_eq, Set.finite_singleton, Set.Finite.isClosed
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
this : Eq (α := Set (WithTop ι)) (interior {⊤}) {⊤}
⊢ Eq (α := Set (WithTop ι)) ({⊤} \ interior {⊤}) ∅

Tactic:
simp [this]
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
suffices : Eq (α := Set (WithTop ι)) (interior {⊤}) {⊤}
⊢ Eq (α := Set (WithTop ι)) ({⊤} \ interior {⊤}) ∅

Tactic:
suffices interior ({⊤} : Set (WithTop ι)) = {⊤} by simp [this]
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
rw : IsOpen[TopologicalSpace.instWithTopOfOrderTopology] {⊤}
⊢ Eq (α := Set (WithTop ι)) (interior {⊤}) {⊤}

Tactic:
rw [interior_eq_iff_isOpen]

Premises used: interior_eq_iff_isOpen
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h :
  ∀ (x : WithTop ι),
    Membership.mem (γ := Set (WithTop ι)) {⊤} x ↔ Membership.mem (γ := Set (WithTop ι)) (Ioi (↑⊤ : WithTop ι)) x
⊢ Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))

Tactic:
ext
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
x : WithTop ι
⊢ Membership.mem (γ := Set (WithTop ι)) {⊤} x ↔ Membership.mem (γ := Set (WithTop ι)) (Ioi (↑⊤ : WithTop ι)) x

Tactic:
simp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))

Tactic:
have : {⊤} = Set.Ioi ((⊤ : ι) : WithTop ι) := by ext; simp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
this : Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))
rw : IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Ioi (↑⊤ : WithTop ι))
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] {⊤}

Tactic:
rw [this]
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
this : Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Ioi (↑⊤ : WithTop ι))

Tactic:
isOpen_Ioi

Premises used: isOpen_Ioi
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
this : Eq (α := Set (WithTop ι)) {⊤} (Ioi (↑⊤ : WithTop ι))
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Ioi (↑⊤ : WithTop ι))

Tactic:
exact isOpen_Ioi

Premises used: isOpen_Ioi
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ 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
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
⊢ ∀ (a : WithTop ι),
    Membership.mem (γ := Set (WithTop ι)) (frontier {x : WithTop ι | x = ⊤}) a →
      Tendsto (fun (x : WithTop ι) ↦ Sum.inr ()) (𝓝[{x : WithTop ι | x = ⊤}] a)
        (𝓝 (if a = ⊤ then Sum.inr () else Sum.inl a.untopA))

Tactic:
simp [h_fr]
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
⊢ ∀ (a : WithTop ι),
    Membership.mem (γ := Set (WithTop ι)) (frontier {x : WithTop ι | x = ⊤}) a →
      Tendsto (fun (x : WithTop ι) ↦ Sum.inl x.untopA) (𝓝[{x : WithTop ι | ¬x = ⊤}] a)
        (𝓝 (if a = ⊤ then Sum.inr () else Sum.inl a.untopA))

Tactic:
simp [h_fr]
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
⊢ ContinuousOn (Y := ι ⊕ Unit) (fun (x : WithTop ι) ↦ Sum.inr ()) {x : WithTop ι | x = ⊤}

Tactic:
simp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
refine : ContinuousOn (Y := ι ⊕ Unit) (fun (x : WithTop ι) ↦ Sum.inl x.untopA) {x : WithTop ι | ¬x = ⊤}
⊢ Continuous[TopologicalSpace.instWithTopOfOrderTopology, instTopologicalSpaceSum] fun (x : WithTop ι) ↦
    if h : x = ⊤ then Sum.inr () else Sum.inl x.untopA

Tactic:
refine continuous_if' (by simp [h_fr]) (by simp [h_fr]) (by simp) ?_

Premises used: continuous_if'
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
⊢ Continuous[inst_1, instTopologicalSpaceSum] Sum.inl

Tactic:
fun_prop
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
h_fr : Eq (α := Set (WithTop ι)) (frontier {⊤}) ∅
⊢ ContinuousOn (Y := ι ⊕ Unit) (fun (x : WithTop ι) ↦ Sum.inl x.untopA) {x : WithTop ι | ¬x = ⊤}

Tactic:
exact Continuous.comp_continuousOn (by fun_prop) continuousOn_untopA

Premises used: Continuous.comp_continuousOn, WithTop.continuousOn_untopA
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Continuous[inst_1, TopologicalSpace.instWithTopOfOrderTopology]
    ((fun (x : ι ⊕ Unit) ↦
        match (motive := ι ⊕ Unit → WithTop ι) x with
        | Sum.inl i => (↑i : WithTop ι)
        | Sum.inr PUnit.unit => ⊤) ∘
      Sum.inl)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : OrderTop ι
⊢ Continuous[_, TopologicalSpace.instWithTopOfOrderTopology]
    ((fun (x : ι ⊕ Unit) ↦
        match (motive := ι ⊕ Unit → WithTop ι) x with
        | Sum.inl i => (↑i : WithTop ι)
        | Sum.inr PUnit.unit => ⊤) ∘
      Sum.inr)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Order.WithTop
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
inr : ∀ (h : Nonempty ι), Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a

Tactic:
obtain (h | h) := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : IsEmpty ι
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a

Tactic:
simpa using .of_forall fun _ ↦ Subsingleton.elim ..
-- Module: Mathlib.Topology.Order.WithTop
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

Tactic:
nhds_top_basis.tendsto_right_iff.trans ?_

Premises used: Iff.trans, Filter.HasBasis.tendsto_right_iff, nhds_top_basis
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
inr : (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a
⊢ Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a

Tactic:
refine nhds_top_basis.tendsto_right_iff.trans ?_

Premises used: Iff.trans, Filter.HasBasis.tendsto_right_iff, nhds_top_basis
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
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
⊢ (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, (↑i : WithTop ι) < x a

Tactic:
rw [← Set.forall_mem_range (p := (∀ᶠ a in f, · < x a)), WithTop.range_coe]

Premises used: Set.forall_mem_range, WithTop.range_coe
-- Module: Mathlib.Topology.Order.WithTop
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) ↔
    ∀ (a : WithTop ι), Membership.mem (γ := Set (WithTop ι)) (Iio ⊤) a → ∀ᶠ (a_2 : α) in f, a < x a_2

Tactic:
simp
-- Module: Mathlib.Topology.Order.WithTop
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 (𝓝 ⊤)
inr : ∀ (h : Nonempty ι), Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)
⊢ Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)

Tactic:
obtain (h | h) := isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
h : IsEmpty ι
⊢ Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)

Tactic:
simpa using Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
h : Nonempty ι
inr : ∀ (i : ι), ∀ᶠ (a : ι) in atTop, (↑i : WithTop ι) < (↑a : WithTop ι)
⊢ Tendsto.{u_1, u_1} (α := ι) some atTop (𝓝 ⊤)

Tactic:
rw [tendsto_nhds_top_iff]

Premises used: WithTop.tendsto_nhds_top_iff
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
h : Nonempty ι
i : ι
h₁ : ∀ a ∈ Ioi i, (↑i : WithTop ι) < (↑a : WithTop ι)
⊢ ∀ᶠ (a : ι) in atTop, (↑i : WithTop ι) < (↑a : WithTop ι)

Tactic:
filter_upwards [atTop_basis_Ioi.mem_of_mem (i := i) trivial]

Premises used: trivial, Filter.atTop_basis_Ioi, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
inst_3 : NoMaxOrder ι
h : Nonempty ι
i : ι
⊢ ∀ a ∈ Ioi i, (↑i : WithTop ι) < (↑a : WithTop ι)

Tactic:
simp
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
s : Set α
hs : s ∈ g
⊢ IsOpen[generateFrom g] s

Tactic:
GenerateOpen.basic s hs

Premises used: TopologicalSpace.GenerateOpen.basic, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
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)
⊢ 𝓝 a = ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s

Tactic:
rw [nhds_def]

Premises used: nhds_def
-- Module: Mathlib.Topology.Order
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)

Tactic:
le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_

Premises used: TopologicalSpace.GenerateOpen.basic, setOf, Membership.mem, le_iInf₂, _private.0.TopologicalSpace.nhds_generateFrom.match_1, le_antisymm, And, And.intro, biInf_mono, IsOpen
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
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
⊢ 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:
refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_

Premises used: le_iInf₂, le_antisymm, biInf_mono
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s_1 : Set α
hs : s_1 ∈ g
ha : a ∈ s_1
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s_1

Tactic:
iInf₂_le _ ⟨ha, hs⟩

Premises used: Set.Mem, iInf₂_le, setOf
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s_1 : Set α
hs : s_1 ∈ g
ha : a ∈ s_1
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s_1

Tactic:
exact iInf₂_le _ ⟨ha, hs⟩

Premises used: iInf₂_le
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
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:
le_top.trans_eq principal_univ.symm

Premises used: LE.le.trans_eq, Filter.principal_univ, le_top, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
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:
exact le_top.trans_eq principal_univ.symm

Premises used: LE.le.trans_eq, Filter.principal_univ, le_top, Eq.symm
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s_1 t : Set α
h : GenerateOpen g s_1
h_1 : GenerateOpen g t
hs :
  ∀ (ha : a ∈ s_1), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s_1
ht : ∀ (ha : a ∈ t), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 t
ha : a ∈ s_1 ∩ t
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (s_1 ∩ t)

Tactic:
(le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal

Premises used: LE.le.trans_eq, Filter.inf_principal, le_inf, And.right, And.left
-- Module: Mathlib.Topology.Order
Goal:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s s_1 t : Set α
h : GenerateOpen g s_1
h_1 : GenerateOpen g t
hs :
  ∀ (ha : a ∈ s_1), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 s_1
ht : ∀ (ha : a ∈ t), ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 t
ha : a ∈ s_1 ∩ t
⊢ ⨅ (s : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {s : Set α | a ∈ s ∧ s ∈ g} s), 𝓟 s ≤ 𝓟 (s_1 ∩ t)

Tactic:
exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal

Premises used: LE.le.trans_eq, Filter.inf_principal, le_inf, And.right, And.left
-- Module: Mathlib.Topology.Order
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
sUnion :
  ∀ (t : Set α) (htS : t ∈ S) (hat : a ∈ t),
    ⨅ (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)

Tactic:
let ⟨t, htS, hat⟩ := ha