-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) *
      HSMul.hSMul (β := ℝ)
        (Measure.real (m := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (Ioo (-π) π)) univ) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) *
      HSMul.hSMul (β := ℝ) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (univ ∩ Ioo (-π) π)) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
simp_rw₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) *
      HSMul.hSMul (β := ℝ) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo (-π) π)) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
simp_rw₃ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) *
      HSMul.hSMul (β := ℝ) (π - -π) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
simp_rw₄ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) *
      HSMul.hSMul (β := ℝ) (π + π) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
simp_rw₅ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)) *
      HSMul.hSMul (β := ℝ) (2 * π) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ 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) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-|x| ^ p)
have simp_rw₆ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-|x| ^ p)) *
    (2 * π * 1) =
  2 * π *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-|x| ^ p)
Tactic: 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]