mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
inst✝ : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
⊢ multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ blimsup u f p = ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b

Tactic:
by

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

Goal state before:
pp: x : EReal
h_top : x ≠ ⊤
h_bot : x ≠ ⊥
⊢ x - x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ blimsup u atTop p = ⨅ i, ⨆ j, ⨆ (_ : p j ∧ i ≤ j), u j

Tactic:
by

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

Goal state before:
pp: x : EReal
⊢ x - x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s t : Set α
f : α → β
hf : LocallyLipschitzOn t f
h : s ⊆ t
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzOnWith K f univ ↔ LipschitzWith K f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ LocallyLipschitzOn univ f ↔ LocallyLipschitz f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (s.domRestrict f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
t : Set ↑s
⊢ LipschitzOnWith K (s.domRestrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: ι : 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)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
s : Set α
f : α → β
⊢ LocallyLipschitzOn s f ↔ LocallyLipschitz (s.domRestrict f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x

Tactic:
by

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

Goal state before:
pp: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ x - y ↔ y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ edist (f x) (f y) < ↑K * r

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ x - y ≤ 0 ↔ x ≤ y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
x y : α
h : edist x y ≠ ∞
⊢ ↑K * edist x y < ∞

Tactic:
by

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

Goal state before:
pp: x y : EReal
⊢ 0 < x - y ↔ y < x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ f (limsup (fun n ↦ (⇑f)^[n] a) atTop) = limsup (fun n ↦ (⇑f)^[n] a) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → a ≤ u x}
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), p x ∧ q x → p x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), p x ∧ q x → q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), p x → p x ∨ q x

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (x : β), q x → p x ∨ q x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y
x y : α
⊢ edist (f x) (f y) ≤ ↑1 * edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ e (blimsup u f p) = blimsup (⇑e ∘ u) f p

Tactic:
by

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

Goal state before:
pp: x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ x - y < 0 ↔ x < y

Tactic:
by

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

Goal state before:
pp: x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -t ≠ ⊥

Tactic:
by

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

Goal state before:
pp: x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -z ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ g (blimsup u f p) ≤ blimsup (⇑g ∘ u) f p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ediam (f '' s) ≤ ↑K * ediam s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
x y : α
⊢ edist ((fun x ↦ b) x) ((fun x ↦ b) y) ≤ ↑0 * edist x y

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
K : ℝ≥0
x y : α
⊢ edist ((fun x ↦ b) x) ((fun x ↦ b) y) ≤ ↑K * edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_1
inst✝ : EMetricSpace β
f : α → β
⊢ LipschitzWith 0 f ↔ ∀ (x y : α), f x = f y

Tactic:
by

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

Goal state before:
pp: x y : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
hy : y ≠ ⊤
h'y : y ≠ ⊥
⊢ (x - y).toReal = x.toReal - y.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: ι : Type x
α : ι → Type u
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : Fintype ι
i : ι
f g : (x : ι) → α x
⊢ edist (eval i f) (eval i g) ≤ edist f g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
⊢ ↑Kf * (↑Kg * edist x y) = ↑(Kf * Kg) * edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ limsup u (f ⊔ g) = limsup u f ⊔ limsup u g

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ p x ∨ q x) = blimsup u f p ⊔ blimsup u f q

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f p ⊔ blimsup u f fun x ↦ ¬p x) = limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ ¬p x) ⊔ blimsup u f p = limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : BoundedLENhdsClass α
inst✝ : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
⊢ BoundedLENhdsClass (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x ↦ (f x, g x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
a : α
⊢ LipschitzWith 1 (Prod.mk a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
a✝ : β
h : a✝ ∈ s
⊢ s.piecewise u v a✝ = u a✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
⊢ LipschitzWith 1 fun a ↦ (a, b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst✝⁹ : Preorder α
inst✝⁸ : Preorder β
inst✝⁷ : TopologicalSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : BoundedLENhdsClass α
inst✝⁴ : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
inst✝³ : Finite ι
inst✝² : (i : ι) → Preorder (π i)
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), BoundedLENhdsClass (π i)
⊢ BoundedLENhdsClass ((i : ι) → π i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
a✝ : β
h : a✝ ∉ s
⊢ s.piecewise u v a✝ = v a✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
⊢ LipschitzWith (Kα + Kβ) (uncurry f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
⊢ LipschitzWith (K ^ 0) f^[0]

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
⊢ limsup (s.piecewise u v) f = (blimsup u f fun x ↦ x ∈ s) ⊔ blimsup v f fun x ↦ x ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) f^[n + 1]

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n

Tactic:
by

Goal state after:
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

Goal state after:
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)
i : ι
l : List ι
⊢ LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
⊢ LipschitzWith (K ^ 0) (f ^ 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : 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
⊢ ClusterPt f.limsSup f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝¹ : PseudoEMetricSpace α
s : Set α
β : Type u_1
inst✝ : EMetricSpace β
f : α → β
⊢ LipschitzOnWith 0 f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y

Tactic:
by

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

Goal state before:
pp: x y : EReal
hy : 0 ≤ y
⊢ (x - y).toENNReal = x.toENNReal - y.toENNReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter α
x : α
hx : ClusterPt x f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
⊢ x ≤ f.limsSup

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a ⊔ limsup u f = limsup (fun x ↦ a ⊔ u x) f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : 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
⊢ Tendsto u f (𝓝 a)

Tactic:
by

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

Goal state before:
pp: a b c d : EReal
h1 : c ≠ ⊥ ∨ d ≠ ⊤
h2 : c ≠ ⊤ ∨ d ≠ ⊥
⊢ a + b - (c + d) = a - c + (b - d)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (max Kf Kg) (fun x ↦ (f x, g x)) s

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x ↦ a ⊔ u x) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (limsup u f)ᶜ = liminf (compl ∘ u) f

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (liminf u f)ᶜ = limsup (compl ∘ u) f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b c : EReal
hb : b ≠ ⊥ ∨ c ≠ ⊥
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - b ↔ a + b ≤ c

Tactic:
by

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

Goal state before:
pp: a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
this : a + -b ≤ c ↔ a ≤ c - -b
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : 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
⊢ ∃ c, Tendsto u f (𝓝 c)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup u f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
⊢ Metric.ediam (image2 f s t) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz (f ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b ↦ u b \ a) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ liminf u f \ a = liminf (fun b ↦ u b \ a) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a \ limsup u f = liminf (fun b ↦ a \ u b) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b ↦ a \ u b) f

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
x✝ : ∃ i, ∃ (_ : i ∈ 𝓕), ∀ i_1 ∈ i, a ∈ s i_1
S : Set ι
hS : S ∈ 𝓕
hS' : ∀ i ∈ S, a ∈ s i
⊢ S ⊆ {x | (fun i ↦ a ∈ s i) x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
h : ∀ᶠ (i : ι) in 𝓕, a ∈ s i
⊢ ∀ i ∈ {i | a ∈ s i}, a ∈ s i

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ (f x, g x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
⊢ LocallyLipschitz f^[0]

Tactic:
by

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

Goal state before:
pp: a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
by

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz f^[n + 1]

Tactic:
by

Goal state after: