-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
theorem measurePreserving_homeomorphUnitSphereProd :
    MeasurePreserving (homeomorphUnitSphereProd E) (μ.comap (↑))
      (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Tactic:
have : Ioo (0 : ℝ) r = r.1 • Ioo (0 : ℝ) 1 := by
  rw [LinearOrderedField.smul_Ioo r.2.out, smul_zero, smul_eq_mul, mul_one]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Tactic:
have hpos : 0 < dim E := Module.finrank_pos

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Tactic:
nontriviality E

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Tactic:
rw [(Homeomorph.measurableEmbedding _).map_apply, toSphere_apply' _ hs, volumeIoiPow_apply_Iio,
  comap_subtype_coe_apply (measurableSet_singleton _).compl, toSphere_apply_aux, this,
  smul_assoc, μ.addHaar_smul_of_nonneg r.2.out.le, Nat.sub_add_cancel hpos, Nat.cast_pred hpos,
  sub_add_cancel, mul_right_comm, ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, mul_div_cancel₀]

Result:
case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ ↑(dim E) ≠ 0

E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ 0 ≤ ↑(dim E)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ μ.toSphere.prod (volumeIoiPow (dim E - 1)) = map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)

Tactic:
refine prod_eq_generateFrom generateFrom_measurableSet
  ((borel_eq_generateFrom_Iio _).symm.trans BorelSpace.measurable_eq.symm)
  isPiSystem_measurableSet isPiSystem_Iio
  μ.toSphere.toFiniteSpanningSetsIn (finiteSpanningSetsIn_volumeIoiPow_range_Iio _)
  fun s hs ↦ forall_mem_range.2 fun r ↦ ?_

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
⊢ (map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)) (s ×ˢ Iio r) =
    μ.toSphere s * (volumeIoiPow (dim E - 1)) (Iio r)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ MeasurePreserving (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ) (μ.toSphere.prod (volumeIoiPow (dim E - 1)))

Tactic:
refine ⟨(homeomorphUnitSphereProd E).measurable, .symm ?_⟩

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
⊢ μ.toSphere.prod (volumeIoiPow (dim E - 1)) = map (⇑(homeomorphUnitSphereProd E)) (comap Subtype.val μ)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
⊢ Ioo 0 ↑r = ↑r • Ioo 0 1

Tactic:
rw [LinearOrderedField.smul_Ioo r.2.out, smul_zero, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
case hb
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ ↑(dim E) ≠ 0

E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ 0 ≤ ↑(dim E)

Tactic:
exacts [(Nat.cast_pos.2 hpos).ne', Nat.cast_nonneg _]

Result:
no goals