Radial Angular Measure closed Ball

@[simp]lemma radialAngularMeasure_closedBall (r : ℝ) :    radialAngularMeasure (Metric.closedBall (0 : Space 3) r) = ENNReal.ofReal (4 * π * r) := by  rw [← setLIntegral_one, ← MeasureTheory.lintegral_indicator measurableSet_closedBall,    lintegral_radialMeasure_eq_spherical_mul _ _    ((measurable_indicator_const_iff 1).mpr measurableSet_closedBall)]  have h1 (x : (Metric.sphere (0 : Space) 1) × ↑(Set.Ioi (0 : ℝ))) :      (Metric.closedBall (0 : Space) r).indicator (fun x => (1 : ENNReal)) (x.2.1 • x.1.1) =      (Set.univ ×ˢ {a | a.1 ≤ r}).indicator (fun x => 1) x :=      Set.indicator_const_eq_indicator_const <| by    simp [norm_smul]    rw [abs_of_nonneg (le_of_lt x.2.2)]  simp [h1]  rw [MeasureTheory.lintegral_indicator <|    MeasurableSet.prod MeasurableSet.univ (measurableSet_setOf.mpr (by fun_prop))]  simp [MeasureTheory.Measure.prod_prod, Measure.volumeIoiPow]  rw [MeasureTheory.Measure.comap_apply _ Subtype.val_injective    (fun s hs => MeasurableSet.subtype_image measurableSet_Ioi hs)    _ (measurableSet_setOf.mpr (by fun_prop))]  trans 3 * ENNReal.ofReal (4 / 3 * π) * volume (α := ℝ) (Set.Ioc 0 r)  · congr    ext x    simp only [Set.mem_image, Set.mem_setOf_eq, Subtype.exists, Set.mem_Ioi, exists_and_left,      exists_prop, exists_eq_right_right, Set.mem_Ioc]    grind  simp only [volume_Ioc, sub_zero]  trans ENNReal.ofReal (3 * ((4 / 3 * π))) * ENNReal.ofReal r  · simp [ENNReal.ofReal_mul]  field_simp  rw [← ENNReal.ofReal_mul (by positivity)]