awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
h : g x < 1 ↔ {y : F | ‖y‖ < 1} x
⊢ g x < 1 ↔ Metric.ball 0 1 x

Tactic:
simp_rw [Metric.ball, dist_zero_right]

Premises used: Metric.ball, dist_zero_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ↔ {y : F | ‖y‖ < 1} x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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)

Tactic:
@Continuous.measurable E F tE mE _ _ _ _ φ ?_

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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) μ
refine : Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)
⊢ Measurable (α := E) (β := F) (⇑φ : (a : E) → F)

Tactic:
refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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) μ
⊢ Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)

Tactic:
@ContinuousLinearEquiv.continuous ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ

Premises used: ContinuousLinearEquiv.continuous
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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) μ
⊢ Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)

Tactic:
exact @ContinuousLinearEquiv.continuous ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ

Premises used: ContinuousLinearEquiv.continuous
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
⊢ MeasurePreserving (⇑ψ : (a : E) → F) μ ν

Tactic:
have : @MeasurePreserving E F mE _ ψ μ ν :=
      @Measurable.measurePreserving E F mE _ ψ (@MeasurableEquiv.measurable E F mE _ ψ) _
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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) μ ν
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))
⊢ 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))

Tactic:
rw [← this.integral_comp']

Premises used: MeasureTheory.MeasurePreserving.integral_comp'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : E), Real.exp (-norm (E := F) ((ψ : (a : E) → F) x : F) ^ p_1) ∂μ) /
        Real.Gamma ((↑(finrank ℝ F) : ℝ) / p_1 + 1))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
⊢ BorelSpace F

Tactic:
have : BorelSpace F := { measurable_eq := rfl }
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 F) → ℝ≥0∞) (Metric.closedBall 0 r) : ℝ≥0∞)
    ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 r) : ℝ≥0∞)

Tactic:
addHaar_closedBall_eq_addHaar_ball ν 0 r

Premises used: OfNat.ofNat, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 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∞)

Tactic:
convert! addHaar_closedBall_eq_addHaar_ball ν 0 r using 1

Premises used: OfNat.ofNat, MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ball
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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∞)
rw : Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x ≤ r} : ℝ≥0∞)
    ((ν : (a : Set F) → ℝ≥0∞) (Metric.closedBall 0 r) : ℝ≥0∞)

Tactic:
rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_closedBall]

Premises used: MeasureTheory.Measure.map_apply, measurableSet_closedBall
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 : ∀ (x : E), g x ≤ r ↔ Metric.closedBall 0 r x
⊢ 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:
congr!
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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
h : g x ≤ r ↔ {y : F | ‖y‖ ≤ r} x
⊢ g x ≤ r ↔ Metric.closedBall 0 r x

Tactic:
simp_rw [Metric.closedBall, dist_zero_right]

Premises used: Metric.closedBall, dist_zero_right
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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 ↔ {y : F | ‖y‖ ≤ r} x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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)

Tactic:
@Continuous.measurable E F tE mE _ _ _ _ φ ?_

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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) μ
refine : Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)
⊢ Measurable (α := E) (β := F) (⇑φ : (a : E) → F)

Tactic:
refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_

Premises used: Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
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) μ
⊢ Continuous (X := E) (Y := F) (⇑φ : (a : E) → F)

Tactic:
@ContinuousLinearEquiv.continuous ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ

Premises used: ContinuousLinearEquiv.continuous