mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)

Tactic:
by

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

Goal state after:
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
a b : E
r : ℝ
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✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup 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✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
a b : E
r : ℝ
h : LipschitzWith C f
hr : ‖a / b‖ ≤ r
⊢ ↑C * ‖a / b‖ ≤ ↑C * r

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
hx : x ≠ 0
ε : ℝ
εpos : ε > 0
h' : ∀ (y : 𝕜), ‖y‖ < ε → y = 0
H :
  ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] [DiscreteTopology 𝕜] {x : 𝕜},
    x ≠ 0 → (∀ (y : 𝕜), ‖y‖ < ε → y = 0) → ‖x‖ < 1 → ‖x‖ = 1
h✝ : 1 ≤ ‖x‖
h : ‖x⁻¹‖ < 1
⊢ x⁻¹ ≠ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 ↔ x ≠ 0

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
⊢ Metric.closedBall 0 1 = Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ≥0∞
hr : r ≠ ∞
⊢ ∃ x, r < ‖x‖ₑ

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ (𝓝[≠] x).NeBot

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
⊢ (𝓝[{x | IsUnit x}] 0).NeBot

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✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range norm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

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✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range nnnorm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

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
𝕜 : Type u_5
h' : NormedField 𝕜
h : ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∃ x, 1 < ‖x‖

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
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < ‖x‖ ∧ ‖x‖ < x✝

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
⊢ x.toNNReal * ‖y‖₊ = ‖x * y‖₊

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x ↦ ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
⊢ (cobounded E)⁻¹ = cobounded E

Tactic:
by

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

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Tactic:
by

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

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R₀ : ℝ
hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀
⊢ max R₀ 1 > 0

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R : ℝ
hR₀ : R > 0
hR : ∀ x ∈ s, ‖x‖ ≤ R
⊢ R + 1 > 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : SeminormedGroup E
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
u : α → E
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖(u m)⁻¹ * u n‖ < ε

Tactic:
by

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : α →ᵈ β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

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✝¹ : Subsingleton α
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y = 0 ∨ edist x y = ∞

Tactic:
by

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
⊢ ratio f ≠ 0

Tactic:
by

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 : α
⊢ edist (f x) (f y) = ↑(ratio f) * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ nndist (f x) (f y) = ratio f * nndist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ dist (f x) (f y) = ↑(ratio f) * dist x y

Tactic:
by

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

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ edist x y ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ edist (f x) (f y) = ↑r * edist x y

Tactic:
rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ edist (f x) (f y) = ↑r * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f✝ : F
f : α → β
hf : Isometry f
⊢ ∀ (x y : α), edist (f x) (f y) = ↑1 * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ∞
⊢ edist ((Isometry.toDilation f hf) x) ((Isometry.toDilation f hf) y) = ↑1 * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
by
  by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
  · exact ratio_of_trivial hf.toDilation h
  · obtain ⟨x, y, h₁, h₂⟩ := h
    exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

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 : α
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (f x) (f y)

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : FunLike F α✝ β
inst✝¹ : DilationClass F α✝ β
f : F
α : Type ?u.22
inst✝ : PseudoEMetricSpace α
x y : α
⊢ edist (id x) (id y) = ↑1 * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ratio (Dilation.id α) = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f✝ : F
g : β →ᵈ γ
f : α →ᵈ β
x y : α
⊢ edist ((⇑g ∘ ⇑f) x) ((⇑g ∘ ⇑f) y) = ↑(ratio g * ratio f) * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ ≤ A * δ * C

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf : Tendsto f l (𝓝 1)
hg : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (Norm.norm ∘ g)
op : E → F → G
h_op : ∃ A, ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
⊢ Tendsto (fun x ↦ op (f x) (g x)) l (𝓝 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : α
⊢ g (f₁ x) = g (f₂ x)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝³ : SeminormedGroup E
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : DiscreteTopology X
inst✝ : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
⊢ Tendsto (norm ∘ e) Filter.cofinite atTop

Tactic:
by

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
s : Set α
⊢ ediam (⇑f '' s) = ↑(ratio f) * ediam s

Tactic:
by

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
⊢ ediam (range ⇑f) = ↑(ratio f) * ediam univ

Tactic:
by

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

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: 𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst✝³ : SeminormedRing 𝕜₁
inst✝² : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomIsometric σ
x : 𝕜₂
⊢ ‖σ' x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormMulClass α
m : ℕ
hm : m ≠ 0
⊢ Tendsto (fun x ↦ x ^ m) (cobounded α) (cobounded α)

Tactic:
by

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 : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ f y ∈ eball (f x) (↑(ratio f) * r)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
K : Set α
hK1 : IsCompact K
hK2 : ∀ x ∉ K, f x = 1
S : ℝ
hS : S > 0
hS' : ∀ x ∈ K, ‖x‖ ≤ S
⊢ 0 < S + 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖

Tactic:
by

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 : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ ↑(ratio f) * edist y x ≤ ↑(ratio f) * r'

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ Tendsto (fun e ↦ ‖e.1 * e.2 - (fun p ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ diam (⇑f '' s) = ↑(ratio f) * diam s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: ⊢ LipschitzWith 2 fun p ↦ p.1 - p.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m n : ℤ
⊢ ‖m * n‖ ≤ ‖m‖ * ‖n‖

Tactic:
by

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddGroup α
f : α → E
inst✝ : One E
hf : HasCompactMulSupport f
⊢ ∃ R, 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
⊢ ‖1‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
a b : ℤ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a : α
ha : a ≠ 0
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ ≤ ↑‖a‖₊⁻¹ * dist (a * x✝¹) (a * x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a : α
ha : a ≠ 0
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ ≤ ↑‖a‖₊⁻¹ * dist (x✝¹ * a) (x✝ * a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a✝ a : α
ha : a ≠ 0
x y : α
⊢ edist (a * x) (a * y) = ↑‖a‖₊ * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ diam (range ⇑f) = ↑(ratio f) * diam univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a✝ a : α
ha : a ≠ 0
x y : α
⊢ edist (x * a) (y * a) = ↑‖a‖₊ * edist x y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ ↑(ratio f) * dist y x < ↑(ratio f) * r'

Tactic:
by

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 g : X ≃ᵈ Y), ⇑e.toEquiv = ⇑g.toEquiv → ⇑e.symm = ⇑g.symm → e = g

Tactic:
by

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
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : Y), edist (e.symm.toFun x) (e.symm.toFun y) = ↑r * edist x y

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Order.AddTorsor

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝³ : Preorder 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:
by

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
X : Type u_4
inst✝ : PseudoEMetricSpace X
x✝¹ x✝ : X
⊢ edist ((Equiv.refl X).toFun x✝¹) ((Equiv.refl X).toFun x✝) = ↑1 * edist x✝¹ x✝

Tactic:
by

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

Goal state after: