mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ ∀ᶠ (x : ℝ≥0∞) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b

Tactic:
simpa using

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
aux : ∀ᶠ (i : ι) in f, (u i).toReal = b.truncateToReal (u i)
aux' : (limsup u f).toReal = b.truncateToReal (limsup u f)
⊢ ∀ᶠ (a : ι) in f, u a ≤ b
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x ↦ max a (f x)

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x ↦ max a (f x)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x ↦ min a (f x)

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x ↦ min a (f x)
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ g x ≤ f x

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty ↑s
g : α → ℝ := fun y ↦ ⨅ x, f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x ↦ f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ g x ≤ f x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: case singleton
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a✝ : ι
hs : ∀ i ∈ {a✝}, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ({a✝}.sup' ⋯ f) l (𝓝 ({a✝}.sup' ⋯ g))

Tactic:
simpa using

Goal state after:
case singleton
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a✝ : ι
hs : ∀ i ∈ {a✝}, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (f a✝) l (𝓝 (g a✝))
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : ∀ i ∈ cons a s ha, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))

Tactic:
forall_mem_cons

Goal state after:
case cons
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s✝ : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
a : ι
s : Finset ι
ha : a ∉ s
hne : s.Nonempty
ihs : (∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) → Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
hs : Tendsto (f a) l (𝓝 (g a)) ∧ ∀ x ∈ s, Tendsto (f x) l (𝓝 (g x))
⊢ Tendsto ((cons a s ha).sup' ⋯ f) l (𝓝 ((cons a s ha).sup' ⋯ g))
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun a ↦ s.sup' hne fun x ↦ f x a) l (𝓝 (s.sup' hne g))

Tactic:
simpa using

Goal state after:
L : Type u_1
inst✝² : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
hne : s.Nonempty
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun a ↦ s.sup' hne f a) l (𝓝 (s.sup' hne g))
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun a ↦ s.sup fun x ↦ f x a) l (𝓝 (s.sup g))

Tactic:
simpa using

Goal state after:
L : Type u_1
inst✝³ : TopologicalSpace L
ι : Type u_3
α : Type u_4
s : Finset ι
f : ι → α → L
l : Filter α
g : ι → L
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))
⊢ Tendsto (fun a ↦ s.sup f a) l (𝓝 (s.sup g))
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup' hne f) x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup' hne f) x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup' hne f) t x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup' hne f) t x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup f) x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup f) x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup f) t x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeSup L
inst✝¹ : OrderBot L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup f) t x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf' hne f) x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf' hne f) x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf' hne f) t x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf' hne f) t x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf f) x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf f) x
Module: Mathlib.Topology.Order.Lattice

Goal state before:
pp: L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf f) t x

Tactic:
simpa using

Goal state after:
L : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace L
inst✝³ : TopologicalSpace X
ι : Type u_3
inst✝² : SemilatticeInf L
inst✝¹ : OrderTop L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.inf f) t x
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : NormedAddCommGroup α
inst✝¹ : Lattice α
inst✝ : HasSolidNorm α
x y : ℤ
h : |x| ≤ |y|
⊢ ‖x‖ ≤ ‖y‖

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : NormedAddCommGroup α
inst✝¹ : Lattice α
inst✝ : HasSolidNorm α
x y : ℤ
h : |x| ≤ |y|
⊢ |x| ≤ |y|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
x y : α
h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
x y₁ y₂ : ℝ
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
x y₁ y₂ : ℝ
⊢ |x * y₁ - x * y₂| ≤ |x| * |y₁ - y₂|
Module: Mathlib.Topology.MetricSpace.Algebra

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
x₁ x₂ y : ℝ
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : IsBoundedSMul α β
x₁ x₂ y : ℝ
⊢ |x₁ * y - x₂ * y| ≤ |x₁ - x₂| * |y|
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
x y : E
⊢ dist (f x) (f y) ≤ C * dist x y

Tactic:
simpa using

Goal state after:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
x y : E
⊢ ‖(f x)⁻¹ * f y‖ ≤ C * ‖x⁻¹ * y‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), ‖f (x⁻¹ * y)‖ = ‖x⁻¹ * y‖
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
simpa using

Goal state after:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
h : ∀ (x y : E), ‖f (x⁻¹ * y)‖ = ‖x⁻¹ * y‖
x : E
⊢ ‖f x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
x y : E
⊢ dist x y ≤ ↑K * dist (f x) (f y)

Tactic:
simpa using

Goal state after:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
K : ℝ≥0
h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
x y : E
⊢ ‖x⁻¹ * y‖ ≤ ↑K * ‖(f x)⁻¹ * f y‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : LipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
simpa using

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : LipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖f x‖ ≤ ↑K * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : AntilipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖x‖ ≤ ↑K * ‖f x‖

Tactic:
simpa using

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : AntilipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖x‖ ≤ ↑K * ‖f x‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
⊢ LipschitzWith 1 norm

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : SeminormedGroup E
⊢ LipschitzWith 1 norm
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ dist (a₁ * a₂⁻¹) (b₁ * b₂⁻¹) ≤ dist a₁ b₁ + dist a₂ b₂
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x ↦ f x * g x

Tactic:
simpa using

Goal state after:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzOnWith (Kf + Kg) (fun x ↦ f x * g x) Set.univ
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ f x * g x

Tactic:
simpa using

Goal state after:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitzOn Set.univ fun x ↦ f x * g x
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ f x * g x

Tactic:
by
  simpa [← locallyLipschitzOn_univ] using hf.locallyLipschitzOn.mul hg.locallyLipschitzOn

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg (g / f)
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

Tactic:
simpa using

Goal state after:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg (g / f)
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖₊ ≤ 2 * ‖a‖₊⁻¹ * ‖b‖₊⁻¹ * ‖a - 1‖₊ * ‖b - 1‖₊
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∀ y ∈ Set.range fun n ↦ ‖u n‖, y ≤ C + ‖u 0‖

Tactic:
simpa using

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∀ (a : ℕ), ‖u a‖ ≤ C + ‖u 0‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Tactic:
simpa using

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
s : Set E
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
⊢ comap norm atTop = cobounded E

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : SeminormedGroup E
⊢ comap norm atTop = cobounded E
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C

Tactic:
simpa using

Goal state after:
E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : SeminormedGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : HasCompactMulSupport f
h'f : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : SeminormedGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : HasCompactMulSupport f
h'f : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: case pos.inr
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
r : ℝ≥0
hne : r ≠ 0
hr : edist (f x) (f y) = ↑r * edist x y
h : edist x y = ∞
⊢ edist (f x) (f y) = ↑1 * edist x y

Tactic:
· simp [hr, h, hne]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ∞
hr : edist (f x) (f y) = ↑r * edist x y
⊢ r = ratio f

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ∞
hr : edist (f x) (f y) = ↑r * edist x y
⊢ r = ratio f
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : HasCompactSupport f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : HasCompactSupport f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : LE G
inst✝² : Preorder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
a b : G
c d : P
h₁ : a ≤ b
h₂ : c < d
⊢ a • c < b • d

Tactic:
refine lt_of_le_of_lt (IsOrderedSMul.smul_le_smul_right a b h₁ c) ?_
  refine lt_of_le_not_ge (IsOrderedSMul.smul_le_smul_left c d (le_of_lt h₂) b) ?_
  by_contra hbdc
  have h : d ≤ c := IsOrderedCancelSMul.le_of_smul_le_smul_left b d c hbdc
  rw [@lt_iff_le_not_ge] at h₂
  simp_all only [not_true_eq_false, and_false]

Goal state after:
Module: Mathlib.Topology.MetricSpace.DilationEquiv

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
⊢ edist (e x) (e y) = 0 ∨ edist (e x) (e y) = ∞

Tactic:
by
      refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]

Goal state after:
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: r : ℝ≥0
s : ℝ≥0∞
⊢ (r • s).toReal = r • s.toReal

Tactic:
rw [ENNReal.smul_def, smul_eq_mul, toReal_mul, coe_toReal]

Goal state after:
r : ℝ≥0
s : ℝ≥0∞
⊢ ↑r * s.toReal = r • s.toReal