awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
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
h :
  Eq.{u_4 + 1} (α := Measure P)
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p : V ≃ᵢ P) : (a : V) → P) μHE[finrank ℝ V]) μHE[finrank ℝ V]
⊢ Eq.{u_4 + 1} (α := Measure P) μHE[finrank ℝ V]
    (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p) : (a : V) → P) volume)
have h₁ : Eq.{u_4 + 1} (α := Measure P)
  (map.{u_3, u_4} (α := V) (⇑(IsometryEquiv.vaddConst p : V ≃ᵢ P) : (a : V) → P) (volume : Measure V)) μHE[finrank ℝ V]
Tactic: rw [InnerProductSpace.euclideanHausdorffMeasure_eq_volume] at h
Cleared hypotheses: h
-- 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 : Submodule ℝ V
p : P
⊢ MeasurePreserving.{u_4, u_3} (α := P) (β := ↥s × ↥sᗮ) (⇑(s.measurableEquivProd p) : (a : P) → ↥s × ↥sᗮ)
    μHE[finrank ℝ V] (volume : Measure (↥s × ↥sᗮ))
have refine : MeasurePreserving (α := V) (β := ↥s × ↥sᗮ)
  (⇑(MeasurableEquiv.trans s.orthogonalDecomposition.toHomeomorph.toMeasurableEquiv
        (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (↥s × ↥sᗮ)))) :
    (a : V) → ↥s × ↥sᗮ)
  (volume : Measure V) (volume : Measure (↥s × ↥sᗮ))
Tactic: refine (measurePreserving_vaddConst _).symm.trans ?_
-- 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 : Submodule ℝ V
p : P
⊢ MeasurePreserving (α := V) (β := ↥s × ↥sᗮ)
    (⇑(MeasurableEquiv.trans s.orthogonalDecomposition.toHomeomorph.toMeasurableEquiv
          (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (↥s × ↥sᗮ)))) :
      (a : V) → ↥s × ↥sᗮ)
    (volume : Measure V) (volume : Measure (↥s × ↥sᗮ))
have refine : MeasurePreserving.{u_3, u_3} (α := WithLp 2 (↥s × ↥sᗮ)) (β := ↥s × ↥sᗮ)
  (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (↥s × ↥sᗮ))) : (a : WithLp 2 (↥s × ↥sᗮ)) → ↥s × ↥sᗮ)
  (volume : Measure (WithLp 2 (↥s × ↥sᗮ))) (volume : Measure (↥s × ↥sᗮ))
Tactic: refine s.orthogonalDecomposition.measurePreserving.trans ?_
-- 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
⊢ ((μHE[finrank ℝ V] : Measure P) : (a : Set P) → ENNReal) t =
    ∫⁻ (x : ↥s),
      ((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩ (↑(mk' (↑x : P) s.directionᗮ) : Set P)) ∂μHE[finrank.{0, u_3} ℝ ↥s.direction]
have obtain : ∀ (p : ↥s),
  ((μHE[finrank ℝ V] : Measure P) : (a : Set P) → ENNReal) t =
    ∫⁻ (x : ↥s),
      ((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩ (↑(mk' (↑x : P) s.directionᗮ) : Set P)) ∂μHE[finrank.{0, u_3} ℝ ↥s.direction]
Tactic: obtain p := hs.some
-- 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
⊢ ((μHE[finrank ℝ V] : Measure P) : (a : Set P) → ENNReal) t =
    ∫⁻ (x : ↥s),
      ((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩ (↑(mk' (↑x : P) s.directionᗮ) : Set P)) ∂μHE[finrank.{0, u_3} ℝ ↥s.direction]
have rw : ∫⁻ (x : ↥s.direction),
    ((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
      (Prod.mk x ⁻¹'
        (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
            (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
          t) =
  ∫⁻ (a : ↥s.direction),
    ((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
      (t ∩
        (↑(mk'
              (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s) a) :
                P)
              s.directionᗮ) :
          Set P))
Tactic: rw [← (s.direction.measurePreserving_measurableEquivProd p.val).symm.measure_preimage_equiv,
    volume_eq_prod, prod_apply (by measurability), euclideanHausdorffMeasure_eq,
    MeasurableEmbedding.lintegral_map
        (by simpa using (IsometryEquiv.vaddConst p).toHomeomorph.measurableEmbedding)]
-- 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),
      ((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) =
    ∫⁻ (a : ↥s.direction),
      ((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      a) :
                  P)
                s.directionᗮ) :
            Set P))
have e_f : ∀ (x : ↥s.direction),
  Eq (α := ENNReal)
    (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      x) :
                  P)
                s.directionᗮ) :
            Set P)) :
      ENNReal)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
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))
⊢ Eq (α := ENNReal)
    (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      x) :
                  P)
                s.directionᗮ) :
            Set P)) :
      ENNReal)
have hu : MeasurableSet u
Tactic: have hu : MeasurableSet u :=
    (ht.inter (closed_of_finiteDimensional _).measurableSet).preimage measurable_subtype_coe
-- 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
⊢ 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
have h : ∀ (x_1 : P),
  x_1 ∈ t ∩ (↑(mk' (↑(x +ᵥ p) : P) s.directionᗮ) : Set P) ↔
    x_1 ∈
      Subtype.val (p := fun (x_2 : P) ↦
          Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) x_2) ''
        u
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
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
⊢ Eq (α := ENNReal)
    (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      x) :
                  P)
                s.directionᗮ) :
            Set P)) :
      ENNReal)
