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
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:
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
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∞)
rw : Measurable (α := E) (β := F) (⇑φ : (a : E) → F)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | g x < r} : ℝ≥0∞) ((ν : (a : Set F) → ℝ≥0∞) (Metric.ball 0 r) : ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.map_apply, measurableSet_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 : ∀ (x : E), g x < r ↔ Metric.ball 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.ball 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.ball 0 r 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
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:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
⊢ 0 < p

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

Tactic:
have h₁ : 0 < p := by linarith
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
⊢ (ENNReal.ofReal p).toReal = p

Tactic:
have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
fun _ => Finset.sum_nonneg' ?_

Premises used: Finset.sum_nonneg'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
refine : ∀ (x : ι → ℝ) (i : ι), 0 ≤ |x i| ^ p
⊢ ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
refine fun _ => Finset.sum_nonneg' ?_

Premises used: Finset.sum_nonneg'
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
x : ι → ℝ
⊢ ∀ (i : ι), 0 ≤ |x i| ^ p

Tactic:
fun i => (fun _ => rpow_nonneg (abs_nonneg _) _) _

Premises used: Real.rpow_nonneg, abs_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
x : ι → ℝ
⊢ ∀ (i : ι), 0 ≤ |x i| ^ p

Tactic:
exact fun i => (fun _ => rpow_nonneg (abs_nonneg _) _) _

Premises used: Real.rpow_nonneg, abs_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
⊢ ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)

Tactic:
have h₂ : ∀ x : ι → ℝ, 0 ≤ ∑ i, |x i| ^ p := by
    refine fun _ => Finset.sum_nonneg' ?_
    exact fun i => (fun _ => rpow_nonneg (abs_nonneg _) _) _
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
x : ι → ℝ
⊢ Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
    HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)

Tactic:
simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]

Premises used: ENNReal.ofReal, WithLp.toLp, PiLp.norm_eq_sum
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
⊢ ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)

Tactic:
have eq_norm (x : ι → ℝ) : ‖toLp (.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p) := by
    simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
⊢ Fact (1 ≤ ENNReal.ofReal p)

Tactic:
have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ofReal_one ▸ (ofReal_le_ofReal hp))
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
⊢ Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0

Tactic:
have nm_zero : ‖toLp (.ofReal p) (0 : ι → ℝ)‖ = 0 := norm_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
⊢ ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0

Tactic:
have eq_zero (x : ι → ℝ) : ‖toLp (.ofReal p) x‖ = 0 ↔ x = 0 :=
    norm_eq_zero.trans (toLp_eq_zero _)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
⊢ ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)

Tactic:
have nm_neg := fun x : ι → ℝ => norm_neg (toLp (.ofReal p) x)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)
⊢ ∀ (x y : ι → ℝ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) y)

Tactic:
have nm_add := fun x y : ι → ℝ => norm_add_le (toLp (.ofReal p) x) (toLp (.ofReal p) y)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℝ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) y)
⊢ ∀ (r : ℝ) (x : ι → ℝ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) (toLp (ENNReal.ofReal p) x)

Tactic:
have nm_smul := fun (r : ℝ) (x : ι → ℝ) =>
    norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℝ)) r (toLp (.ofReal p) x)
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℝ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℝ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) (toLp (ENNReal.ofReal p) x)
⊢ ∀ (x : ι → ℝ), HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) = 0 ↔ x = 0

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm,
    norm_eq_abs] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℝ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℝ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℝ), HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) = 0 ↔ x = 0
⊢ HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (α := ℝ) |0 i| p) (1 / p) = 0

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm,
    norm_eq_abs] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℝ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℝ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℝ), HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (α := ℝ) |0 i| p) (1 / p) = 0
⊢ ∀ (x : ι → ℝ), HPow.hPow (α := ℝ) (∑ i : ι, |(-x) i| ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm,
    norm_eq_abs] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
Goal:
ι : Type u_1
inst : Fintype ι
p : ℝ
hp : 1 ≤ p
h₁ : 0 < p
this_1 : (ENNReal.ofReal p).toReal = p
h₂ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
eq_norm :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) =
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
this : Fact (1 ≤ ENNReal.ofReal p)
nm_zero : Norm.norm.{u_1} (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) 0) = 0
eq_zero : ∀ (x : ι → ℝ), Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) = 0 ↔ x = 0
nm_neg :
  ∀ (x : ι → ℝ),
    Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (-toLp (ENNReal.ofReal p) x) =
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x)
nm_add :
  ∀ (x y : ι → ℝ),
    ‖HAdd.hAdd (α := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) (toLp (ENNReal.ofReal p) y)‖ ≤
      Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) x) +
        Norm.norm (E := WithLp (ENNReal.ofReal p) (ι → ℝ)) (toLp (ENNReal.ofReal p) y)
nm_smul :
  ∀ (r : ℝ) (x : ι → ℝ),
    ‖HSMul.hSMul (β := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) r (toLp (ENNReal.ofReal p) x)‖ ≤
      ‖r‖ * Norm.norm (E := PiLp (ENNReal.ofReal p) fun (x : ι) ↦ ℝ) (toLp (ENNReal.ofReal p) x)
eq_zero₁ : ∀ (x : ι → ℝ), HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) = 0 ↔ x = 0
nm_zero₁ : HPow.hPow (α := ℝ) (∑ i : ι, HPow.hPow (α := ℝ) |0 i| p) (1 / p) = 0
nm_neg₁ :
  ∀ (x : ι → ℝ), HPow.hPow (α := ℝ) (∑ i : ι, |(-x) i| ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
⊢ ∀ (x y : ι → ℝ),
    HPow.hPow (α := ℝ) (∑ i : ι, |(x + y) i| ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i : ι, |y i| ^ p) (1 / p)

Tactic:
simp_rw [← toLp_neg, ← toLp_add, ← toLp_smul, eq_norm,
    norm_eq_abs] at eq_zero nm_zero nm_neg nm_add nm_smul

Premises used: WithLp.toLp_smul, WithLp.toLp_neg, WithLp.toLp_add, Real.norm_eq_abs