no goals
α : Type ?u.826990
β : Type ?u.826993
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
⊢ ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]