-- 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
s : AffineSubspace ℝ P
hs : Nonempty.{u_4 + 1} ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ) :=
  Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) x_1) ⁻¹'
    (t ∩ (↑(mk' (↑(x +ᵥ p) : P) s.directionᗮ) : Set P))
hu : MeasurableSet u
hinter :
  t ∩ (↑(mk' (↑(x +ᵥ p) : P) s.directionᗮ) : Set P) =
    Subtype.val (p := fun (x_1 : P) ↦
        Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) x_1) ''
      u
hxp : Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) (↑(x +ᵥ p) : P)
hrank : finrank.{0, u_3} ℝ ↥s.directionᗮ = finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))
⊢ Eq (α := ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure V) : (a : Set V) → ENNReal)
        (Set.image (α := ↥s.directionᗮ) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s.directionᗮ : Set V)))
          (Prod.mk x ⁻¹'
            (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
                (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
              t)) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))] :
            Measure ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))) :
          (a : Set ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ).direction) → ENNReal)
        ((⇑(IsometryEquiv.vaddConst
                (Subtype.mk (p := fun (x_1 : P) ↦
                  Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) x_1) (↑(x +ᵥ p) : P)
                  hxp)) :
            (a : ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ).direction) → ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ)) ⁻¹'
          u) :
      ENNReal)
have e_f : Eq (α := ENNReal)
  (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure V) : (a : Set V) → ENNReal)
      (Set.image (α := ↥s.directionᗮ) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s.directionᗮ : Set V)))
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t)) :
    ENNReal)
  (((μHE[finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))] : Measure V) : (a : Set V) → ENNReal)
      (Set.image (α := ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)))
        (Subtype.val (p := fun (x_1 : V) ↦ x_1 ∈ (↑(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)) : Set V)))
        ((⇑(IsometryEquiv.vaddConst
                (Subtype.mk (p := fun (x_1 : P) ↦
                  Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) x_1) (↑(x +ᵥ p) : P)
                  hxp)) :
            (a : ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ).direction) → ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ)) ⁻¹'
          u)) :
    ENNReal)
Tactic: conv_rhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]