awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ 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) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)
have simp_rw₂ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |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 (-b * |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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ 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) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)
have simp_rw₃ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p)) *
    HSMul.hSMul (β := ℝ) (π - -π) 1 =
  2 * π *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₃ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)) *
      HSMul.hSMul (β := ℝ) (π - -π) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ 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) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)
have simp_rw₄ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p)) *
    HSMul.hSMul (β := ℝ) (π + π) 1 =
  2 * π *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |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 (-b * |x| ^ p)
simp_rw₃ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)) *
      HSMul.hSMul (β := ℝ) (π - -π) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)
simp_rw₄ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)) *
      HSMul.hSMul (β := ℝ) (π + π) 1 =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ 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) =
    2 * π *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        x * |x| ^ q * rexp (-b * |x| ^ p)
have simp_rw₅ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p)) *
    HSMul.hSMul (β := ℝ) (2 * π) 1 =
  2 * π *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ (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)
have e_a : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    x * |x| ^ q * rexp (-b * |x| ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    x ^ (q + 1) * rexp (-b * x ^ p))
Tactic: congr 1
-- 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 (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x * |x| ^ q * rexp (-b * |x| ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-b * x ^ p))
have e_a : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun x hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (hypothesis)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)
have hx₁ : 0 < x
Tactic: rw [mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
x : ℝ
hx : 0 < x
⊢ x * |x| ^ q * rexp (-b * |x| ^ p) = x ^ (q + 1) * rexp (-b * x ^ p)
have e_a : x * x ^ q * rexp (-b * x ^ p) = x ^ q * x * rexp (-b * x ^ p)
Tactic: rw [abs_eq_self.mpr hx.le, rpow_add hx, rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ 0 < p
have linarith : p ≤ 0 → -1 + (1 - p) + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ -1 < q + 1
have linarith : q + 1 ≤ -1 → -2 - q + (q + 1 - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ (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)
have rw : 2 * π * (b ^ (-(q + 2) / p) * (1 / p) * Real.Gamma ((q + 2) / p)) =
  2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
Tactic: rw [_root_.integral_rpow_mul_exp_neg_mul_rpow (by linarith) (by linarith) hb, add_assoc,
        one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 1 ≤ p
hq : -2 < q
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
have _ : 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)))
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
-- 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 volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
have _₁ : (@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)
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
-- 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)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p)) =
    2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
have _₂ : 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)
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
-- 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)
⊢ (@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 * |x| ^ q * rexp (-b * |x| ^ p)) =
  2 * π *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ (q + 1) * rexp (-b * x ^ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ LT.lt (α := ℝ) (-2) 0
have linarith : LE.le (α := ℝ) 0 (-2) → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (-2) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
linarith : LE.le (α := ℝ) 0 (-2) → HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (-2) = 0
⊢ LT.lt (α := ℝ) (-2) 0
have linarith₁ : LE.le (α := ℝ) 0 (-2) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p)) = π * Real.Gamma (2 / p + 1)
have h : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ rexp (-‖x‖ ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℂ) ↦ HPow.hPow (β := ℝ) ‖x‖ 0 * rexp (-‖x‖ ^ p))
Tactic: convert! (integral_rpow_mul_exp_neg_rpow hp (by linarith : (-2 : ℝ) < 0)) using 1