no goals
𝓕 : Type ?u.1207458
𝕜 : Type ?u.1207461
α : Type u_1
ι : Type ?u.1207467
κ : Type ?u.1207470
E : Type u_2
F : Type ?u.1207476
G : Type ?u.1207479
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x => f x / g x
simpa only [div_eq_mul_inv] using hf.mul' hg.inv