case pos
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖

case neg
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
by_cases h : r = 0
no goals
case pos
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
simp [h, zero_smul α x]
case neg
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
case neg
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
refine' le_antisymm (norm_smul_le r x) _
no goals
case neg
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
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]
no goals
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
rw [inv_smul_smul₀ h]
case h
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
gcongr
no goals
case h
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
apply norm_smul_le
no goals
α : Type u_2
β : Type u_1
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]