[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
simpa [smul_zero] using dist_smul_pair r 0 x
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y
[PROOFSTEP]
simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
simpa [mul_sub, dist_eq_norm] using norm_mul_le x (y₁ - y₂)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
simpa [sub_mul, dist_eq_norm] using norm_mul_le (x₁ - x₂) y
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x : αᵐᵒᵖ
y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
simpa [sub_mul, dist_eq_norm, mul_comm] using norm_mul_le (y₁ - y₂) x.unop
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ : αᵐᵒᵖ
y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
simpa [mul_sub, dist_eq_norm, mul_comm] using norm_mul_le y (x₁ - x₂).unop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a : α
b₁ b₂ : β
⊢ dist (a • b₁) (a • b₂) ≤ dist a 0 * dist b₁ b₂
[PROOFSTEP]
simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a₁ a₂ : α
b : β
⊢ dist (a₁ • b) (a₂ • b) ≤ dist a₁ a₂ * dist b 0
[PROOFSTEP]
simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
[PROOFSTEP]
by_cases h : r = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
[PROOFSTEP]
simp [h, zero_smul α x]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
[PROOFSTEP]
refine' le_antisymm (norm_smul_le r x) _
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
[PROOFSTEP]
calc
  ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
  _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
  _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
[PROOFSTEP]
rw [inv_smul_smul₀ h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
[PROOFSTEP]
apply norm_smul_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
[PROOFSTEP]
rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y
[PROOFSTEP]
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ edist (s • x) (s • y) = ‖s‖₊ • edist x y
[PROOFSTEP]
simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]
