-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
rw :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (r * 0))) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₁ :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₂ :
  ((↑r⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₃ :
  ((↑(1 / r) : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₄ :
  ((↑1 : ℂ) / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₅ rw₆ :
  (1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑(r * t) : ℂ) ^ (a - 1) * cexp (-(↑(r * t) : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))

Tactic:
rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]

Premises used: Complex.real_smul, HMul.hMul, HSub.hSub, Complex.ofReal_one, Complex.ofReal, MulZeroClass.mul_zero, HPow.hPow, one_div, Complex.exp, Complex.ofReal_div, MeasureTheory.integral_comp_mul_left_Ioi, OfNat.ofNat, Neg.neg