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
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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (AffineSubspace.mk' p (ℝ ∙ v)) 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
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)
⊢ 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)))

Tactic:
have hadd : MeasurableEmbedding (IsometryEquiv.vaddConst p') :=
    (IsometryEquiv.vaddConst p').toHomeomorph.measurableEmbedding
-- 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
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)))
⊢ MeasurableEmbedding g

Tactic:
have hg : MeasurableEmbedding g := hadd.comp hf
-- 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
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
unfold :
  μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ
      (map (α := ℝ)
        (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))
        volume)
⊢ μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)

Tactic:
unfold g
-- 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
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
rw :
  Eq.{u_4 + 1} (α := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (map.{u_3, u_4} (α := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
      (⇑(IsometryEquiv.vaddConst p') :
        (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
      volume)
    (map
      (⇑(IsometryEquiv.vaddConst p') :
        (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
      (HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v‖ₑ
        (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)))
⊢ μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ
      (map (α := ℝ)
        (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))
        volume)

Tactic:
rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
      ← Measure.map_smul]

Premises used: EuclideanGeometry.euclideanHausdorffMeasure_eq, MeasureTheory.Measure.map_smul, MeasurableEmbedding.measurable, MeasureTheory.Measure.map_map
-- 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
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
e_μ :
  volume =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v‖ₑ
      (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)
⊢ Eq.{u_4 + 1} (α := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v)))
    (map.{u_3, u_4} (α := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
      (⇑(IsometryEquiv.vaddConst p') :
        (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
      volume)
    (map
      (⇑(IsometryEquiv.vaddConst p') :
        (a : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) → ↥(AffineSubspace.mk' p (ℝ ∙ v)))
      (HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v‖ₑ
        (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)))

Tactic:
congr
-- 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
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
⊢ Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) v

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
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
v' : ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  Subtype.mk (p := fun (x : V) ↦
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) x) v ⋯
this :
  volume =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v'‖ₑ
      (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)
⊢ volume =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v‖ₑ
      (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)

Tactic:
simpa [v']
-- 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
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
v' : ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  Subtype.mk (p := fun (x : V) ↦
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) x) v ⋯
e_μ :
  volume =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v'‖ₑ
      (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)
⊢ volume =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v‖ₑ
      (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)

Tactic:
suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']
-- 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
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
v' : ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  Subtype.mk (p := fun (x : V) ↦
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) x) v ⋯
⊢ v' ≠ 0

Tactic:
simpa [v'] using hv
-- 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
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
v' : ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) :=
  Subtype.mk (p := fun (x : V) ↦
    Membership.mem (γ := Submodule ℝ V) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) x) v ⋯
⊢ volume =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v'‖ₑ
      (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)

Tactic:
exact volume_eq_of_finrank_eq_one hrank (by simpa [v'] using hv)

Premises used: MeasureTheory.volume_eq_of_finrank_eq_one