-- Module: Mathlib.MeasureTheory.Constructions.HaarToSphere
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
s : Set (↑(sphere 0 1) : Type u_1)
hs : MeasurableSet s
rw :
  (HSMul.hSMul (β := Measure (↑(sphere 0 1) : Type u_1)) (dim E)
          (fst
            (restrict
              (comap
                (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                  (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                  (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                    (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
                μ)
              (SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))))) :
        (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞)
      s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₁ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      (((fst
                (restrict
                  (comap
                    (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                      (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                      (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                        (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
                    μ)
                  (SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                    (Iio
                      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1)))) :
              Measure (↑(sphere 0 1) : Type u_1)) :
            (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞)
          s :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₂ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      (((restrict
                (comap
                  (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                    (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                    (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                      (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
                  μ)
                (SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                  (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))) :
              Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) :
            (a : Set ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) → ℝ≥0∞)
          (Prod.fst ⁻¹' s) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₃ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      (((comap
                (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
                  (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
                  (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                    (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → (↑{0}ᶜ : Type u_1)))
                μ :
              Measure ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) :
            (a : Set ((↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type))) → ℝ≥0∞)
          (Prod.fst ⁻¹' s ∩
            SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
              (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₄ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      ((μ : (a : Set E) → ℝ≥0∞)
          (comp (β := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
              (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
              (⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → { x : E // x ∈ {0}ᶜ }) ''
            (Prod.fst ⁻¹' s ∩
              SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1)))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₅ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      ((μ : (a : Set E) → ℝ≥0∞)
          (image (α := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            ((⇑(Homeomorph.symm (homeomorphUnitSphereProd E)) :
                (a : (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) → { x : E // x ∈ {0}ᶜ }) ''
              (Prod.fst ⁻¹' s ∩
                SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                  (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₆ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      ((μ : (a : Set E) → ℝ≥0∞)
          (image (α := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            ((⇑(homeomorphUnitSphereProd E) :
                (a : { x : E // x ∈ {0}ᶜ }) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ⁻¹'
              (Prod.fst ⁻¹' s ∩
                SProd.sprod (α := Set (↑(sphere 0 1) : Type u_1)) univ
                  (Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₇ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      ((μ : (a : Set E) → ℝ≥0∞)
          (image (α := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            ((⇑(homeomorphUnitSphereProd E) :
                (a : { x : E // x ∈ {0}ᶜ }) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ⁻¹'
              (Prod.fst ⁻¹' s ∩
                Prod.snd ⁻¹'
                  Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1)))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₈ :
  HSMul.hSMul (β := ℝ≥0∞) (dim E)
      ((μ : (a : Set E) → ℝ≥0∞)
          (image (α := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            ((⇑(homeomorphUnitSphereProd E) :
                (a : { x : E // x ∈ {0}ᶜ }) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ⁻¹'
              s ×ˢ Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₉ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (image (α := { x : E // Membership.mem (γ := Set E) {0}ᶜ x })
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x))
            ((⇑(homeomorphUnitSphereProd E) :
                (a : { x : E // x ∈ {0}ᶜ }) → (↑(sphere 0 1) : Type u_1) × (↑(Ioi 0) : Type)) ⁻¹'
              s ×ˢ Iio (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1))) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
rw₁₀ rw₁₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (Ioo 0 (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) 1 toSphere._proof_1) : ℝ) •
            Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)
⊢ ((μ.toSphere : Measure (↑(sphere 0 1) : Type u_1)) : (a : Set (↑(sphere 0 1) : Type u_1)) → ℝ≥0∞) s =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(dim E) : ℝ≥0∞) : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞)
          (HSMul.hSMul (α := Set ℝ) (Ioo 0 1)
            (Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 1) x) '' s)) :
        ℝ≥0∞)

Tactic:
rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
    ((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
      (Homeomorph.measurableEmbedding _)).comap_apply,
    image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]

Premises used: MeasureTheory.Measure.toSphere_apply_aux, MeasurableSingletonClass.measurableSet_singleton, Homeomorph.measurableEmbedding, MeasureTheory.Measure.toSphere, Set.univ_prod, MeasureTheory.Measure.restrict_apply, Set.prod_eq, MeasureTheory.Measure.fst_apply, Homeomorph.image_symm, MeasurableSet.compl, MeasurableEmbedding.comap_apply, MeasurableEmbedding.comp, MeasureTheory.Measure.smul_apply, nsmul_eq_mul, Set.image_comp, measurable_fst, MeasurableEmbedding.subtype_coe