-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (goal)
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : MetricSpace P
inst_6 : MeasurableSpace P
inst_7 : BorelSpace P
inst_8 : NormedAddTorsor V P
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
hrank' : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv)
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) ⋯)
hf :
  MeasurableEmbedding (α := ℝ) (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) x) p ⋯
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) :=
  Function.comp (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
hadd :
  MeasurableEmbedding.{u_3, u_4} (α := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) (β :=
    ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (⇑(IsometryEquiv.vaddConst p') : (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
hg : MeasurableEmbedding g
hm :
  μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)
hx : ∀ (x : ℝ), x • v +ᵥ p = (↑(g x) : P)
simp_rw :
  ∫⁻ (x : ↥(AffineSubspace.mk' p (ℝ ∙ v))),
      ((μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ] : Measure P) :
          (a : Set P) → ENNReal)
        (t ∩
          (↑(AffineSubspace.mk' (↑x : P) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ) :
            Set P)) ∂μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        ((μHE[finrank ℝ V - 1] : Measure P) : (a : Set P) → ENNReal)
          (t ∩ (↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ) : Set P))
⊢ ((μHE[finrank ℝ V] : Measure P) : (a : Set P) → ENNReal) t =
    ‖v‖ₑ *
      ∫⁻ (x : ℝ),
        ((μHE[finrank ℝ V - 1] : Measure P) : (a : Set P) → ENNReal)
          (t ∩ (↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ) : Set P))
have simp_rw₁ : ∫⁻ (x : ↥(AffineSubspace.mk' p (ℝ ∙ v))),
    ((μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ] : Measure P) :
        (a : Set P) → ENNReal)
      (t ∩
        (↑(AffineSubspace.mk' (↑x : P) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ) :
          Set P)) ∂μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
  ‖v‖ₑ *
    ∫⁻ (x : ℝ),
      ((μHE[finrank ℝ V - 1] : Measure P) : (a : Set P) → ENNReal)
        (t ∩ (↑(AffineSubspace.mk' (↑(g x) : P) (ℝ ∙ v)ᗮ) : Set P))
Tactic: simp_rw [(AffineSubspace.mk' p (ℝ ∙ v)).euclideanHausdorffMeasure_eq_lintegral ht, hx,
    hm, lintegral_smul_measure, hg.lintegral_map, smul_eq_mul, hrank', AffineSubspace.direction_mk']