mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mp
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)

pp: case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)

Tactic:
·

Goal state after:
case mp
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)

Tactic:
·

Goal state after:
case mpr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

pp: case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z

Tactic:
·

Goal state after:
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mpr.inl
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)

pp: case mpr.inr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)

Tactic:
·

Goal state after:
case mpr.inl
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case mpr.inr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)

Tactic:
·

Goal state after:
case mpr.inr
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Tactic:
·

Goal state after:
case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)

pp: case right
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
·

Goal state after:
case left
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))

Tactic:
·

Goal state after:
case right
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : OrderClosedTopology α
inst✝² : Preorder β
inst✝¹ : IsDirectedOrder β
inst✝ : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

pp: case inr
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)

pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
·

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I ↦ sSup (a '' I)) '' F.sets)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F

Tactic:
·

Goal state after:
case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I ↦ sSup (a '' I)) '' F.sets) ≤ limsup a F
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) →
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)

pp: case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Tactic:
·

Goal state after:
case mp
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t) →
    ∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t

Tactic:
·

Goal state after:
case mpr
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
x : ↑s
K : ℝ≥0
⊢ (∃ t, (∃ t_1 ∈ 𝓝[s] ↑x, Subtype.val ⁻¹' t_1 ⊆ t) ∧ LipschitzOnWith K f (s ∩ Subtype.val '' t)) →
    ∃ t ∈ 𝓝[s] ↑x, LipschitzOnWith K f t
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
·

Goal state after:
case inl
x : ℝ
h : 0 ≤ x
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
·

Goal state after:
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal

Tactic:
·

Goal state after:
case bot.bot
hy : 0 ≤ ⊥
⊢ (⊥ - ⊥).toENNReal = ⊥.toENNReal - ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ - ↑a✝).toENNReal = ⊥.toENNReal - (↑a✝).toENNReal

Tactic:
·

Goal state after:
case bot.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊥ - ↑a✝).toENNReal = ⊥.toENNReal - (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal

Tactic:
·

Goal state after:
case bot.top
hy : 0 ≤ ⊤
⊢ (⊥ - ⊤).toENNReal = ⊥.toENNReal - ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.bot
a✝ : ℝ
hy : 0 ≤ ⊥
⊢ (↑a✝ - ⊥).toENNReal = (↑a✝).toENNReal - ⊥.toENNReal

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℝ
hy : 0 ≤ ⊥
⊢ (↑a✝ - ⊥).toENNReal = (↑a✝).toENNReal - ⊥.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal

Tactic:
·

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (↑a✝¹ - ↑a✝).toENNReal = (↑a✝¹).toENNReal - (↑a✝).toENNReal
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
⊢ ClusterPt f.limsSup f

pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Subsingleton α
⊢ ClusterPt f.limsSup f

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
⊢ ClusterPt f.limsSup f
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∀ (x : α), x ≤ f.limsSup
⊢ ClusterPt f.limsSup f

pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
⊢ ClusterPt f.limsSup f

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∀ (x : α), x ≤ f.limsSup
⊢ ClusterPt f.limsSup f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top
a✝ : ℝ
hy : 0 ≤ ⊤
⊢ (↑a✝ - ⊤).toENNReal = (↑a✝).toENNReal - ⊤.toENNReal

Tactic:
·

Goal state after:
case coe.top
a✝ : ℝ
hy : 0 ≤ ⊤
⊢ (↑a✝ - ⊤).toENNReal = (↑a✝).toENNReal - ⊤.toENNReal
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
⊢ ClusterPt f.limsSup f

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
⊢ ClusterPt f.limsSup f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal

Tactic:
·

Goal state after:
case top.bot
hy : 0 ≤ ⊥
⊢ (⊤ - ⊥).toENNReal = ⊤.toENNReal - ⊥.toENNReal
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
⊢ ClusterPt f.limsSup f

pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∃ x, x < f.limsSup
⊢ ClusterPt f.limsSup f

Tactic:
·

Goal state after:
case pos
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∀ (x : α), f.limsSup ≤ x
⊢ ClusterPt f.limsSup f
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∃ x, x < f.limsSup
⊢ ClusterPt f.limsSup f

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∃ x, x < f.limsSup
⊢ ClusterPt f.limsSup f
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
⊢ LipschitzWith (List.map K []).prod (List.map f []).prod

Tactic:
by simpa using! LipschitzWith.id

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ - ↑a✝).toENNReal = ⊤.toENNReal - (↑a✝).toENNReal

Tactic:
·

Goal state after:
case top.coe
a✝ : ℝ
hy : 0 ≤ ↑a✝
⊢ (⊤ - ↑a✝).toENNReal = ⊤.toENNReal - (↑a✝).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal

Tactic:
·

Goal state after:
case top.top
hy : 0 ≤ ⊤
⊢ (⊤ - ⊤).toENNReal = ⊤.toENNReal - ⊤.toENNReal
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Subsingleton α
⊢ ClusterPt f.limsSup f

Tactic:
·

Goal state after:
case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Subsingleton α
⊢ ClusterPt f.limsSup f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
·

Goal state after:
case pos
x y : ℝ
hy : 0 ≤ ↑y
hxy : x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
·

Goal state after:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ (↑x - ↑y).toENNReal = (↑x).toENNReal - (↑y).toENNReal
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ Tendsto u ⊥ (𝓝 a)

pp: case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ Tendsto u ⊥ (𝓝 a)
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
·

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)

pp: case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
hbot : f.NeBot
⊢ ∃ c, Tendsto u f (𝓝 c)

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
b : ℝ
⊢ ↑b + a - ↑b = a

Tactic:
add_sub_cancel_left

Goal state after:
a : EReal
b : ℝ
⊢ a = a
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
hι : IsEmpty ι
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)

pp: case inr
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)

Tactic:
·

Goal state after:
case inl
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
hι : IsEmpty ι
⊢ Tendsto (fun r ↦ ⨆ i, u i r) atTop (𝓝 c)