Theorem: helper (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a b : ℝ
⊢ ENNReal.ofReal (a * b) = ENNReal.ofReal a * ENNReal.ofReal b
Tactic:
sorry
State after:
no goals