-- 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⁻¹‖ ^ 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 : ι → ℂ | 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}
h₁₁ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | (r ^ p)⁻¹ * ∑ i : ι, ‖a i‖ ^ p < 1}
h₁₂ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p * 1}
h₁₃ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) < r}
    {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p}
h₁₄ :
  Eq.{u_1 + 1} (α := Set (ι → ℂ)) {x : ι → ℂ | HPow.hPow (α := ℝ) (∑ i : ι, ‖x i‖ ^ p) (1 / p) ^ p < r ^ p}
    {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p}
⊢ {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 * p) < r ^ p}
  {a : ι → ℂ | ∑ i : ι, ‖a i‖ ^ p < r ^ p}
Tactic: simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hr), Set.preimage_setOf_eq, Pi.smul_apply,
        norm_smul, mul_rpow (norm_nonneg _) (norm_nonneg _), Real.norm_eq_abs, 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]