awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 1)) : ℝ≥0∞)
Tactic: rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 1)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞)
have rw : Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
Tactic: rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < 1} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 1)) : ℝ≥0∞)
have h : ∀ (x : E), g x < 1 ↔ Metric.ball 0 1 x
Tactic: congr!
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
x : E
⊢ g x < 1 ↔ Metric.ball 0 1 x
have h : g x < 1 ↔ {y : F | ‖y‖ < 1} x
Tactic: simp_rw [Metric.ball, dist_zero_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
have refine : Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)
Tactic: refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
ψ : E ≃ᵐ F := φ.toHomeomorph.toMeasurableEquiv
⊢ ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1)) =
    ENNReal.ofReal ((∫ (x : F), Real.exp (-‖x‖ ^ p_1) ∂ν) / Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))
have this₁ : MeasurePreserving (⇑ψ : (a : E) → F) μ ν
Tactic: have : @MeasurePreserving E F mE _ ψ μ ν :=
      @Measurable.measurePreserving E F mE _ ψ (@MeasurableEquiv.measurable E F mE _ ψ) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
p_1 : ℝ
hp : 0 < p_1
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this_5 : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
ψ : E ≃ᵐ F := φ.toHomeomorph.toMeasurableEquiv
this : MeasurePreserving (⇑ψ : (a : E) → F) μ ν
⊢ ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1)) =
    ENNReal.ofReal ((∫ (x : F), Real.exp (-‖x‖ ^ p_1) ∂ν) / Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))
have h : ENNReal.ofReal ((∫ (x : E), Real.exp (-g x ^ p_1) ∂μ) / Real.Gamma ((↑(finrank ℝ E) : ℝ) / p_1 + 1)) =
  ENNReal.ofReal
    ((∫ (x : E), Real.exp (-norm (E := F) ((ψ : (a : E) → F) x : F) ^ p_1) ∂μ) /
      Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))
Tactic: rw [← this.integral_comp']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this : MeasurableSpace F := borel F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞)
have this₁ : BorelSpace F
Tactic: have : BorelSpace F := { measurable_eq := rfl }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
  ((ν : (a : Set F) → ℝ≥0∞) (Metric.closedBall 0 r) : ℝ≥0∞)
Tactic: convert! addHaar_closedBall_eq_addHaar_ball ν 0 r using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
    ((ν : (a : Set F) → ℝ≥0∞) (Metric.closedBall 0 r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 r) : ℝ≥0∞)
Tactic: convert! addHaar_closedBall_eq_addHaar_ball ν 0 r using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
    ((ν : (a : Set F) → ℝ≥0∞) (Metric.closedBall 0 r) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.closedBall 0 r)) : ℝ≥0∞)
Tactic: rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_closedBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.closedBall 0 r)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
    ((ν : (a : Set F) → ℝ≥0∞) (Metric.closedBall 0 r) : ℝ≥0∞)
have rw : Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
Tactic: rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_closedBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.closedBall 0 r)) : ℝ≥0∞)
have h : ∀ (x : E), g x ≤ r ↔ Metric.closedBall 0 r x
Tactic: congr!
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
x : E
⊢ g x ≤ r ↔ Metric.closedBall 0 r x
have h : g x ≤ r ↔ {y : F | ‖y‖ ≤ r} x
Tactic: simp_rw [Metric.closedBall, dist_zero_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
have refine : Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)
Tactic: refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 r) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞)
  ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 r)) : ℝ≥0∞)
Tactic: rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : FiniteDimensional ℝ E
mE : MeasurableSpace E
tE : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : BorelSpace E
inst_5 : T2Space E
inst_6 : ContinuousSMul ℝ E
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
g : E → ℝ
h1 : g 0 = 0
h2 : ∀ (x : E), g (-x) = g x
h3 : ∀ (x y : E), g (x + y) ≤ g x + g y
h4 : ∀ {x : E}, g x = 0 → x = 0
h5 : ∀ (r : ℝ) (x : E), g (r • x) ≤ |r| * g x
inst_8 : Nontrivial E
r : ℝ
F : Type u_1 := E
p : AddGroupNorm F := { toFun := g, map_zero' := h1, add_le' := h3, neg' := h2, eq_zero_of_map_eq_zero' := ⋯ }
this_1 : NormedAddCommGroup F := p.toNormedAddCommGroup
this_2 : NormedSpace ℝ F := { toModule := inst_1, norm_smul_le := ⋯ }
this_3 : TopologicalSpace F := UniformSpace.toTopologicalSpace
this_4 : MeasurableSpace F := borel F
this : BorelSpace F
φ : E ≃L[ℝ] F := LinearEquiv.toContinuousLinearEquiv (LinearEquiv.refl ℝ E)
ν : Measure F := map (⇑φ : (a : E) → F) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Set.preimage (β := F) (⇑φ : (a : E) → F) (Metric.ball 0 r)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 r) : ℝ≥0∞)
have rw : Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
Tactic: rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball]