mathlib-initiative/mathlib-tactics huggingface dataset:
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 α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x : α
y₁ y₂ : β
⊢ dist (MulOpposite.op x • y₁) (MulOpposite.op x • y₂) ≤ dist (MulOpposite.op x) 0 * dist y₁ y₂

Tactic:
by

Goal state after:
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 α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x₁ x₂ : α
y : β
⊢ dist (MulOpposite.op x₁ • y) (MulOpposite.op x₂ • y) ≤ dist (MulOpposite.op x₁) (MulOpposite.op x₂) * dist y 0

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : Type u_4
β : ι → Type u_5
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : Zero α
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul α (β i)
x : α
y₁ y₂ : (i : ι) → β i
⊢ 0 ≤ dist x 0 * dist y₁ y₂

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : Type u_4
β : ι → Type u_5
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : Zero α
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul α (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul α (β i)
x₁ x₂ : α
y : (i : ι) → β i
⊢ 0 ≤ dist x₁ x₂ * dist y 0

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : (i : ι) → PseudoMetricSpace (α i)
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul (α i) (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul (α i) (β i)
x : (i : ι) → α i
y₁ y₂ : (i : ι) → β i
⊢ 0 ≤ dist x 0 * dist y₁ y₂

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝⁸ : PseudoMetricSpace α✝
inst✝⁷ : PseudoMetricSpace β✝
ι : Type u_3
inst✝⁶ : Fintype ι
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : (i : ι) → PseudoMetricSpace (α i)
inst✝⁴ : (i : ι) → PseudoMetricSpace (β i)
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMul (α i) (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul (α i) (β i)
x₁ x₂ : (i : ι) → α i
y : (i : ι) → β i
⊢ 0 ≤ dist x₁ x₂ * dist y 0

Tactic:
by

Goal state after:
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
s : Set E
a✝ b✝ : E
r : ℝ
a b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
by

Goal state after:
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
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
by

Goal state after:
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✝¹ : IsometryClass 𝓕 E F
inst✝ : OneHomClass 𝓕 E F
f : 𝓕
x : E
⊢ ‖f x‖ₑ = ‖x‖ₑ

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist b (b * a) = ‖a‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist (b * a) b = ‖a‖

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzOnWith C f s
ha : a ∈ s
hb : b ∈ s
hr : ‖a⁻¹ * b‖ ≤ r
⊢ ↑C * ‖a⁻¹ * b‖ ≤ ↑C * r

Tactic:
by

Goal state after:
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
C : ℝ≥0
⊢ LipschitzWith C f ↔ ∀ (x y : E), ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
a b : E
r : ℝ
f : E → F
C : ℝ≥0
h : LipschitzWith C f
hr : ‖a⁻¹ * b‖ ≤ r
⊢ ↑C * ‖a⁻¹ * b‖ ≤ ↑C * r

Tactic:
by

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

Goal state before:
pp: M : Type u
G : Type v
X : Type w
inst✝⁴ : PseudoEMetricSpace X
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : IsIsometricSMul M X
c : Mᵐᵒᵖ
x y : X
⊢ edist ((fun x ↦ c • x) x) ((fun x ↦ c • x) y) = edist x y

Tactic:
by

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

Goal state before:
pp: M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoEMetricSpace M
inst✝ : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ edist (a / c) (b / c) = edist a b

Tactic:
by

Goal state after:
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 : 𝓕
⊢ Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
⊢ edist a⁻¹ b⁻¹ = edist a b

Tactic:
by

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

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹ y = edist x y⁻¹

Tactic:
by

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

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a / b) (a / c) = edist b c

Tactic:
by

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

Goal state after:
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 : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
⊢ (↑K + 1)⁻¹ > 0

Tactic:
by

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x ↦ c • x) ⁻¹' eball x r = eball (c⁻¹ • x) r

Tactic:
by

Goal state after:
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 : 𝓕
x✝ : ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
c : ℝ
hc0 : c > 0
hc : ∀ (x : E), c * ‖x‖ ≤ ‖f x‖
⊢ 0 ≤ c⁻¹

Tactic:
by

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoEMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ≥0∞
⊢ (fun x ↦ c • x) ⁻¹' closedEBall x r = closedEBall (c⁻¹ • x) r

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' eball b r = eball (b / a) r

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b / a) r

Tactic:
by

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

Goal state before:
pp: M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ dist (a / c) (b / c) = dist a b

Tactic:
by

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

