awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iic a ∪ Ici a] a = 𝓝 a
rw₁ : 𝓝[univ] a = 𝓝 a
rw₂ rw₃ : 𝓝 a = 𝓝 a
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]

Premises used: nhdsWithin_univ, Set.Iic_union_Ici, nhdsWithin_union
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ici a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iic a ∪ Ici a)] a = 𝓝[s] a
rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
rw₃ rw₄ : 𝓝[s] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a

Tactic:
rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]

Premises used: Set.inter_univ, Set.Iic_union_Ici, nhdsWithin_union, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iio a ∪ Ici a] a = 𝓝 a
rw₁ : 𝓝[univ] a = 𝓝 a
rw₂ rw₃ : 𝓝 a = 𝓝 a
⊢ 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]

Premises used: Set.Iio_union_Ici, nhdsWithin_univ, nhdsWithin_union
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ici a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ici a)] a = 𝓝[s] a
rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
rw₃ rw₄ : 𝓝[s] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a

Tactic:
rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]

Premises used: Set.Iio_union_Ici, Set.inter_univ, nhdsWithin_union, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iic a ∪ Ioi a] a = 𝓝 a
rw₁ : 𝓝[univ] a = 𝓝 a
rw₂ rw₃ : 𝓝 a = 𝓝 a
⊢ 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]

Premises used: nhdsWithin_univ, Set.Iic_union_Ioi, nhdsWithin_union
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iic a ∪ s ∩ Ioi a] a = 𝓝[s] a
rw₁ : 𝓝[s ∩ (Iic a ∪ Ioi a)] a = 𝓝[s] a
rw₂ : 𝓝[s ∩ univ] a = 𝓝[s] a
rw₃ rw₄ : 𝓝[s] a = 𝓝[s] a
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a

Tactic:
rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]

Premises used: Set.inter_univ, Set.Iic_union_Ioi, nhdsWithin_union, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
rw : 𝓝[Iio a ∪ Ioi a] a = 𝓝[≠] a
rw₁ rw₂ : 𝓝[≠] a = 𝓝[≠] a
⊢ 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a

Tactic:
rw [← nhdsWithin_union, Iio_union_Ioi]

Premises used: Set.Iio_union_Ioi, nhdsWithin_union
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
s : Set α
a : α
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a = 𝓝[s \ {a}] a
rw₁ : 𝓝[s ∩ (Iio a ∪ Ioi a)] a = 𝓝[s \ {a}] a
rw₂ : 𝓝[s ∩ {a}ᶜ] a = 𝓝[s \ {a}] a
rw₃ : 𝓝[s ∩ (univ \ {a})] a = 𝓝[s \ {a}] a
rw₄ : 𝓝[univ ∩ (s \ {a})] a = 𝓝[s \ {a}] a
rw₅ rw₆ : 𝓝[s \ {a}] a = 𝓝[s \ {a}] a
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a

Tactic:
rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
    inter_sdiff_left_comm, univ_inter]

Premises used: Set.univ_inter, Set.Iio_union_Ioi, nhdsWithin_union, Set.compl_eq_univ_diff, Set.inter_sdiff_left_comm, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a : α
⊢ 𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a

Tactic:
simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]

Premises used: Set.Ioi_insert, nhdsWithin_union, Set.union_singleton
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a b : α
⊢ uIoo a b ⊆ {a}ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
a b : α
⊢ uIoo a b ⊆ {b}ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhdsLE_sup_nhdsGE]

Premises used: ContinuousWithinAt, ContinuousAt, Filter.tendsto_sup, nhdsLE_sup_nhdsGE
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
rw : ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ici a) a
rw₁ : ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
rw₂ rw₃ :
  ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a ↔
    ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a
⊢ ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a

Tactic:
rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
    continuousAt_iff_continuous_left_right]

Premises used: continuousAt_iff_continuous_left_right, continuousWithinAt_Iio_iff_Iic, continuousWithinAt_Ioi_iff_Ici
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
s : Set α
a : α
f : α → β
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a

Tactic:
simp only [ContinuousWithinAt, ← tendsto_sup, nhdsWithinLE_sup_nhdsWithinGE]

Premises used: ContinuousWithinAt, Filter.tendsto_sup, nhdsWithinLE_sup_nhdsWithinGE
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : TopologicalSpace β
s : Set α
a : α
f : α → β
rw : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
rw₁ : ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
rw₂ rw₃ :
  ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a ↔
    ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a

Tactic:
rw [continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic,
    continuousWithinAt_iff_continuous_left_right]

Premises used: continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_inter_Iio_iff_Iic, continuousWithinAt_iff_continuous_left_right
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
haveI : (this : Nonempty β) → β
⊢ β

Tactic:
haveI : Nonempty β := ⟨f a⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
this_1 : Nonempty β
this : TopologicalSpace α := Preorder.topology α
⊢ β

Tactic:
exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f

