-- Module: Mathlib.Analysis.MellinTransform
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)
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)
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)
rw₇ :
  HSMul.hSMul (β := E) (HPow.hPow (β := ℂ) (↑a : ℂ) 1 * (↑a : ℂ) ^ (-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)
rw₈ :
  HSMul.hSMul (β := E) ((↑a : ℂ) * (↑a : ℂ) ^ (-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)
rw₉ :
  HSMul.hSMul (β := E) ((↑a : ℂ) * (↑a : ℂ) ^ (-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)
rw₁₀ :
  HSMul.hSMul (β := E) ((↑a : ℂ) * ((↑a : ℂ) ^ (-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)
rw₁₁ :
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s) * (↑a : ℂ)⁻¹ * (↑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₁₂ rw₁₃ :
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@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)

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')]

Premises used: Iff.mpr, mul_assoc, MeasureTheory.integral_smul, sub_eq_add_neg, HSub.hSub, Complex.ofReal_ne_zero, measurableSet_Ioi, Complex.ofReal, MulZeroClass.mul_zero, LT.lt.ne', MeasureTheory.setIntegral_congr_fun, Complex.cpow_one, HPow.hPow, Complex.coe_smul, Complex.cpow_add, mul_comm, HSMul.hSMul, MeasureTheory.integral_comp_mul_left_Ioi, OfNat.ofNat, Complex.ofReal_inv, SemigroupAction.mul_smul, inv_mul_cancel_right₀