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 α
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)
neg : ∀ᶠ (x : α) in 𝓝[>] c, f x ∈ s
⊢ rightLim f c ∈ id s

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

Premises used: IsClosed.mem_of_tendsto, tendsto_rightLim_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))
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)
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))
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)
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_nhdsGT_of_mem ⟨hc.1.le, hc.2⟩] with d hd using hu hd

Premises used: LT.lt.le, And.right, And.left, And.intro, Ioo_mem_nhdsGT_of_mem
-- 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))
h' : (𝓝[>] a).NeBot
⊢ rightLim (leftLim f) a = rightLim f a

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

Premises used: Function.rightLim, leftLim_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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
inl : ∀ (hα : IsEmpty α), Tendsto g atTop (𝓝 b)
inr : ∀ (hα : Nonempty α), Tendsto g atTop (𝓝 b)
⊢ Tendsto g atTop (𝓝 b)

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : IsEmpty α
⊢ Tendsto g atTop (𝓝 b)

Tactic:
simp [filter_eq_bot_of_isEmpty atTop]

Premises used: Filter.atTop, Filter.filter_eq_bot_of_isEmpty
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
inr : ∀ (i : Set β), i ∈ 𝓝 b ∧ IsClosed[inst_1] i → ∀ᶠ (x : α) in atTop, g x ∈ id i
⊢ Tendsto g atTop (𝓝 b)

Tactic:
apply (closed_nhds_basis b).tendsto_right_iff.2

Premises used: Iff.mpr, closed_nhds_basis, Filter.HasBasis.tendsto_right_iff
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
⊢ ∃ (a : α), ∀ (b : α), a ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s

Tactic:
simpa [eventually_atTop] using h'.and (h s_mem)

Premises used: Filter.Eventually.and, Filter.eventually_atTop
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
inr : ∀ (u : α) (hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s), ∀ᶠ (x : α) in atTop, g x ∈ id s
⊢ ∀ᶠ (x : α) in atTop, g x ∈ id s

Tactic:
obtain ⟨u, hu⟩ : ∃ a, ∀ (b : α), a ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s := by
    simpa [eventually_atTop] using h'.and (h s_mem)
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
h₁ : ∀ (ha : u < a), g a ∈ id s
⊢ a ∈ Ioi u → g a ∈ id s

Tactic:
(ha : u < a)
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
h₁ : ∀ (a : α) (ha : u < a), g a ∈ id s
⊢ ∀ᶠ (x : α) in atTop, g x ∈ id s

Tactic:
filter_upwards [Ioi_mem_atTop u] with a (ha : u < a)

Premises used: Filter.Ioi_mem_atTop
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
h₁ : ∀ᶠ (x : α) in 𝓝 a, f x ∈ s
⊢ g a ∈ id s

Tactic:
apply s_closed.mem_of_mapClusterPt (hu a ha.le).1

Premises used: LT.lt.le, And.left, IsClosed.mem_of_mapClusterPt
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
y : α
hy : y ∈ Ici u
⊢ f y ∈ s

Tactic:
(hu y hy).2

Premises used: And.right
-- 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 β
inst_5 : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst_1] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α) {x : α | x ∈ Ici u → Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ s) x} x}
      a
h₂ h₃ : ∀ (y : α) (hy : y ∈ Ici u), f y ∈ s
⊢ ∀ᶠ (x : α) in 𝓝 a, f x ∈ s

Tactic:
filter_upwards [Ici_mem_nhds ha] with y hy using (hu y hy).2

Premises used: Ici_mem_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 β
inst_5 : NoBotOrder α
f g : α → β
b : β
h : Tendsto f atBot (𝓝 b)
h' : ∀ᶠ (x : α) in atBot, MapClusterPt (g x) (𝓝 x) f
⊢ Tendsto g atBot (𝓝 b)

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

Premises used: setOf, tendsto_atTop_of_mapClusterPt, Filter.atBot, Set.Iic, 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 : NoTopOrder α
inst_5 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
apply : ∀ (x : α), MapClusterPt (leftLim f x) (𝓝 x) f
⊢ Tendsto (leftLim f) atTop (𝓝 b)

