awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
ha : IsSuccPrelimit a
⊢ map (α := { x : X // x ∈ Iio a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop = 𝓝[<] a

Tactic:
map_coe_Ioi_atBot (toDual a) ha.dual

Premises used: Order.IsSuccPrelimit.dual, OrderDual.toDual, Set.Ici, Set.Mem, setOf, Filter.atTop, map_coe_Ioi_atBot, OrderDual, Set.Iio, DFunLike.coe
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
rw :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto (α := { x : X // x ∈ Ioo a b }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop l
rw₂ rw₃ :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto (fun (x : { x : X // x ∈ Ioo a b }) ↦ f (↑x : X)) atTop l
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] b) l

Tactic:
rw [← map_coe_Ioo_atTop h hb, tendsto_map'_iff, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, map_coe_Ioo_atTop, Function.comp_def
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
ha : IsPredPrelimit a
rw :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot) l
rw₁ :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto (α := { x : X // x ∈ Ioo a b }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot l
rw₂ rw₃ :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto (fun (x : { x : X // x ∈ Ioo a b }) ↦ f (↑x : X)) atBot l
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
rw [← map_coe_Ioo_atBot h ha, tendsto_map'_iff, Function.comp_def]

Premises used: map_coe_Ioo_atBot, Filter.tendsto_map'_iff, Function.comp_def
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
rw :
  Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioi a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot) l
rw₁ :
  Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto (α := { x : X // x ∈ Ioi a }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot l
rw₂ rw₃ :
  Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto (fun (x : { x : X // x ∈ Ioi a }) ↦ f (↑x : X)) atBot l
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l

Tactic:
rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, map_coe_Ioi_atBot, Function.comp_def
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
rw :
  Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto f (map (α := { x : X // x ∈ Iio a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto (α := { x : X // x ∈ Iio a }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop l
rw₂ rw₃ :
  Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto (fun (x : { x : X // x ∈ Iio a }) ↦ f (↑x : X)) atTop l
⊢ Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] a) l

Tactic:
rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]

Premises used: Filter.tendsto_map'_iff, Function.comp_def, map_coe_Iio_atTop
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
hb : IsSuccPrelimit b
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[<] b)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b) ∘ f) l (𝓝[<] b) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
rw₂ rw₃ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)

Tactic:
rw [← comap_coe_Ioo_nhdsLT a b hb, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.tendsto_comap_iff, Function.comp_def, comap_coe_Ioo_nhdsLT
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
ha : IsPredPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[>] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b) ∘ f) l (𝓝[>] a) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
rw₂ rw₃ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)

Tactic:
rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.tendsto_comap_iff, Function.comp_def, comap_coe_Ioo_nhdsGT
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Ioi a) : Type u_1)
ha : IsPredPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) (𝓝[>] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a) ∘ f) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
rw₂ rw₃ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)

Tactic:
rw [← comap_coe_Ioi_nhdsGT a ha, tendsto_comap_iff, Function.comp_def]

Premises used: comap_coe_Ioi_nhdsGT, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Iio a) : Type u_1)
ha : IsSuccPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) (𝓝[<] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a) ∘ f) l (𝓝[<] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
rw₂ rw₃ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)

Tactic:
rw [← comap_coe_Iio_nhdsLT a ha, tendsto_comap_iff, Function.comp_def]

Premises used: Filter.tendsto_comap_iff, Function.comp_def, comap_coe_Iio_nhdsLT
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
inl : IsEmpty α → ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
inr : Nonempty α → ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h_1 : IsEmpty α
h :
  univ ∈ 𝓝 x ∧
    Set.Finite.{u_2} (α := α) {i : α | Set.Nonempty.{u_1} (α := X) ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ univ)}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
use univ

Premises used: Set.univ
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : IsEmpty α
⊢ univ ∈ 𝓝 x ∧
    Set.Finite.{u_2} (α := α) {i : α | Set.Nonempty.{u_1} (α := X) ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ univ)}

Tactic:
simp [Subsingleton.elim _ (∅ : Set α)]

Premises used: EmptyCollection.emptyCollection, Subsingleton.elim
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
inr :
  ∀ (x_L : X) (hx_L : x_L < x),
    ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
obtain ⟨x_L, hx_L⟩ := exists_lt x

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
inr :
  ∀ (x_R : X) (hx_R : x < x_R),
    ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
obtain ⟨x_R, hx_R⟩ := exists_gt x

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
inr :
  ∀ (a_L : α) (ha_L : ∀ a ≤ a_L, g a ≤ x_L),
    ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
obtain ⟨a_L, ha_L : ∀ a ≤ a_L, g a ≤ x_L⟩ :=
    hu.eventually_le_atBot x_L |>.exists_forall_of_atBot

Premises used: Filter.Tendsto.eventually_le_atBot, Filter.Eventually.exists_forall_of_atBot
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
inr :
  ∀ (a_R : α) (ha_R : ∀ a ≥ a_R, x_R ≤ f a),
    ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
obtain ⟨a_R, ha_R : ∀ a ≥ a_R, x_R ≤ f a⟩ :=
    hl.eventually_ge_atTop x_R |>.exists_forall_of_atTop

Premises used: Filter.Tendsto.eventually_ge_atTop, Filter.Eventually.exists_forall_of_atTop
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
⟨Ioo x_L x_R, Ioo_mem_nhds hx_L hx_R, (finite_Icc a_L a_R).subset ?_⟩

Premises used: Set.Finite.subset, Set.finite_Icc, Ioo_mem_nhds, And.intro, Exists.intro, Set.Ioo
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
inr : {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ Ioo x_L x_R).Nonempty} ⊆ Icc a_L a_R
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}

