-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
_ :
  Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p)))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-b * |x.1| ^ p))) =
    HMul.hMul (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |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 (-b * |x| ^ p)
_₃ :
  (2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x ^ (q + 1) * rexp (-b * x ^ p)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
have _₄ : (2 * π *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-b * x ^ p)) =
  2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
Tactic: calc
    _ = ∫ x in Ioi (0 : ℝ) ×ˢ Ioo (-π) π, x.1 * (|x.1| ^ q * rexp (-b * |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 (-b * |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 (-b * |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 (-b * 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 * π / p) * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p) := by
      rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc,
        one_add_one_eq_two]
      ring