awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h' : 𝓝[<] a = ⊥
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
simp only [MapClusterPt, ClusterPt, h', leftLim_eq_of_eq_bot, A]

Premises used: leftLim_eq_of_eq_bot, ClusterPt, MapClusterPt
-- 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
h' : (𝓝[<] a).NeBot
pos : ∀ (H : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)), MapClusterPt (leftLim f a) (𝓝[≤] a) f
neg : ∀ (H : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)), MapClusterPt (leftLim f a) (𝓝[≤] a) f
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
by_cases! H : ¬ ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
-- 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
h' : (𝓝[<] a).NeBot
H : ¬∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
simp [MapClusterPt, ClusterPt, H, leftLim_eq_of_not_tendsto, A]

Premises used: ClusterPt, MapClusterPt, leftLim_eq_of_not_tendsto
-- 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
h' : (𝓝[<] a).NeBot
H : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
⊢ MapClusterPt (leftLim f a) (𝓝[<] a) f

Tactic:
have : MapClusterPt (f.leftLim a) (𝓝[<] a) f := (tendsto_leftLim_of_tendsto H).mapClusterPt
-- 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
h' : (𝓝[<] a).NeBot
H : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
this : MapClusterPt (leftLim f a) (𝓝[<] a) f
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
MapClusterPt.mono this (nhdsWithin_mono _ Iio_subset_Iic_self)

Premises used: MapClusterPt.mono, Set.Iio_subset_Iic_self, 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 α
f : α → β
a : α
A : (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot
h' : (𝓝[<] a).NeBot
H : ∃ (y : β), Tendsto f (𝓝[<] a) (𝓝 y)
this : MapClusterPt (leftLim f a) (𝓝[<] a) f
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

Tactic:
exact MapClusterPt.mono this (nhdsWithin_mono _ Iio_subset_Iic_self)

Premises used: MapClusterPt.mono, Set.Iio_subset_Iic_self, 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 α
f : α → β
a : α
⊢ MapClusterPt (rightLim f a) (𝓝[≥] a) f

Tactic:
mapClusterPt_leftLim (α := αᵒᵈ) _ _

Premises used: mapClusterPt_leftLim, Set.Ici, 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 α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
rw : 𝓝[<] a ⊔ 𝓝[Icc a a] a = 𝓝[<] a ⊔ pure a
⊢ 𝓝[≤] a = 𝓝[<] a ⊔ pure a

Tactic:
rw [← Iio_union_Icc_eq_Iic le_rfl, nhdsWithin_union]

Premises used: le_rfl, Set.Iio_union_Icc_eq_Iic, nhdsWithin_union
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ 𝓝[<] a ⊔ 𝓝[Icc a a] a = 𝓝[<] a ⊔ pure a

Tactic:
simp
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ 𝓝[≤] a = 𝓝[<] a ⊔ pure a

Tactic:
have : 𝓝[≤] a = 𝓝[<] a ⊔ pure a := by
    rw [← Iio_union_Icc_eq_Iic le_rfl, nhdsWithin_union]
    simp
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
rw : Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a)) ∧ Tendsto (leftLim f) (pure a) (𝓝 (leftLim f a))
⊢ ContinuousWithinAt (leftLim f) (Iic a) a

Tactic:
rw [ContinuousWithinAt, this, tendsto_sup]

Premises used: ContinuousWithinAt, Filter.tendsto_sup
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
simp : Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a))
⊢ Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a)) ∧ Tendsto (leftLim f) (pure a) (𝓝 (leftLim f a))

Tactic:
simp only [tendsto_pure_nhds, and_true]

Premises used: and_true, tendsto_pure_nhds
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
apply : ∀ (i : Set β), i ∈ 𝓝 (leftLim f a) ∧ IsClosed[inst_1] i → ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id i
⊢ Tendsto (leftLim f) (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2

Premises used: Iff.mpr, closed_nhds_basis, Filter.HasBasis.tendsto_right_iff, 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 α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
inl : ∀ (h' : 𝓝[<] a = ⊥), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
inr : ∀ (h' : (𝓝[<] a).NeBot), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

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 α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : 𝓝[<] a = ⊥
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

Tactic:
simp [h']
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
⊢ (Iio a).Nonempty

Tactic:
Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))

Premises used: Filter.nonempty_of_mem, self_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 α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
inr : ∀ (b : α) (hb : b ∈ Iio a), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

Tactic:
obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))

Premises used: Filter.nonempty_of_mem, Set.Nonempty, self_mem_nhdsWithin, 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
⊢ ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s

Tactic:
have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this_1 : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
⊢ ∃ u < a, Ioo u a ⊆ {x : α | f x ∈ s}

Tactic:
simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this

Premises used: mem_nhdsLT_iff_exists_Ioo_subset', Iff.mp
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
inr : ∀ (u : α) (au : u < a) (hu : Ioo u a ⊆ {x : α | f x ∈ s}), ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

Tactic:
obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by
    have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
    simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
h₁ : ∀ (c : α) (hc : c ∈ Ioo u a), leftLim f c ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, leftLim f x ∈ id s

Tactic:
filter_upwards [Ioo_mem_nhdsLT au] with c hc

