case h.e'_2
ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = ↑↑volume ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = volume
convert (addHaarMeasure_unique volume (piIcc01 ι)).symm
no goals
case h.e'_2
ι : Type u_1
inst✝ : Fintype ι
⊢ addHaarMeasure (piIcc01 ι) = ↑↑volume ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
simp only [piIcc01, volume_pi_pi fun _ => Icc (0 : ℝ) 1, PositiveCompacts.coe_mk,
  Compacts.coe_mk, Finset.prod_const_one, ENNReal.ofReal_one, Real.volume_Icc, one_smul, sub_zero]