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 : 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)
    (((μ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)
⊢ 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:
simp_rw [← InnerProductSpace.euclideanHausdorffMeasure_eq_volume]

Premises used: InnerProductSpace.euclideanHausdorffMeasure_eq_volume
-- 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ᗮ))
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)
| (((μ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)

Tactic:
rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]

Premises used: Isometry.euclideanHausdorffMeasure_image
-- 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)
    (((μ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)
⊢ 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:
conv_lhs => rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]

Premises used: Isometry.euclideanHausdorffMeasure_image
-- 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ᗮ))
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)
| (((μ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:
rw [← isometry_subtype_coe.euclideanHausdorffMeasure_image]

Premises used: Isometry.euclideanHausdorffMeasure_image
-- 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 (α := 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))
⊢ Eq (α := ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥s.directionᗮ] : Measure V) : (a : Set V) → ENNReal)
        (Set.image (α := ↥s.directionᗮ) (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s.directionᗮ : Set V)))
          (Prod.mk x ⁻¹'
            (⇑(MeasurableEquiv.symm (s.direction.measurableEquivProd (↑p : P))) :
                (a : ↥s.direction × ↥s.directionᗮ) → P) ⁻¹'
              t)) :
      ENNReal)
    (((μHE[finrank.{0, u_3} ℝ ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ))] : Measure V) : (a : Set V) → ENNReal)
        (Set.image (α := ↥(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)))
          (Subtype.val (p := fun (x_1 : V) ↦ x_1 ∈ (↑(direction (mk' (↑(x +ᵥ p) : P) s.directionᗮ)) : Set V)))
          ((⇑(IsometryEquiv.vaddConst
                  (Subtype.mk (p := fun (x_1 : P) ↦
                    Membership.mem (γ := AffineSubspace ℝ P) (mk' (↑(x +ᵥ p) : P) s.directionᗮ) x_1) (↑(x +ᵥ p) : P)
                    hxp)) :
              (a : ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ).direction) → ↥(mk' (↑(x +ᵥ p) : P) s.directionᗮ)) ⁻¹'
            u)) :
      ENNReal)

Tactic:
congrm μHE[$hrank] ?_
-- 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 :
  ∀ (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
⊢ 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:
ext y
-- 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ᗮ))
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:
simp [u, vadd_vadd, add_comm]

Premises used: vadd_vadd, add_comm
-- 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
rw : finrank.{0, u_3} ℝ ↥(ℝ ∙ v) = 1
⊢ finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))) = 1

Tactic:
rw [AffineSubspace.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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
⊢ finrank.{0, u_3} ℝ ↥(ℝ ∙ v) = 1

Tactic:
apply finrank_span_singleton hv

Premises used: finrank_span_singleton
-- 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
⊢ 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
-- 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
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
rw₂ 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)))ᗮ = finrank ℝ V - 1

Tactic:
rw [← (AffineSubspace.mk' p (ℝ ∙ v)).direction.finrank_add_finrank_orthogonal, hrank,
      Nat.add_sub_cancel_left]

Premises used: Real, AffineSubspace.mk', Nat.add_sub_cancel_left, Submodule.span, Submodule.finrank_add_finrank_orthogonal, Singleton.singleton, 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
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

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]
-- 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
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ v) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ 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))) ⋯)
⊢ MeasurableEmbedding (α := ℝ) (β := ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v))))
    (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction)

Tactic:
have hf : MeasurableEmbedding f := f.toHomeomorph.measurableEmbedding