α : Type ?u.2804
β : Type u_1
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd
α : Type ?u.2804
β : Type u_1
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.fst * p.snd) (q.fst * q.snd) ≤ ↑(LipschitzMul.C β) * dist p q
rw [← lipschitzWith_iff_dist_le_mul]
no goals
α : Type ?u.2804
β : Type u_1
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd
exact lipschitzWith_lipschitz_const_mul_edist