no goals
α : Type u_1
β : Type ?u.3495308
γ : Type ?u.3495311
δ : Type ?u.3495314
ι : Type ?u.3495317
R : Type ?u.3495320
R' : Type ?u.3495323
inst✝ : MeasurableSpace α
⊢ toMeasure 0 (_ : inst✝ ≤ OuterMeasure.caratheodory 0) = 0
rw [← Measure.measure_univ_eq_zero, toMeasure_apply _ _ MeasurableSet.univ,
  OuterMeasure.coe_zero, Pi.zero_apply]