no goals
𝓕 : Type ?u.1212646
𝕜 : Type ?u.1212649
α : Type u_1
ι : Type ?u.1212655
κ : Type ?u.1212658
E : Type u_2
F : Type ?u.1212664
G : Type ?u.1212667
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 : AntilipschitzWith Kf f
hg : LipschitzWith Kg (g / f)
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
simpa only [Pi.div_apply, mul_div_cancel'_right] using hf.mul_lipschitzWith hg hK