[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.fst * p.snd) (q.fst * q.snd) ≤ ↑(LipschitzMul.C β) * dist p q
[PROOFSTEP]
rw [← lipschitzWith_iff_dist_le_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd
[PROOFSTEP]
exact lipschitzWith_lipschitz_const_mul_edist
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
s : Submonoid β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd
[PROOFSTEP]
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
s : Submonoid β
x₁ x₂ y₁ y₂ : { x // x ∈ s }
⊢ edist ((fun p => p.fst * p.snd) (x₁, x₂)) ((fun p => p.fst * p.snd) (y₁, y₂)) ≤
    ↑(LipschitzMul.C β) * edist (x₁, x₂) (y₁, y₂)
[PROOFSTEP]
convert lipschitzWith_lipschitz_const_mul_edist ⟨(x₁ : β), x₂⟩ ⟨y₁, y₂⟩ using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ dist (p.fst + p.snd) (q.fst + q.snd) ≤ ↑2 * dist p q
[PROOFSTEP]
simp only [Real.dist_eq, Prod.dist_eq, Prod.fst_sub, Prod.snd_sub, NNReal.coe_ofNat, add_sub_add_comm, two_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.fst - q.fst + (p.snd - q.snd)| ≤ max |p.fst - q.fst| |p.snd - q.snd| + max |p.fst - q.fst| |p.snd - q.snd|
[PROOFSTEP]
refine le_trans (abs_add (p.1 - q.1) (p.2 - q.2)) ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.fst - q.fst| + |p.snd - q.snd| ≤ max |p.fst - q.fst| |p.snd - q.snd| + max |p.fst - q.fst| |p.snd - q.snd|
[PROOFSTEP]
exact add_le_add (le_max_left _ _) (le_max_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzAdd.C ℝ) fun p => p.fst + p.snd
[PROOFSTEP]
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
x₁ x₂ y₁ y₂ : ℝ≥0
⊢ edist ((fun p => p.fst + p.snd) (x₁, x₂)) ((fun p => p.fst + p.snd) (y₁, y₂)) ≤
    ↑(LipschitzAdd.C ℝ) * edist (x₁, x₂) (y₁, y₂)
[PROOFSTEP]
exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
rw [Metric.continuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
⊢ ∀ (b : α × β) (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : α × β), dist a b < δ → dist (a.fst • a.snd) (b.fst • b.snd) < ε
[PROOFSTEP]
rintro ⟨a, b⟩ ε ε0
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (a_1 : α × β), dist a_1 (a, b) < δ → dist (a_1.fst • a_1.snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ δ * (δ + dist b 0) + dist a 0 * δ < ε
[PROOFSTEP]
have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by continuity
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
⊢ Continuous fun δ => δ * (δ + dist b 0) + dist a 0 * δ
[PROOFSTEP]
continuity
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
this : Continuous fun δ => δ * (δ + dist b 0) + dist a 0 * δ
⊢ ∃ δ, δ > 0 ∧ δ * (δ + dist b 0) + dist a 0 * δ < ε
[PROOFSTEP]
refine ((this.tendsto' _ _ ?_).eventually (gt_mem_nhds ε0)).exists_gt
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
this : Continuous fun δ => δ * (δ + dist b 0) + dist a 0 * δ
⊢ 0 * (0 + dist b 0) + dist a 0 * 0 = 0
[PROOFSTEP]
simp
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (a_1 : α × β), dist a_1 (a, b) < δ → dist (a_1.fst • a_1.snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
refine ⟨δ, δ0, fun (a', b') hab' => ?_⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
⊢ dist ((a', b').fst • (a', b').snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
obtain ⟨ha, hb⟩ := max_lt_iff.1 hab'
[GOAL]
case mk.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
⊢ dist ((a', b').fst • (a', b').snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
calc
  dist (a' • b') (a • b) ≤ dist (a' • b') (a • b') + dist (a • b') (a • b) := dist_triangle ..
  _ ≤ dist a' a * dist b' 0 + dist a 0 * dist b' b := (add_le_add (dist_pair_smul _ _ _) (dist_smul_pair _ _ _))
  _ ≤ δ * (δ + dist b 0) + dist a 0 * δ :=
    by
    have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
    mono* <;> apply_rules [dist_nonneg, le_of_lt]
  _ < ε := hδε
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
⊢ dist a' a * dist b' 0 + dist a 0 * dist b' b ≤ δ * (δ + dist b 0) + dist a 0 * δ
[PROOFSTEP]
have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ dist a' a * dist b' 0 + dist a 0 * dist b' b ≤ δ * (δ + dist b 0) + dist a 0 * δ
[PROOFSTEP]
mono*
[GOAL]
case h₁.h₁
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ dist a' a ≤ δ
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₁.c0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ dist b' 0
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₁.b0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ δ
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ dist b' b ≤ δ
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₂.c0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ dist b' b
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₂.b0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ dist a 0
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x y₁ y₂ : ℝ
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
simpa [Real.dist_eq, mul_sub] using (abs_mul x (y₁ - y₂)).le
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x₁ x₂ y : ℝ
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
simpa [Real.dist_eq, sub_mul] using (abs_mul (x₁ - x₂) y).le
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x y₁ y₂ : ℝ≥0
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
convert dist_smul_pair (x : ℝ) (y₁ : ℝ) y₂ using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x₁ x₂ y : ℝ≥0
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
convert dist_pair_smul (x₁ : ℝ) x₂ (y : ℝ) using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : PseudoMetricSpace β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMul α β
inst✝² : BoundedSMul α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x : α
y₁ y₂ : β
⊢ dist (MulOpposite.op x • y₁) (MulOpposite.op x • y₂) ≤ dist (MulOpposite.op x) 0 * dist y₁ y₂
[PROOFSTEP]
simpa only [op_smul_eq_smul] using dist_smul_pair x y₁ y₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : PseudoMetricSpace β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMul α β
inst✝² : BoundedSMul α β
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
[PROOFSTEP]
simpa only [op_smul_eq_smul] using dist_pair_smul x₁ x₂ y
