awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 0 < p
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-x ^ p))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p)) =
    Gamma (1 / p + 1)
have h₁ : Gamma (1 / p + 1) = 1 / p * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
Tactic: convert! (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 0 < p
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-x ^ p))
have h : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ 1 * rexp (-x ^ p))
Tactic: simp_rw [rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
have h : Gamma (1 / p + 1) = 1 / p * Gamma (1 / p)
Tactic: rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 0 < p
h : Gamma (1 / p + 1) = 1 / p * Gamma (1 / p)
⊢ Gamma (1 / p + 1) = 1 / p * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
have h₁ : 1 / p * Gamma (1 / p) = 1 / p * Gamma (1 / p)
Tactic: rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p)) =
    b ^ (-1 / p) * Gamma (1 / p + 1)
have h : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    HPow.hPow (β := ℝ) x 0 * rexp (-b * x ^ p))
Tactic: convert! (integral_rpow_mul_exp_neg_mul_rpow hp neg_one_lt_zero hb) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
h :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-b * x ^ p))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p)) =
    b ^ (-1 / p) * Gamma (1 / p + 1)
have h₁ : b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
Tactic: convert! (integral_rpow_mul_exp_neg_mul_rpow hp neg_one_lt_zero hb) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HPow.hPow (β := ℝ) x 0 * rexp (-b * x ^ p))
have h : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-b * x ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 * rexp (-b * x ^ p))
Tactic: simp_rw [rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
have h : b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
Tactic: rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp)), mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
h : b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
have h₁ : b ^ (-1 / p) * (1 / p * Gamma (1 / p)) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
Tactic: rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp)), mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p b : ℝ
hp : 0 < p
hb : 0 < b
h : b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
h₁ : b ^ (-1 / p) * (1 / p * Gamma (1 / p)) = b ^ (-1 / p) * (1 / p) * Gamma (1 / p)
⊢ b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-HAdd.hAdd (α := ℝ) 0 1 / p) * (1 / p) * Gamma (HAdd.hAdd (α := ℝ) 0 1 / p)
have h₂ : b ^ (-1 / p) * (1 / p * Gamma (1 / p)) = b ^ (-1 / p) * (1 / p * Gamma (1 / p))
Tactic: rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp)), mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
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)))
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
    p_1.1 •
      (‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ q * rexp (-‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_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)))
Tactic: rw [← Complex.integral_comp_polarCoord_symm, polarCoord_target]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
      p_1.1 •
        (‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_1‖ ^ q * rexp (-‖(↑Complex.polarCoord.symm : ℝ × ℝ → ℂ) p_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)))
have simp_rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (Measure.restrict volume (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (p_1 : ℝ × ℝ) ↦
    p_1.1 • (|p_1.1| ^ q * rexp (-|p_1.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)))
Tactic: simp_rw [Complex.norm_polarCoord_symm, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ (@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)
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
    x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
    z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1)
Tactic: rw [← setIntegral_prod_mul, volume_eq_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-|z.1| ^ p) * 1)
have simp_rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
    (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
    x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
    z.1 * |z.1| ^ q * rexp (-|z.1| ^ p))
Tactic: simp_rw [mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (x : ℝ × ℝ) ↦
      x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      z.1 * |z.1| ^ q * rexp (-|z.1| ^ p))
have h : ∀ (x : ℝ × ℝ), x.1 * (|x.1| ^ q * rexp (-|x.1| ^ p)) = x.1 * |x.1| ^ q * rexp (-|x.1| ^ p)
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ -π ≤ π
have linarith : π < -π → π - -π + 2 * (0 - π) = 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
linarith : π < -π → π - -π + 2 * (0 - π) = 0
⊢ -π ≤ π
have linarith₁ : π < -π → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 1 ≤ p
hq : -2 < q
⊢ 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)) *
    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)
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 : ℝ
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)
⊢ 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)) *
    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)
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 : ℝ
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)
⊢ 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)) *
    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)
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 : ℝ
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)
⊢ 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)) *
    HSMul.hSMul (β := ℝ) (π - -π) 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]
-- 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)
⊢ 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)) *
    HSMul.hSMul (β := ℝ) (π + π) 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]
-- 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)
⊢ 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)) *
    HSMul.hSMul (β := ℝ) (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]