Premises used: nhdsWithin, Set.Iio, Filter.limUnder
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
haveI haveI₁ haveI₂ haveI₃ : (this : Nonempty β) → β
⊢ β

Tactic:
classical
  haveI : Nonempty β := ⟨f a⟩
  letI : TopologicalSpace α := Preorder.topology α
  exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)

Tactic:
have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ 𝓝[<] a ≠ ⊥

Tactic:
rw [h'α.topology_eq_generate_intervals] at h h' h''

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h₁ : 𝓝[<] a ≠ ⊥
⊢ Tendsto f (𝓝[<] a) (𝓝 y)

Tactic:
rw [h'α.topology_eq_generate_intervals] at h h' h''

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h₁ : 𝓝[<] a ≠ ⊥
h'₁ : Tendsto f (𝓝[<] a) (𝓝 y)
⊢ ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)

Tactic:
rw [h'α.topology_eq_generate_intervals] at h h' h''

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
simp : (𝓝[<] a).limUnder f = y
⊢ leftLim f a = y

Tactic:
simp only [leftLim, h, h'', not_true, or_self_iff, if_false]

Premises used: or_self_iff, if_false, not_true, Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ (𝓝[<] a).NeBot

Tactic:
haveI := neBot_iff.2 h
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
this : (𝓝[<] a).NeBot
⊢ (𝓝[<] a).limUnder f = y

Tactic:
lim_eq h'

Premises used: lim_eq, Filter.limUnder
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst_2 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[<] a ≠ ⊥
h' : Tendsto f (𝓝[<] a) (𝓝 y)
h'' : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
this : (𝓝[<] a).NeBot
⊢ (𝓝[<] a).limUnder f = y

Tactic:
exact lim_eq h'

Premises used: lim_eq
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
y : β
h : 𝓝[>] a ≠ ⊥
h' : Tendsto f (𝓝[>] a) (𝓝 y)
⊢ rightLim f a = y

Tactic:
leftLim_eq_of_tendsto (α := αᵒᵈ) h h'

Premises used: Function.rightLim, leftLim_eq_of_tendsto
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ 𝓝[<] a = ⊥

Tactic:
rw [h'α.topology_eq_generate_intervals] at h

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

Tactic:
simp [leftLim, h]

Premises used: Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
h : 𝓝[>] a = ⊥
⊢ rightLim f a = f a

Tactic:
leftLim_eq_of_eq_bot (α := αᵒᵈ) f h

Premises used: leftLim_eq_of_eq_bot, Function.rightLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)

Tactic:
rw [h'α.topology_eq_generate_intervals] at h

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = f a

Tactic:
simp [leftLim, h]

Premises used: Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ (y : β), Tendsto f (𝓝[>] a) (𝓝 y)
⊢ rightLim f a = f a

Tactic:
leftLim_eq_of_not_tendsto (α := αᵒᵈ) f h

Premises used: Function.rightLim, leftLim_eq_of_not_tendsto
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
⊢ OrderTopology α

Tactic:
have : OrderTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

Tactic:
apply leftLim_eq_of_eq_bot

Premises used: leftLim_eq_of_eq_bot
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
simp : IsMin a
⊢ Iio a = ∅

Tactic:
simp
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ IsMin a

Tactic:
grind [IsBot, IsMin]

Premises used: IsBot, IsMin
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ Iio a = ∅

Tactic:
have : Iio a = ∅ := by simp; grind [IsBot, IsMin]
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this_1 : OrderTopology α
this : Iio a = ∅
⊢ 𝓝[<] a = ⊥

Tactic:
simp [this]
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
f : α → β
a : α
ha : IsTop a
⊢ rightLim f a = f a

Tactic:
leftLim_eq_of_isBot (α := αᵒᵈ) ha

Premises used: Function.rightLim, leftLim_eq_of_isBot
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
inl : ∀ (h' : 𝓝[<] a = ⊥), leftLim f a = f a
inr : ∀ (h' : 𝓝[<] a ≠ ⊥), leftLim f a = f a
⊢ leftLim f a = f a

Tactic:
rcases eq_or_ne (𝓝[<] a) ⊥ with h' | h'

Premises used: nhdsWithin, Bot.bot, eq_or_ne, Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

Tactic:
simp [leftLim_eq_of_eq_bot f h']

Premises used: leftLim_eq_of_eq_bot
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : 𝓝[<] a ≠ ⊥
inr : Tendsto f (𝓝[<] a) (𝓝 (f a))
⊢ leftLim f a = f a

Tactic:
apply leftLim_eq_of_tendsto h'

Premises used: leftLim_eq_of_tendsto
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : 𝓝[<] a ≠ ⊥
⊢ Tendsto f (𝓝[<] a) (𝓝 (f a))

Tactic:
hf.tendsto.mono_left (nhdsWithin_mono _ Iio_subset_Iic_self)

Premises used: Filter.Tendsto.mono_left, Set.Iio_subset_Iic_self, ContinuousWithinAt.tendsto, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : 𝓝[<] a ≠ ⊥
⊢ Tendsto f (𝓝[<] a) (𝓝 (f a))

Tactic:
exact hf.tendsto.mono_left (nhdsWithin_mono _ Iio_subset_Iic_self)

Premises used: Filter.Tendsto.mono_left, Set.Iio_subset_Iic_self, ContinuousWithinAt.tendsto, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Ici a) a
⊢ rightLim f a = f a

Tactic:
ContinuousWithinAt.leftLim_eq (α := αᵒᵈ) hf

Premises used: ContinuousWithinAt.leftLim_eq, Function.rightLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
inl : ∀ (h' : 𝓝[<] a = ⊥), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
inr : ∀ (h' : (𝓝[<] a).NeBot), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
rcases eq_or_neBot (𝓝[<] a) with h' | h'

Premises used: nhdsWithin, Filter.eq_or_neBot, Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : 𝓝[<] a = ⊥
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
simp [h']
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
inr : ∀ (h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)) (h' : (𝓝[<] a).NeBot), Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
rw [h'α.topology_eq_generate_intervals] at h h' ⊢

Premises used: OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
inr : Tendsto f (𝓝[<] a) (𝓝 ((𝓝[<] a).limUnder f))
⊢ Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
simp only [leftLim, neBot_iff.1 h', h, not_true_eq_false, or_self, ↓reduceIte]

Premises used: Filter.neBot_iff, not_true_eq_false, Iff.mp, or_self, reduceIte, Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 ((𝓝[<] a).limUnder f))

Tactic:
tendsto_nhds_limUnder h

Premises used: tendsto_nhds_limUnder
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 ((𝓝[<] a).limUnder f))

Tactic:
exact tendsto_nhds_limUnder h

Premises used: tendsto_nhds_limUnder
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
h : ∃ (y : β), Tendsto f (𝓝[>] a) (𝓝 y)
⊢ Tendsto f (𝓝[>] a) (𝓝 (rightLim f a))

Tactic:
tendsto_leftLim_of_tendsto (α := αᵒᵈ) h

Premises used: Set.Ioi, tendsto_leftLim_of_tendsto, setOf, Function.rightLim, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
⊢ (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot

Tactic:
inf_neBot_iff.mpr (fun s hs s' hs' ↦ ?_)

Premises used: Iff.mpr, Filter.inf_neBot_iff
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
refine : ∀ (s : Set β) (hs : s ∈ 𝓝 (f a)) (s' : Set β) (hs' : s' ∈ map f (𝓝[≤] a)), (s ∩ s').Nonempty
⊢ (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot

Tactic:
refine inf_neBot_iff.mpr (fun s hs s' hs' ↦ ?_)

Premises used: Iff.mpr, Filter.inf_neBot_iff
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
s : Set β
hs : s ∈ 𝓝 (f a)
s' : Set β
hs' : s' ∈ map f (𝓝[≤] a)
⊢ (s ∩ s').Nonempty

Tactic:
⟨f a, mem_of_mem_nhds hs, ?_⟩

Premises used: mem_of_mem_nhds, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
s : Set β
hs : s ∈ 𝓝 (f a)
s' : Set β
hs' : s' ∈ map f (𝓝[≤] a)
refine : f a ∈ s'
⊢ (s ∩ s').Nonempty

Tactic:
refine ⟨f a, mem_of_mem_nhds hs, ?_⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
s : Set β
hs : s ∈ 𝓝 (f a)
s' : Set β
hs' : s' ∈ map f (𝓝[≤] a)
⊢ f ⁻¹' s' ∈ 𝓝[≤] a

Tactic:
simp only [mem_map] at hs'

Premises used: Filter.mem_map
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
s : Set β
hs : s ∈ 𝓝 (f a)
s' : Set β
hs' : f ⁻¹' s' ∈ 𝓝[≤] a
⊢ f a ∈ s'

Tactic:
apply mem_of_mem_nhdsWithin self_mem_Iic hs'

Premises used: Set.self_mem_Iic, mem_of_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
⊢ (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot

Tactic:
have A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot := by
    refine inf_neBot_iff.mpr (fun s hs s' hs' ↦ ?_)
    refine ⟨f a, mem_of_mem_nhds hs, ?_⟩
    simp only [mem_map] at hs'
    apply mem_of_mem_nhdsWithin self_mem_Iic hs'
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
inl : ∀ (h' : 𝓝[<] a = ⊥), MapClusterPt (leftLim f a) (𝓝[≤] a) f
inr : ∀ (h' : (𝓝[<] a).NeBot), MapClusterPt (leftLim f a) (𝓝[≤] a) f
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
rcases eq_or_neBot (𝓝[<] a) with h' | h'

Premises used: nhdsWithin, Filter.eq_or_neBot, Set.Iio