Premises used: Ioo_mem_nhdsLT
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h₁ : ∀ (h'c : 𝓝[<] c = ⊥), leftLim f c ∈ id s
h₂ : ∀ (h'c : (𝓝[<] c).NeBot), leftLim f c ∈ id s
⊢ leftLim f c ∈ id s

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

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 α
inst_3 : OrderTopology α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[<] c = ⊥
⊢ leftLim f c ∈ id s

Tactic:
simpa [h'c, leftLim_eq_of_eq_bot] using hu hc

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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
pos : ∀ (h''c : ¬∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)), leftLim f c ∈ id s
neg : ∀ (h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)), leftLim f c ∈ id s
⊢ leftLim f c ∈ id s

Tactic:
by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ¬∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s

Tactic:
simpa [leftLim_eq_of_not_tendsto _ h''c] using hu hc

Premises used: leftLim_eq_of_not_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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
neg : ∀ᶠ (x : α) in 𝓝[<] c, f x ∈ s
⊢ leftLim f c ∈ id s

Tactic:
apply s_closed.mem_of_tendsto (tendsto_leftLim_of_tendsto h''c)

Premises used: tendsto_leftLim_of_tendsto, IsClosed.mem_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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
d : α
hd : d ∈ Ioo u a
⊢ f d ∈ s

Tactic:
hu hd

Premises used: Set.Mem, setOf
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ (y : β), Tendsto f (𝓝[<] c) (𝓝 y)
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α | x ∈ Ioo u a → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x} a_1
h₂ h₃ : ∀ (d : α) (hd : d ∈ Ioo u a), f d ∈ s
⊢ ∀ᶠ (x : α) in 𝓝[<] c, f x ∈ s

Tactic:
filter_upwards [Ioo_mem_nhdsLT_of_mem ⟨hc.1, hc.2.le⟩] with d hd using hu hd

Premises used: LT.lt.le, Ioo_mem_nhdsLT_of_mem, And.right, And.left, And.intro
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ leftLim (leftLim f) a = leftLim f a

Tactic:
(continuousWithinAt_leftLim_Iic h).leftLim_eq

Premises used: ContinuousWithinAt.leftLim_eq, continuousWithinAt_leftLim_Iic
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[>] a) (𝓝 (rightLim f a))
⊢ ContinuousWithinAt (rightLim f) (Ici a) a

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

Premises used: Set.Ici, setOf, Function.rightLim, OrderDual, continuousWithinAt_leftLim_Iic
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[>] a) (𝓝 (rightLim f a))
⊢ rightLim (rightLim f) a = rightLim f a

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

Premises used: Function.rightLim, leftLim_leftLim
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
⊢ (Iio a).Nonempty

Tactic:
Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))

Premises used: Filter.nonempty_of_mem, self_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 α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
obtain : ∀ (b : α) (hb : b ∈ Iio a), leftLim (rightLim f) a = leftLim f a
⊢ leftLim (rightLim f) a = leftLim f a

Tactic:
obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))

Premises used: Filter.nonempty_of_mem, Set.Nonempty, self_mem_nhdsWithin, 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
apply : Tendsto (rightLim f) (𝓝[<] a) (𝓝 (leftLim f a))
⊢ leftLim (rightLim f) a = leftLim f a

Tactic:
apply leftLim_eq_of_tendsto (neBot_iff.mp h')

Premises used: Filter.neBot_iff, leftLim_eq_of_tendsto, Iff.mp
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
apply : ∀ (i : Set β), i ∈ 𝓝 (leftLim f a) ∧ IsClosed[inst_1] i → ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id i
⊢ Tendsto (rightLim f) (𝓝[<] a) (𝓝 (leftLim f a))

Tactic:
apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2

Premises used: Iff.mpr, closed_nhds_basis, Filter.HasBasis.tendsto_right_iff, 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 α
inst_4 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s

Tactic:
have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
⊢ ∃ u < a, Ioo u a ⊆ {x : α | f x ∈ s}

Tactic:
simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this

Premises used: mem_nhdsLT_iff_exists_Ioo_subset', Iff.mp
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
obtain : ∀ (u : α) (au : u < a) (hu : Ioo u a ⊆ {x : α | f x ∈ s}), ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s

Tactic:
obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by
    have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
    simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
h₁ : ∀ (c : α) (hc : c ∈ Ioo u a), rightLim f c ∈ id s
⊢ ∀ᶠ (x : α) in 𝓝[<] a, rightLim f x ∈ id s

Tactic:
filter_upwards [Ioo_mem_nhdsLT au] with c hc

Premises used: Ioo_mem_nhdsLT
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h₁ : ∀ (h'c : 𝓝[>] c = ⊥), rightLim f c ∈ id s
h₂ : ∀ (h'c : (𝓝[>] c).NeBot), rightLim f c ∈ id s
⊢ rightLim f c ∈ id s

Tactic:
rcases eq_or_neBot (𝓝[>] c) with h'c | h'c

Premises used: Set.Ioi, nhdsWithin, Filter.eq_or_neBot
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[>] c = ⊥
⊢ rightLim f c ∈ id s

Tactic:
simpa [h'c, rightLim_eq_of_eq_bot] using hu hc

Premises used: rightLim_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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
pos : ∀ (h''c : ¬∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)), rightLim f c ∈ id s
neg : ∀ (h''c : ∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)), rightLim f c ∈ id s
⊢ rightLim f c ∈ id s

Tactic:
by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
-- 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 : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst_1] s
u : α
au : u < a
hu : Ioo u a ⊆ {x : α | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ¬∃ (y : β), Tendsto f (𝓝[>] c) (𝓝 y)
⊢ rightLim f c ∈ id s

Tactic:
simpa [rightLim_eq_of_not_tendsto _ h''c] using hu hc

Premises used: rightLim_eq_of_not_tendsto