have 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
Tactic: have hinter : t ∩ (mk' (x +ᵥ p).val s.directionᗮ) = Subtype.val '' u := by
    ext x
    simp [u]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
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
⊢ Eq (α := ENNReal)
    (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      x) :
                  P)
                s.directionᗮ) :
            Set P)) :
      ENNReal)
have hxp : Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) (↑(x +ᵥ p) : P)
Tactic: have hxp : (x +ᵥ p).val ∈ mk' (x +ᵥ p).val s.directionᗮ := by simp
-- 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)
⊢ finrank.{0, u_3} ℝ ↥s.directionᗮ = finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))
have rw : finrank.{0, u_3} ℝ ↥s.directionᗮ = finrank.{0, u_3} ℝ ↥s.directionᗮ
Tactic: rw [direction_mk']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
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)
⊢ Eq (α := ENNReal)
    (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      x) :
                  P)
                s.directionᗮ) :
            Set P)) :
      ENNReal)
have hrank : finrank.{0, u_3} ℝ ↥s.directionᗮ = finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))
Tactic: have hrank : finrank ℝ s.directionᗮ = finrank ℝ (mk' (x +ᵥ p).val s.directionᗮ).direction := by
    rw [direction_mk']
-- 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ᗮ))
⊢ Measurable.{u_3, u_4} (α := ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))) (β :=
    ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ))
    (⇑(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ᗮ))
have funProp : LE.le.{u_3} (α := MeasurableSpace ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)))
  (Subtype.instMeasurableSpace (p := fun (x_1 : V) ↦ x_1 ∈ direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)))
  MeasureSpace.toMeasurableSpace
Tactic: fun_prop
-- 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ᗮ))
funProp :
  LE.le.{u_3} (α := MeasurableSpace ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)))
    (Subtype.instMeasurableSpace (p := fun (x_1 : V) ↦ x_1 ∈ direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)))
    MeasureSpace.toMeasurableSpace
⊢ Measurable.{u_3, u_4} (α := ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))) (β :=
    ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ))
    (⇑(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ᗮ))
have funProp₁ : MeasurableEmbedding.{u_3, u_4} (β := ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ))
  fun (a : ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))) ↦
  ((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) :
        IsometryEquiv.{u_3, u_4} ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)) ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ)) :
      (a : ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ).direction) → ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ))
    a
Tactic: fun_prop
-- 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)
    (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
        (Prod.mk x ⁻¹'
          (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
              (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
            t) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure P) : (a : Set P) → ENNReal)
        (t ∩
          (↑(mk'
                (↑(((IsometryEquiv.vaddConst p : IsometryEquiv.{u_3, u_4} ↥s.direction ↥s) : (a : ↥s.direction) → ↥s)
                      x) :
                  P)
                s.directionᗮ) :
            Set P)) :
      ENNReal)
have e_f : Eq (α := ENNReal)
  (((volume : Measure ↥s.directionᗮ) : (a : Set ↥s.directionᗮ) → ENNReal)
      (Prod.mk x ⁻¹'
        (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
            (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
          t) :
    ENNReal)
  (((volume : 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)
Tactic: rw [IsometryEquiv.vaddConst_apply, hinter, euclideanHausdorffMeasure_coe_image, hrank,
    euclideanHausdorffMeasure_eq ⟨x +ᵥ p, hxp⟩, map_apply (by fun_prop) hu]