𝓕 : Type ?u.85510
𝕜 : Type ?u.85513
α : Type ?u.85516
ι : Type ?u.85519
κ : Type ?u.85522
E : Type u_1
F : Type ?u.85528
G : Type ?u.85531
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖
𝓕 : Type ?u.85510
𝕜 : Type ?u.85513
α : Type ?u.85516
ι : Type ?u.85519
κ : Type ?u.85522
E : Type u_1
F : Type ?u.85528
G : Type ?u.85531
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖u‖ ≤ ‖v‖ + ‖u / v‖
rw [add_comm]
𝓕 : Type ?u.85510
𝕜 : Type ?u.85513
α : Type ?u.85516
ι : Type ?u.85519
κ : Type ?u.85522
E : Type u_1
F : Type ?u.85528
G : Type ?u.85531
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖u‖ = ‖u / v * v‖
𝓕 : Type ?u.85510
𝕜 : Type ?u.85513
α : Type ?u.85516
ι : Type ?u.85519
κ : Type ?u.85522
E : Type u_1
F : Type ?u.85528
G : Type ?u.85531
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖u‖ ≤ ‖u / v‖ + ‖v‖
refine' (norm_mul_le' _ _).trans_eq' _
no goals
𝓕 : Type ?u.85510
𝕜 : Type ?u.85513
α : Type ?u.85516
ι : Type ?u.85519
κ : Type ?u.85522
E : Type u_1
F : Type ?u.85528
G : Type ?u.85531
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : E
⊢ ‖u‖ = ‖u / v * v‖
rw [div_mul_cancel']