Goal state before:
pp: M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ nndist (a / c) (b / c) = nndist a b

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ dist (a / b) (a / c) = dist b c

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ nndist (a / b) (a / c) = nndist b c

Tactic:
by

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r

Tactic:
by

Goal state after:
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 : 𝓕
x✝ : ∃ K, AntilipschitzWith K ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f
x : E
⊢ (↑K + 1)⁻¹ * ↑K ≤ 1

Tactic:
by

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r

Tactic:
by

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
by

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

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Tactic:
by

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

Goal state before:
pp: M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsIsometricSMul M X
c : M
x y : Xᵐᵒᵖ
⊢ edist ((fun x ↦ c • x) x) ((fun x ↦ c • x) y) = edist x y

Tactic:
by

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

Goal state before:
pp: M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsIsometricSMul M X
c : ULift.{u_2, u} M
⊢ Isometry fun x ↦ c • x

Tactic:
by

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

Goal state before:
pp: M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsIsometricSMul M X
c : M
x y : ULift.{u_2, w} X
⊢ edist ((fun x ↦ c • x) x) ((fun x ↦ c • x) y) = edist x y

Tactic:
by

Goal state after:
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, AntilipschitzWith K ⇑f) ↔ ∃ c > 0, ∀ (x : E), c * ‖x‖ ≤ ‖f x‖

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a₁ a₂ b₁ b₂ : E
r₁ r₂ : ℝ
a : Eᵐᵒᵖ
b c : E
⊢ dist (a • b) (a • c) = dist b c

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (b * a) = ‖b‖

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ s.sup' hs f * a = s.sup' hs fun i ↦ f i * a

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (b * a) a = ‖b‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (a / b) = ‖b‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist (a / b) a = ‖b‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist (a / b) c = dist a (c * b)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist a (b / c) = dist (a * c) b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : PosMulReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ a * s.sup' hs f = s.sup' hs fun i ↦ a * f i

Tactic:
by

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

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

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
a : G₀
inst✝ : MulPosReflectLT G₀
ha : 0 ≤ a
f : ι → G₀
s : Finset ι
hs : s.Nonempty
⊢ s.sup' hs f / a = s.sup' hs fun i ↦ f i / a

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
⊢ s.sup f / a = s.sup fun i ↦ f i / a

Tactic:
by

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

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

Tactic:
by

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 α
K : ℝ≥0
f : α → E
⊢ LipschitzWith K f⁻¹ ↔ LipschitzWith K f

Tactic:
by

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 α
K : ℝ≥0
f : α → E
⊢ AntilipschitzWith K f⁻¹ ↔ AntilipschitzWith K f

Tactic:
by

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 α
K : ℝ≥0
f : α → E
s : Set α
⊢ LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s

Tactic:
by

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 α
f : α → E
⊢ LocallyLipschitz f⁻¹ ↔ LocallyLipschitz f

Tactic:
by

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 α
f : α → E
s : Set α
⊢ LocallyLipschitzOn s f⁻¹ ↔ LocallyLipschitzOn s f

Tactic:
by

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 : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x ↦ f x * g x

Tactic:
by

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 α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x ↦ f x * g x) t

Tactic:
by

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 α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ f x * g x

Tactic:
by

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
s : Set α
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf + Kg) (fun x ↦ f x / g x) s

Tactic:
by

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 : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x ↦ f x / g x

Tactic:
by

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 α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
⊢ LocallyLipschitzOn s fun x ↦ f x / g x

Tactic:
by

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 α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x ↦ f x / g x

Tactic:
by

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
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x ↦ f x * g x

Tactic:
by

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:
by

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedCommGroup F
E : Type u_5
inst✝ : SeminormedCommGroup E
K : ℝ≥0
f : E → F
hf : AntilipschitzWith K f
x y : E
⊢ ‖x⁻¹ * y‖ ≤ ↑K * ‖(f x)⁻¹ * f y‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
p : E
⊢ mk p = 1 ↔ ‖p‖ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a b : α
⊢ ‖1‖ * ‖1‖ = ‖1‖ * 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a : α
⊢ ↑‖a⁻¹‖₊ = ↑‖a‖₊⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)

Tactic:
by

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

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

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ N + 1 ≤ n + 1

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
⊢ CauchySeq fun n ↦ ∏ k ∈ range (n + 1), u k

Tactic:
by

Goal state after:
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
⊢ ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖

Tactic:
by

Goal state after: