awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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ᗮ))

Tactic:
(measurePreserving_vaddConst _).symm.trans ?_

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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ᗮ))
⊢ MeasurePreserving.{u_4, u_3} (α := P) (β := ↥s × ↥sᗮ) (⇑(s.measurableEquivProd p) : (a : P) → ↥s × ↥sᗮ)
    μHE[finrank ℝ V] (volume : Measure (↥s × ↥sᗮ))

Tactic:
refine (measurePreserving_vaddConst _).symm.trans ?_

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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ᗮ))

Tactic:
s.orthogonalDecomposition.measurePreserving.trans ?_

Premises used: MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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ᗮ))
⊢ 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 s.orthogonalDecomposition.measurePreserving.trans ?_

Premises used: MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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_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:
WithLp.volume_preserving_ofLp _ _

Premises used: Set.Mem, WithLp.volume_preserving_ofLp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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_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:
exact WithLp.volume_preserving_ofLp _ _

Premises used: WithLp.volume_preserving_ofLp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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]
⊢ ((μ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

Premises used: Nonempty.some
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ MeasurableSet.{u_3} (α := ↥s.direction × ↥s.directionᗮ)
    ((⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) : (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
      t)

Tactic:
measurability
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ MeasurableEmbedding.{u_3, u_4} (α := ↥s.direction) (β := ↥s) (⇑(IsometryEquiv.vaddConst p) : (a : ↥s.direction) → ↥s)

Tactic:
simpa using (IsometryEquiv.vaddConst p).toHomeomorph.measurableEmbedding

Premises used: Homeomorph.measurableEmbedding, IsometryEquiv.vaddConst, IsometryEquiv.toHomeomorph
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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))
⊢ ((μ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:
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)]

Premises used: EuclideanGeometry.euclideanHausdorffMeasure_eq, MeasureTheory.MeasurePreserving.symm, Submodule.measurePreserving_measurableEquivProd, MeasureTheory.Measure.prod_apply, MeasurableEmbedding.lintegral_map, MeasureTheory.MeasurePreserving.measure_preimage_equiv, MeasureTheory.Measure.volume_eq_prod, Subtype.val, AffineSubspace.direction
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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)
⊢ ∫⁻ (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:
congr with x
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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))
⊢ MeasurableSet u

Tactic:
have hu : MeasurableSet u :=
    (ht.inter (closed_of_finiteDimensional _).measurableSet).preimage measurable_subtype_coe
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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
⊢ 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:
ext x
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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_1 : ↥s.direction
u : Set ↥(mk' (↑(x_1 +ᵥ p) : P) s.directionᗮ) :=
  Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x_1 +ᵥ p) : P) s.directionᗮ) x) ⁻¹'
    (t ∩ (↑(mk' (↑(x_1 +ᵥ p) : P) s.directionᗮ) : Set P))
hu : MeasurableSet u
x : P
⊢ x ∈ t ∩ (↑(mk' (↑(x_1 +ᵥ p) : P) s.directionᗮ) : Set P) ↔
    x ∈
      Subtype.val (p := fun (x : P) ↦
          Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x_1 +ᵥ p) : P) s.directionᗮ) x) ''
        u

Tactic:
simp [u]
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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

Tactic:
have hinter : t ∩ (mk' (x +ᵥ p).val s.directionᗮ) = Subtype.val '' u := by
    ext x
    simp [u]
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) (↑(x +ᵥ p) : P)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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)
rw rw₁ : finrank.{0, u_3} ℝ ↥s.directionᗮ = finrank.{0, u_3} ℝ ↥s.directionᗮ
⊢ finrank.{0, u_3} ℝ ↥s.directionᗮ = finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))

Tactic:
rw [direction_mk']

Premises used: AffineSubspace.direction_mk'
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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ᗮ))

Tactic:
have hrank : finrank ℝ s.directionᗮ = finrank ℝ (mk' (x +ᵥ p).val s.directionᗮ).direction := by
    rw [direction_mk']
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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
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
⊢ 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ᗮ))

Tactic:
fun_prop
-- Module: Mathlib.Geometry.Euclidean.Volume.Measure
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ᗮ))
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)
⊢ 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:
rw [IsometryEquiv.vaddConst_apply, hinter, euclideanHausdorffMeasure_coe_image, hrank,
    euclideanHausdorffMeasure_eq ⟨x +ᵥ p, hxp⟩, map_apply (by fun_prop) hu]

Premises used: EuclideanGeometry.euclideanHausdorffMeasure_eq, MeasureTheory.Measure.map_apply, IsometryEquiv.vaddConst_apply, AffineSubspace.euclideanHausdorffMeasure_coe_image