Tactic:
refine ⟨Ioo x_L x_R, Ioo_mem_nhds hx_L hx_R, (finite_Icc a_L a_R).subset ?_⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
inr : a_L ≤ n
inr₁ : n ≤ a_R
⊢ n ∈ Icc a_L a_R

Tactic:
constructor
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
inr : ∀ (hxL : n < a_L), y ≤ x_L
⊢ a_L ≤ n

Tactic:
contrapose! hxL
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxR : y < x_R
hxL : n < a_L
⊢ y ≤ x_L

Tactic:
hg.trans (ha_L n hxL.le)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxR : y < x_R
hxL : n < a_L
⊢ y ≤ x_L

Tactic:
exact hg.trans (ha_L n hxL.le)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
inr : ∀ (hxR : a_R < n), x_R ≤ y
⊢ n ≤ a_R

Tactic:
contrapose! hxR
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : a_R < n
⊢ x_R ≤ y

Tactic:
(ha_R n hxR.le).trans hf

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : a_R < n
⊢ x_R ≤ y

Tactic:
exact (ha_R n hxR.le).trans hf

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
l u : α → X
hl : Tendsto l atTop atTop
hu : Tendsto u atBot atBot
⊢ LocallyFinite.{u_2, u_1} (X := X) fun (n : α) ↦ Ico (l n) (u n)

Tactic:
locallyFinite_Icc_of_tendsto hl hu |>.subset fun _ => Set.Ico_subset_Icc_self

Premises used: Set.Ico_subset_Icc_self, locallyFinite_Icc_of_tendsto, LocallyFinite.subset
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
l u : α → X
hl : Tendsto l atTop atTop
hu : Tendsto u atBot atBot
⊢ LocallyFinite.{u_2, u_1} (X := X) fun (n : α) ↦ Ioc (l n) (u n)

Tactic:
locallyFinite_Icc_of_tendsto hl hu |>.subset fun _ => Set.Ioc_subset_Icc_self

Premises used: locallyFinite_Icc_of_tendsto, LocallyFinite.subset, Set.Ioc_subset_Icc_self
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
l u : α → X
hl : Tendsto l atTop atTop
hu : Tendsto u atBot atBot
⊢ LocallyFinite.{u_2, u_1} (X := X) fun (n : α) ↦ Ioo (l n) (u n)

Tactic:
locallyFinite_Icc_of_tendsto hl hu |>.subset fun _ => Set.Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, locallyFinite_Icc_of_tendsto, LocallyFinite.subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := TopologicalSpace α) (generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a})
    (generateFrom {s : Set α | ∃ (a : α), s = Iio a ∨ s = Ioi a})

Tactic:
simp_rw [or_comm]

Premises used: or_comm
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
⊢ SecondCountableTopology α

Tactic:
⟨{ s : Set α | ∃ a, s = Ioi a ∨ s = Iio a }, ?_, ?_⟩

Premises used: Set.Ioi, setOf, Exists, SecondCountableTopology.mk, And.intro, Exists.intro, Or, Set.Iio, Eq
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
refine_1 : Set.Countable.{u} (α := Set α) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
refine_2 : ts = generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
⊢ SecondCountableTopology α

Tactic:
refine ⟨{ s : Set α | ∃ a, s = Ioi a ∨ s = Iio a }, ?_, ?_⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
f1 : α → Set α := fun (a : α) ↦ Ioi a
f2 : α → Set α := fun (a : α) ↦ Iio a
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s
⊢ s ∈ range f1 ∪ range f2

Tactic:
grind
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
f1 : α → Set α := fun (a : α) ↦ Ioi a
f2 : α → Set α := fun (a : α) ↦ Iio a
⊢ Set.Countable.{u} (α := Set α) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

Tactic:
exact Countable.mono (fun s hs => by grind) ((countable_range f1).union (countable_range f2))

Premises used: Set.countable_range, Set.Countable.union, Set.Countable.mono
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
⊢ ts = generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

Tactic:
OrderTopology.topology_eq_generate_intervals

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
⊢ ts = generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

Tactic:
exact OrderTopology.topology_eq_generate_intervals

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
topology_eq_generate_intervals :
  Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)
⊢ OrderTopology.{u} αᵒᵈ

Tactic:
constructor
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
topology_eq_generate_intervals :
  ∀ [t : OrderTopology α], Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)
⊢ Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)

Tactic:
rcases t.topology_eq_generate_intervals with rfl

Premises used: OrderTopology.topology_eq_generate_intervals, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
t : OrderTopology α
topology_eq_generate_intervals :
  Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace
    (generateFrom {s : Set αᵒᵈ | ∃ (a : αᵒᵈ), s = Iio a ∨ s = Ioi a})
⊢ Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)

Tactic:
simp_rw [Preorder.topology, or_comm]

Premises used: Preorder.topology, or_comm
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
t : OrderTopology α
⊢ Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace
    (generateFrom {s : Set αᵒᵈ | ∃ (a : αᵒᵈ), s = Iio a ∨ s = Ioi a})

Tactic:
rfl