awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Volume.Measure (hypothesis)
Goal:
V : Type u_3
P : Type u_4
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : MetricSpace P
inst_6 : MeasurableSpace P
inst_7 : BorelSpace P
inst_8 : NormedAddTorsor V P
p : P
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)
⊢ ((μ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 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)))
Tactic: have hadd : MeasurableEmbedding (IsometryEquiv.vaddConst p') :=
    (IsometryEquiv.vaddConst p').toHomeomorph.measurableEmbedding
-- 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))) ⋯)
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)))
⊢ ((μ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 hg : MeasurableEmbedding g
Tactic: have hg : MeasurableEmbedding g := hadd.comp hf
-- 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
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
⊢ μ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)
have 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)))
Tactic: rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
      ← Measure.map_smul]
-- 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
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
⊢ 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)))
have e_μ : volume =
  HSMul.hSMul (β := Measure ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))) ‖v‖ₑ
    (map (α := ℝ) (⇑f : (a : ℝ) → ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction) volume)
Tactic: congr
-- 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
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)
have e_μ : 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']
-- 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))) ⋯)
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
⊢ ((μ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 hm : μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
  HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)
Tactic: have hm : μHE[finrank ℝ (AffineSubspace.mk' p (ℝ ∙ v)).direction] =
      ‖v‖ₑ • (volume : Measure ℝ).map g := by
    unfold g
    rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
      ← Measure.map_smul]
    congr
    let v' : (AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, by simp⟩
    suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']
    exact volume_eq_of_finrank_eq_one hrank (by simpa [v'] using hv)
-- 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))) ⋯)
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
hm :
  μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)
⊢ ((μ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 hx : ∀ (x : ℝ), x • v +ᵥ p = (↑(g x) : P)
Tactic: have hx (x : ℝ) : x • v +ᵥ p = g x := by rfl
-- 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
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
hm :
  μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
    HSMul.hSMul (β := Measure ↥(AffineSubspace.mk' p (ℝ ∙ v))) ‖v‖ₑ (map g volume)
hx : ∀ (x : ℝ), x • v +ᵥ p = (↑(g x) : P)
⊢ ((μ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 simp_rw : ∫⁻ (x : ↥(AffineSubspace.mk' p (ℝ ∙ v))),
    ((μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ] : Measure P) :
        (a : Set P) → ENNReal)
      (t ∩
        (↑(AffineSubspace.mk' (↑x : P) (AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))ᗮ) :
          Set P)) ∂μHE[finrank.{0, u_3} ℝ ↥(AffineSubspace.direction (AffineSubspace.mk' p (ℝ ∙ v)))] =
  ‖v‖ₑ *
    ∫⁻ (x : ℝ),
      ((μHE[finrank ℝ V - 1] : Measure P) : (a : Set P) → ENNReal)
        (t ∩ (↑(AffineSubspace.mk' (x • v +ᵥ p) (ℝ ∙ v)ᗮ) : Set P))
Tactic: simp_rw [(AffineSubspace.mk' p (ℝ ∙ v)).euclideanHausdorffMeasure_eq_lintegral ht, hx,
    hm, lintegral_smul_measure, hg.lintegral_map, smul_eq_mul, hrank', AffineSubspace.direction_mk']
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
⊢ X ^ n ⊂ X ^ (n + 1)
have inl : ∀ (hXclosure : HPow.hPow (β := ℕ) (↑X : Set G) 0 ≠ (↑(closure (↑X : Set G)) : Set G)),
  HPow.hPow (β := ℕ) X 0 ⊂ X ^ HAdd.hAdd (α := ℕ) 0 1
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n, hXclosure
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
inl :
  ∀ (hXclosure : HPow.hPow (β := ℕ) (↑X : Set G) 0 ≠ (↑(closure (↑X : Set G)) : Set G)),
    HPow.hPow (β := ℕ) X 0 ⊂ X ^ HAdd.hAdd (α := ℕ) 0 1
⊢ X ^ n ⊂ X ^ (n + 1)
have inr : ∀ (hn : n ≠ 0), X ^ n ⊂ X ^ (n + 1)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
hn : n ≠ 0
⊢ X ^ n ⊂ X ^ (n + 1)
have inr : X ^ n ≠ X ^ (n + 1)
Tactic: refine (pow_subset_pow_right hX₁ <| n.le_add_right _).ssubset_of_ne ?_
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : (↑X : Set G) ^ n ≠ (↑(closure (↑X : Set G)) : Set G)
hn : n ≠ 0
⊢ X ^ n ≠ X ^ (n + 1)
have inr : ∀ (hXn : X ^ n = X ^ (n + 1)), (↑X : Set G) ^ n = (↑(closure (↑X : Set G)) : Set G)
Tactic: contrapose hXclosure with hXn
Cleared hypotheses: hXclosure
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
⊢ (↑X : Set G) ^ n = (↑(closure (↑X : Set G)) : Set G)
have inr : (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
Tactic: rw [← closure_pow (mod_cast hX₁) hn]
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
have inr : ∀
  (this :
    ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
      (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1),
      (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G))
  (hn₁ : ¬n = 1), (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
Tactic: wlog hn₁ : n = 1
-- Lean 4 proof step from Mathlib.Geometry.Group.Growth.LinearLowerBound (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
inr :
  ∀
    (this :
      ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X)
        (hX : X.Nontrivial) (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1),
        (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G))
    (hn₁ : ¬n = 1), (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
⊢ (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
have wlog : ∀ {G : Type u_1} [inst : Group G] [inst_2 : DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial)
  (hn : n ≠ 0) (hXn : X ^ n = X ^ (n + 1)) (hn₁ : n = 1), (↑X : Set G) ^ n = (↑(closure ((↑X : Set G) ^ n)) : Set G)
Tactic: wlog hn₁ : n = 1
Cleared hypotheses: hX₁, hX, hn, hXn