-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  EqOn.{0, u_1} (β := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
    (fun (t : ℝ) ↦ HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * t))) (Ioi 0)
rw :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * x))) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₁ :
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * a_1)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₂ :
  (↑a : ℂ) ^ (1 - s) •
      HSMul.hSMul (β := E) a⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (a * 0))) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1) • f x) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₃ :
  (↑a : ℂ) ^ (1 - s) •
      HSMul.hSMul (β := E) a⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1) • f x) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₄ :
  (↑a : ℂ) ^ (1 - s) •
      HSMul.hSMul (β := E) (↑a⁻¹ : ℂ)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1) • f x) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (a * t)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
have rw₅ : HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s) * (↑a⁻¹ : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑x : ℂ) ^ (s - 1) • f x) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr ha.ne')]