awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
    (((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)
have e_f : Eq (α := ENNReal)
  (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : 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} ℝ ↥(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)
Tactic: simp_rw [← InnerProductSpace.euclideanHausdorffMeasure_eq_volume]
-- 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ᗮ))
| (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : 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)
have rw : (((μ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)
Tactic: rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
-- 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 ↥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} ℝ ↥(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 ↥(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: conv_lhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
-- 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ᗮ))
| (((μ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 rw : (((μ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: rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]
-- 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 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)
have e_f : Eq (α := Set V)
  (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))
  (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))
Tactic: congrm μHE[$hrank] ?_
-- 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 (α := Set V)
    (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))
    (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))
have e_f : ∀ (y : V),
  Membership.mem (γ := Set V)
      (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))
      y ↔
    Membership.mem (γ := Set V)
      (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))
      y
Tactic: ext y
-- 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
⊢ finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
have rw : finrank.{0, u_3} ℝ ↥(ℝ ∙ v) = 1
Tactic: rw [AffineSubspace.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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ ((μ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 hrank : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
Tactic: have hrank : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction = 1 := by
    rw [AffineSubspace.direction_mk']
    apply finrank_span_singleton hv
-- 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
⊢ finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
have rw : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ =
  finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) +
      finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ -
    1
Tactic: rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]
-- 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
rw :
  finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ =
    finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) +
        finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ -
      1
⊢ finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
have rw₁ : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ =
  1 + finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ - 1
Tactic: rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]
-- 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
rw :
  finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ =
    finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) +
        finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ -
      1
rw₁ :
  finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ =
    1 + finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ - 1
⊢ finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
have rw₂ : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ =
  finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ
Tactic: rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]
-- 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
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1
⊢ ((μ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 hrank' : finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ = finrank ℝ V - 1
Tactic: have hrank' : finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1 := by
    rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]
-- 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
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))) ⋯)
⊢ ((μ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 hf : MeasurableEmbedding (α := ℝ) (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
  (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)
Tactic: have hf : MeasurableEmbedding f := f.toHomeomorph.measurableEmbedding