-- Module: Mathlib.MeasureTheory.Integral.Gamma
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
_ :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (x : ℝ) ↦ 1)
_₂ :
  HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (x : ℝ) ↦ 1) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
_₃ :
  (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-x ^ p)
_₄ :
  (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-x ^ p)) =
    2 * π / p * Real.Gamma ((q + 2) / p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-‖x‖ ^ p)) =
    2 * π / p * Real.Gamma ((q + 2) / p)

Tactic:
calc
    _ = ∫ x in Ioi (0 : ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) := by
      rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]
      simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]
    _ = (∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (-|x| ^ p)) * ∫ _ in Ioo (-π) π, 1 := by
      rw [← setIntegral_prod_mul, volume_eq_prod]
      simp_rw [mul_one]
      congr! 2; ring
    _ = 2 * π * ∫ x in Ioi (0 : ℝ), x * |x| ^ q * rexp (-|x| ^ p) := by
      simp_rw [integral_const, measureReal_restrict_apply MeasurableSet.univ, Set.univ_inter,
        volume_real_Ioo_of_le (a := -π) (b := π) (by linarith [pi_nonneg]),
        sub_neg_eq_add, ← two_mul, smul_eq_mul, mul_one, mul_comm]
    _ = 2 * π * ∫ x in Ioi (0 : ℝ), x ^ (q + 1) * rexp (-x ^ p) := by
      congr 1
      refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)
      rw [mem_Ioi] at hx
      rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]
      ring
    _ = (2 * Real.pi / p) * Real.Gamma ((q + 2) / p) := by
      rw [_root_.integral_rpow_mul_exp_neg_rpow (by linarith) (by linarith), add_assoc,
        one_add_one_eq_two]
      ring

Premises used: Set.Ioi, Real.pi, HMul.hMul, abs, MeasureTheory.Measure.restrict, HDiv.hDiv, Real.exp, HPow.hPow, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, MeasureTheory.integral, Real.Gamma, OfNat.ofNat, Set.Ioo, Neg.neg