no goals
E : Type ?u.231205
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ LipschitzWith 1 ↑equivRealProd
simpa using AddMonoidHomClass.lipschitz_of_bound equivRealProdLm 1 equivRealProd_apply_le'