LipschitzOnWith.of_iLipENorm_ne_top

lemma LipschitzOnWith.of_iLipENorm_ne_top (hφ : iLipENorm φ z R ≠ ⊤) :    LipschitzOnWith (iLipNNNorm φ z R / R.toNNReal) φ (ball z R) := by  intro x hx y hy  have hR : 0 < R := by    simp only [mem_ball] at hx    apply dist_nonneg.trans_lt hx  rcases eq_or_ne x y with rfl | hne  · simp  have : (ENNReal.ofReal R) * (‖φ x - φ y‖ₑ / edist x y) ≤ iLipENorm φ z R := calc      (ENNReal.ofReal R) * (‖φ x - φ y‖ₑ / (edist x y))    _ ≤ (ENNReal.ofReal R) *        ⨆ (x ∈ ball z R) (y ∈ ball z R) (_ : x ≠ y), (‖φ x - φ y‖ₑ / edist x y) := by      gcongr      simp only [ne_eq, le_iSup_iff, iSup_le_iff]      tauto    _ ≤ _ := le_add_self  rw [edist_eq_enorm_sub, ENNReal.coe_div (by simp [hR]), iLipNNNorm, coe_toNNReal hφ]  rw [← ENNReal.div_le_iff_le_mul]; rotate_left  · have : edist x y ≠ 0 := by simp [hne]    simp [this]  · simp [edist_ne_top]  rw [ENNReal.le_div_iff_mul_le]; rotate_left  · simp [hR]  · simp  convert this using 1  simp only [ENNReal.ofReal, mul_comm]