awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : r ≤ 0
this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} ∅
inl :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) ∅ =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₁ :
  0 = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₂ :
  0 =
    HPow.hPow (α := ℝ≥0∞) 0 (card ι) *
      ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
inl₃ : 0 = 0 * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inl₄ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [this, measure_empty, ← zero_eq_ofReal.mpr hr, zero_pow Fin.pos'.ne', zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma ((↑(card ι) : ℝ) / p + 1))
have inr : ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
    {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℝ)))
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} : ℝ≥0∞)
Tactic: rw [← volume_sum_rpow_lt_one _ hp, ← ofReal_pow (le_of_lt hr), ← finrank_pi ℝ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞)
      {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal (r ^ finrank.{0, u_1} ℝ (ι → ℝ)))
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ℝ≥0∞) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1} :
        ℝ≥0∞)
have h : {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
  HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
Tactic: convert! addHaar_smul_of_nonneg volume (le_of_lt hr) {x : ι → ℝ | ∑ i, |x i| ^ p < 1} using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
⊢ 0 < p
have linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₃ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₄ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₅ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₆ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r⁻¹| * |a x|) ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r⁻¹| * |a x|) ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₇ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * |a x| ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r⁻¹| * |a x|) ^ p) 1}
h₇ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * |a x| ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₈ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r|⁻¹ ^ p * |a x| ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r⁻¹| * |a x|) ^ p) 1}
h₇ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * |a x| ^ p) 1}
h₈ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r|⁻¹ ^ p * |a x| ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₉ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r| ^ p)⁻¹ * |a x| ^ p) 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r⁻¹| * |a x|) ^ p) 1}
h₇ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * |a x| ^ p) 1}
h₈ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r|⁻¹ ^ p * |a x| ^ p) 1}
h₉ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r| ^ p)⁻¹ * |a x| ^ p) 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₁₀ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | (|r| ^ p)⁻¹ * ∑ i : ι, |a i| ^ p < 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℝ), LE.le (α := ℝ) 0 (∑ i : ι, |x i| ^ p)
h₂ : ∀ (x : ι → ℝ), 0 ≤ HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p)
hr : 0 < r
h :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    (Set.preimage (β := ι → ℝ) (fun (x : ι → ℝ) ↦ r⁻¹ • x) {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1})
h₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |(r⁻¹ • a) i| ^ p) 1}
h₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ • a x| ^ p) 1}
h₅ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹ * a x| ^ p) 1}
h₆ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r⁻¹| * |a x|) ^ p) 1}
h₇ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r⁻¹| ^ p * |a x| ^ p) 1}
h₈ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, |r|⁻¹ ^ p * |a x| ^ p) 1}
h₉ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | LT.lt (α := ℝ) (∑ x : ι, (|r| ^ p)⁻¹ * |a x| ^ p) 1}
h₁₀ :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
    {a : ι → ℝ | (|r| ^ p)⁻¹ * ∑ i : ι, |a i| ^ p < 1}
⊢ {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r} =
    HSMul.hSMul (β := Set (ι → ℝ)) r {x : ι → ℝ | LT.lt (α := ℝ) (∑ i : ι, |x i| ^ p) 1}
have h₁₁ : Eq.{u_1 + 1} (α := Set (ι → ℝ)) {x : ι → ℝ | HPow.hPow (α := ℝ) (∑ i : ι, |x i| ^ p) (1 / p) < r}
  {a : ι → ℝ | (r ^ p)⁻¹ * ∑ i : ι, |a i| ^ p < 1}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
      smul_eq_mul, abs_mul, mul_rpow (abs_nonneg _) (abs_nonneg _), abs_inv,
      inv_rpow (abs_nonneg _), ← Finset.mul_sum, abs_eq_self.mpr (le_of_lt hr),
      inv_mul_lt_iff₀ (rpow_pos_of_pos hr _), mul_one, ← rpow_lt_rpow_iff
      (rpow_nonneg (h₁ _) _) (le_of_lt hr) (by linarith : 0 < p), ← rpow_mul
      (h₁ _), div_mul_cancel₀ _ (ne_of_gt (by linarith) : p ≠ 0), Real.rpow_one]