Tactic:
apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))

Premises used: Filter.Eventually.of_forall, tendsto_atTop_of_mapClusterPt
-- 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 : NoTopOrder α
inst_5 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
x : α
⊢ MapClusterPt (leftLim f x) (𝓝 x) f

Tactic:
MapClusterPt.mono (mapClusterPt_leftLim _ _) nhdsWithin_le_nhds

Premises used: mapClusterPt_leftLim, nhdsWithin_le_nhds, MapClusterPt.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 : NoTopOrder α
inst_5 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
x : α
⊢ MapClusterPt (leftLim f x) (𝓝 x) f

Tactic:
exact MapClusterPt.mono (mapClusterPt_leftLim _ _) nhdsWithin_le_nhds

Premises used: mapClusterPt_leftLim, nhdsWithin_le_nhds, MapClusterPt.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 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
inl : ∀ (val : OrderTop α), Tendsto (rightLim f) atTop (𝓝 b)
inr : NoTopOrder α → Tendsto (rightLim f) atTop (𝓝 b)
⊢ Tendsto (rightLim f) atTop (𝓝 b)

Tactic:
cases topOrderOrNoTopOrder α

Premises used: topOrderOrNoTopOrder
-- 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 : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val : OrderTop α
inl : ∀ (h : Tendsto f (pure ⊤) (𝓝 b)), Tendsto (rightLim f) (pure ⊤) (𝓝 b)
⊢ Tendsto (rightLim f) atTop (𝓝 b)

Tactic:
simp only [OrderTop.atTop_eq α] at h ⊢

Premises used: Filter.OrderTop.atTop_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 : T3Space β
f : α → β
b : β
val : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
⊢ rightLim f ⊤ = f ⊤

Tactic:
have : f.rightLim ⊤ = f ⊤ := rightLim_eq_of_isTop isTop_top
-- 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 : α → β
b : β
val : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
this : rightLim f ⊤ = f ⊤
inl : Tendsto (rightLim f) (pure ⊤) (𝓝 (rightLim f ⊤))
⊢ Tendsto (rightLim f) (pure ⊤) (𝓝 b)

Tactic:
rw [tendsto_nhds_unique h (tendsto_pure_nhds f ⊤), ← this]

Premises used: tendsto_pure_nhds, Top.top, tendsto_nhds_unique
-- 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 : α → β
b : β
val : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
this : rightLim f ⊤ = f ⊤
⊢ Tendsto (rightLim f) (pure ⊤) (𝓝 (rightLim f ⊤))

Tactic:
apply tendsto_pure_nhds

Premises used: 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 : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val : NoTopOrder α
apply : ∀ (x : α), MapClusterPt (rightLim f x) (𝓝 x) f
⊢ Tendsto (rightLim f) atTop (𝓝 b)

Tactic:
apply tendsto_atTop_of_mapClusterPt h (Eventually.of_forall (fun x ↦ ?_))

Premises used: Filter.Eventually.of_forall, tendsto_atTop_of_mapClusterPt
-- 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 : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val : NoTopOrder α
x : α
⊢ MapClusterPt (rightLim f x) (𝓝 x) f

Tactic:
MapClusterPt.mono (mapClusterPt_rightLim _ _) nhdsWithin_le_nhds

Premises used: mapClusterPt_rightLim, nhdsWithin_le_nhds, MapClusterPt.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 : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
val : NoTopOrder α
x : α
⊢ MapClusterPt (rightLim f x) (𝓝 x) f

Tactic:
exact MapClusterPt.mono (mapClusterPt_rightLim _ _) nhdsWithin_le_nhds

Premises used: mapClusterPt_rightLim, nhdsWithin_le_nhds, MapClusterPt.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 : NoBotOrder α
inst_5 : T3Space β
f : α → β
b : β
h : Tendsto f atBot (𝓝 b)
⊢ Tendsto (rightLim f) atBot (𝓝 b)

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

Premises used: setOf, Function.rightLim, Filter.atBot, Set.Iic, OrderDual, tendsto_leftLim_atTop_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 : α → β
b : β
h : Tendsto f atBot (𝓝 b)
⊢ Tendsto (leftLim f) atBot (𝓝 b)

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

