awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
Tactic: rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
        abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
have rw : (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x ^ (1 / p * p))) =
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
Tactic: rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x ^ (1 / p * p))) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
⊢ (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
have rw₁ : (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-HPow.hPow (β := ℝ) x 1)) =
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
Tactic: rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x ^ (1 / p * p))) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
rw₁ :
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-HPow.hPow (β := ℝ) x 1)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
⊢ (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-(x ^ (1 / p)) ^ p)) =
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
have rw₂ : (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)) =
  (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x))
Tactic: rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p))
have simp_rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p)))
Tactic: simp_rw [smul_eq_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p)))
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))) = 1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p))
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 1 / p * (x ^ (1 / p - 1) * ((x ^ (1 / p)) ^ q * rexp (-x))) = 1 / p * (rexp (-x) * x ^ (1 / p - 1 + q / p))
have rw : x ^ (1 / p - 1) * (x ^ (1 / p * q) * rexp (-x)) / p = 1 / p * (rexp (-x) * (x ^ (1 / p - 1) * x ^ (q / p)))
Tactic: rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
    1 / p * Gamma ((q + 1) / p)
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
  1 / p *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ ((q + 1) / p - 1)
Tactic: rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
    1 / p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ ((q + 1) / p - 1)
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * rexp (-x) * x ^ ((q + 1) / p - 1)) =
  1 / p *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ ((q + 1) / p - 1)
Tactic: simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by ring, ← integral_const_mul,
        ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ ((q + 1) / p - 1)) =
    1 / p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ ((q + 1) / p - 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
    1 / p *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        rexp (-x) * x ^ ((q + 1) / p - 1)
have simp_rw₁ : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * rexp (-x) * x ^ ((q + 1) / p - 1))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
    1 / p * (rexp (-a) * a ^ ((q + 1) / p - 1)))
Tactic: simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by ring, ← integral_const_mul,
        ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p)) =
    1 / p * Gamma ((q + 1) / p)
have _ : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    x ^ q * rexp (-x ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
Tactic: calc
    _ = ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * exp (-x)) := by
      rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
        abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
    _ = ∫ (x : ℝ) in Ioi 0, 1 / p * exp (-x) * x ^ (1 / p - 1 + q / p) := by
      simp_rw [smul_eq_mul, mul_assoc]
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]
      ring_nf
    _ = (1 / p) * Gamma ((q + 1) / p) := by
      rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
      simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by ring, ← integral_const_mul,
        ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
_ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p)) =
    1 / p * Gamma ((q + 1) / p)
have _₁ : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p))
Tactic: calc
    _ = ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * exp (-x)) := by
      rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
        abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
    _ = ∫ (x : ℝ) in Ioi 0, 1 / p * exp (-x) * x ^ (1 / p - 1 + q / p) := by
      simp_rw [smul_eq_mul, mul_assoc]
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]
      ring_nf
    _ = (1 / p) * Gamma ((q + 1) / p) := by
      rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
      simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by ring, ← integral_const_mul,
        ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q : ℝ
hp : 0 < p
hq : -1 < q
_ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
_₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * rexp (-x)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-x ^ p)) =
    1 / p * Gamma ((q + 1) / p)
have _₂ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    1 / p * rexp (-x) * x ^ (1 / p - 1 + q / p)) =
  1 / p * Gamma ((q + 1) / p)
Tactic: calc
    _ = ∫ (x : ℝ) in Ioi 0, (1 / p * x ^ (1 / p - 1)) • ((x ^ (1 / p)) ^ q * exp (-x)) := by
      rw [← integral_comp_rpow_Ioi _ (one_div_ne_zero (ne_of_gt hp)),
        abs_eq_self.mpr (le_of_lt (one_div_pos.mpr hp))]
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [← rpow_mul (le_of_lt hx) _ p, one_div_mul_cancel (ne_of_gt hp), rpow_one]
    _ = ∫ (x : ℝ) in Ioi 0, 1 / p * exp (-x) * x ^ (1 / p - 1 + q / p) := by
      simp_rw [smul_eq_mul, mul_assoc]
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [← rpow_mul (le_of_lt hx), div_mul_eq_mul_div, one_mul, rpow_add hx]
      ring_nf
    _ = (1 / p) * Gamma ((q + 1) / p) := by
      rw [Gamma_eq_integral (div_pos (neg_lt_iff_pos_add.mp hq) hp)]
      simp_rw [show 1 / p - 1 + q / p = (q + 1) / p - 1 by ring, ← integral_const_mul,
        ← mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  x ^ q * rexp (-b * x ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hx₁ : 0 < b
⊢ x ^ q * rexp (-b * x ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))
have rw : p ≠ 0
Tactic: rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hx₁ : 0 < b
rw : p ≠ 0
⊢ x ^ q * rexp (-b * x ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))
have hx₂ : 0 ≤ b
Tactic: rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
hx₁ : 0 < b
rw : p ≠ 0
hx₂ hx₃ : 0 ≤ b
⊢ x ^ q * rexp (-b * x ^ p) = b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))
have rw₁ : 0 ≤ b ^ p⁻¹
Tactic: rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))) =
    (b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))
have rw : 0 < b ^ p⁻¹
Tactic: rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ ((b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
have rw : b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
rw : b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))
hx : 0 < b
⊢ ((b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
have hx₁ : 0 ≤ b
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))
have e_a : p⁻¹ * -1 + -p⁻¹ * q = -(q + 1) / p
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p)) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
have _ : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    x ^ q * rexp (-b * x ^ p))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))
Tactic: calc
    _ = ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) := by
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
      all_goals positivity
    _ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) := by
      rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
      all_goals positivity
    _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by
      rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
      · congr; ring
      all_goals positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
_ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p)) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
have _₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))) =
  (b ^ p⁻¹)⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))
Tactic: calc
    _ = ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) := by
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
      all_goals positivity
    _ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) := by
      rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
      all_goals positivity
    _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by
      rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
      · congr; ring
      all_goals positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
_ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p))) =
    (b ^ p⁻¹)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      x ^ q * rexp (-b * x ^ p)) =
    b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
have _₂ : ((b ^ p⁻¹)⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p))) =
  b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p)
Tactic: calc
    _ = ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * ((b ^ p⁻¹ * x) ^ q * rexp (-(b ^ p⁻¹ * x) ^ p)) := by
      refine setIntegral_congr_fun measurableSet_Ioi (fun _ hx => ?_)
      rw [mul_rpow _ (le_of_lt hx), mul_rpow _ (le_of_lt hx), ← rpow_mul, ← rpow_mul,
        inv_mul_cancel₀, rpow_one, mul_assoc, ← mul_assoc, ← rpow_add, neg_mul p⁻¹, neg_add_cancel,
        rpow_zero, one_mul, neg_mul]
      all_goals positivity
    _ = (b ^ p⁻¹)⁻¹ * ∫ x in Ioi (0 : ℝ), b ^ (-p⁻¹ * q) * (x ^ q * rexp (-x ^ p)) := by
      rw [integral_comp_mul_left_Ioi (fun x => b ^ (-p⁻¹ * q) * (x ^ q * exp (-x ^ p))) 0,
        mul_zero, smul_eq_mul]
      all_goals positivity
    _ = b ^ (-(q + 1) / p) * (1 / p) * Gamma ((q + 1) / p) := by
      rw [integral_const_mul, integral_rpow_mul_exp_neg_rpow _ hq, mul_assoc, ← mul_assoc,
        ← rpow_neg_one, ← rpow_mul, ← rpow_add]
      · congr; ring
      all_goals positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Gamma (goal)
Goal:
p : ℝ
hp : 0 < p
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦ rexp (-x ^ p)) =
    Gamma (1 / p + 1)
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 : ℝ) ↦
    HPow.hPow (β := ℝ) x 0 * rexp (-x ^ p))
Tactic: convert! (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1