Premises used: setOf, Function.rightLim, tendsto_rightLim_atTop_of_tendsto, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : 𝓝[<] x ≠ ⊥
⊢ leftLim f x = sSup (f '' Iio x)

Tactic:
leftLim_eq_of_tendsto h (hf.tendsto_nhdsLT x)

Premises used: Monotone.tendsto_nhdsLT, leftLim_eq_of_tendsto
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : 𝓝[>] x ≠ ⊥
⊢ rightLim f x = sInf (f '' Ioi x)

Tactic:
rightLim_eq_of_tendsto h (hf.tendsto_nhdsGT x)

Premises used: Monotone.tendsto_nhdsGT, rightLim_eq_of_tendsto
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this : TopologicalSpace α := Preorder.topology α
⊢ OrderTopology α

Tactic:
haveI : OrderTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
inl : ∀ (h' : 𝓝[<] x = ⊥), leftLim f x ≤ f y
inr : ∀ (h' : 𝓝[<] x ≠ ⊥), leftLim f x ≤ f y
⊢ leftLim f x ≤ f y

Tactic:
rcases eq_or_ne (𝓝[<] x) ⊥ 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 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ leftLim f x ≤ f y

Tactic:
simpa [leftLim, h'] using hf h

Premises used: Function.leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
⊢ (𝓝[<] x).NeBot

Tactic:
haveI A : NeBot (𝓝[<] x) := neBot_iff.2 h'
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
inr : sSup (f '' Iio x) ≤ f y
⊢ leftLim f x ≤ f y

Tactic:
rw [leftLim_eq_sSup hf h']

Premises used: Monotone.leftLim_eq_sSup
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ sSup (f '' Iio x) ≤ f y

Tactic:
csSup_le ?_ ?_

Premises used: csSup_le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
inr : (f '' Iio x).Nonempty
inr₁ : ∀ b ∈ f '' Iio x, b ≤ f y
⊢ sSup (f '' Iio x) ≤ f y

Tactic:
refine csSup_le ?_ ?_

Premises used: csSup_le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
inr : (Iio x).Nonempty
⊢ (f '' Iio x).Nonempty

Tactic:
simp only [image_nonempty]

Premises used: Set.image_nonempty
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ (Iio x).Nonempty

Tactic:
(forall_mem_nonempty_iff_neBot.2 A) _ self_mem_nhdsWithin

Premises used: Iff.mpr, Filter.forall_mem_nonempty_iff_neBot, self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
⊢ (Iio x).Nonempty

Tactic:
exact (forall_mem_nonempty_iff_neBot.2 A) _ self_mem_nhdsWithin

Premises used: Iff.mpr, Filter.forall_mem_nonempty_iff_neBot, self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
inr : ∀ a < x, f a ≤ f y
⊢ ∀ b ∈ f '' Iio x, b ≤ f y

Tactic:
simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: Set.mem_Iio, and_imp, Set.mem_image, forall_exists_index, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
z : α
hz : z < x
⊢ f z ≤ f y

Tactic:
hf (hz.le.trans h)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
A : (𝓝[<] x).NeBot
z : α
hz : z < x
⊢ f z ≤ f y

Tactic:
exact hf (hz.le.trans h)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ OrderTopology α

Tactic:
haveI : OrderTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
inl : ∀ (h' : 𝓝[<] y = ⊥), f x ≤ leftLim f y
inr : ∀ (h' : 𝓝[<] y ≠ ⊥), f x ≤ leftLim f y
⊢ f x ≤ leftLim f y

Tactic:
rcases eq_or_ne (𝓝[<] y) ⊥ 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 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
inl : f x ≤ f y
⊢ f x ≤ leftLim f y

Tactic:
rw [leftLim_eq_of_eq_bot _ h']

Premises used: leftLim_eq_of_eq_bot
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
⊢ f x ≤ f y

Tactic:
hf h.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
⊢ f x ≤ f y

Tactic:
exact hf h.le

Premises used: LT.lt.le