awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
rw :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (r * 0))) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₁ :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑(r * t) : ℂ) ^ (a - 1) * cexp (-(↑(r * t) : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
have rw₂ : ((↑r⁻¹ : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
  1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
Tactic: rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
rw :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (r * 0))) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₁ :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₂ :
  ((↑r⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑(r * t) : ℂ) ^ (a - 1) * cexp (-(↑(r * t) : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
have rw₃ : ((↑(1 / r) : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
  1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
Tactic: rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
rw :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (r * 0))) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₁ :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₂ :
  ((↑r⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₃ :
  ((↑(1 / r) : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑(r * t) : ℂ) ^ (a - 1) * cexp (-(↑(r * t) : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
have rw₄ : ((↑1 : ℂ) / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
  1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
Tactic: rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
rw :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (r * 0))) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₁ :
  HSMul.hSMul (β := ℂ) r⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₂ :
  ((↑r⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₃ :
  ((↑(1 / r) : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
rw₄ :
  ((↑1 : ℂ) / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑(r * t) : ℂ) ^ (a - 1) * cexp (-(↑(r * t) : ℂ))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
have rw₅ : (1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ))) =
  1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
Tactic: rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
⊢ (1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
have simp_rw : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
    1 / (↑r : ℂ) * ((1 / (↑r : ℂ)) ^ (a - 1) * (↑a_1 : ℂ) ^ (a - 1) * cexp (-(↑a_1 : ℂ))))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) * ((↑a_1 : ℂ) ^ (a - 1) * cexp (-(↑a_1 : ℂ))))
Tactic: simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
⊢ (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
have rw : (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
  1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) * a.GammaIntegral
Tactic: rw [aux, Gamma_eq_integral ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
⊢ (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) * a.GammaIntegral
have e_a : ∀ (x : ℝ), (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (a - 1)
Tactic: congr 2 with x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (a - 1)
have e_a : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (↑(-x) : ℂ) * (↑x : ℂ) ^ (a - 1)
Tactic: rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
e_a : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (↑(-x) : ℂ) * (↑x : ℂ) ^ (a - 1)
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (a - 1)
have e_a₁ : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1)
Tactic: rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
e_a : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (↑(-x) : ℂ) * (↑x : ℂ) ^ (a - 1)
e_a₁ : (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1)
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-(↑x : ℂ)) = (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (a - 1)
have e_a₂ : cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1) = cexp (-(↑x : ℂ)) * (↑x : ℂ) ^ (a - 1)
Tactic: rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
have _ : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
Tactic: calc
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by
      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
      rw [mem_Ioi] at hx
      rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]
    _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
    _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
      simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
    _ = (1 / r) ^ a * Gamma a := by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
_ :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
have _₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
  1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
Tactic: calc
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by
      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
      rw [mem_Ioi] at hx
      rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]
    _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
    _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
      simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
    _ = (1 / r) ^ a * Gamma a := by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
_ :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
have _₂ : (1 / (↑r : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
  1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
Tactic: calc
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by
      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
      rw [mem_Ioi] at hx
      rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]
    _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
    _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
      simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
    _ = (1 / r) ^ a * Gamma a := by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
_ :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ))))
_₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑t : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
_₂ :
  (1 / (↑r : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (1 / (↑r : ℂ)) ^ (a - 1) * (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
    1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
have _₃ : (1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-(↑t : ℂ))) =
  (1 / (↑r : ℂ)) ^ a * Gamma a
Tactic: calc
    _ = ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * (r * t) ^ (a - 1) * exp (-(r * t)) := by
      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
      rw [mem_Ioi] at hx
      rw [mul_cpow_ofReal_nonneg hr.le hx.le, ← mul_assoc, one_div, ← ofReal_inv,
        ← mul_cpow_ofReal_nonneg (inv_pos.mpr hr).le hr.le, ← ofReal_mul r⁻¹,
        inv_mul_cancel₀ hr.ne', ofReal_one, one_cpow, one_mul]
    _ = 1 / r * ∫ (t : ℝ) in Ioi 0, (1 / r) ^ (a - 1) * t ^ (a - 1) * exp (-t) := by
      simp_rw [← ofReal_mul]
      rw [integral_comp_mul_left_Ioi (fun x ↦ _ * x ^ (a - 1) * exp (-x)) _ hr, mul_zero,
        real_smul, ← one_div, ofReal_div, ofReal_one]
    _ = 1 / r * (1 / r : ℂ) ^ (a - 1) * (∫ (t : ℝ) in Ioi 0, t ^ (a - 1) * exp (-t)) := by
      simp_rw [← MeasureTheory.integral_const_mul, mul_assoc]
    _ = (1 / r) ^ a * Gamma a := by
      rw [aux, Gamma_eq_integral ha]
      congr 2 with x
      rw [ofReal_exp, ofReal_neg, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ Gamma s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
have rw : (Complex.Gamma (↑s : ℂ)).re =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    rexp (-x) * x ^ (s - 1)
Tactic: rw [Gamma, Complex.Gamma_eq_integral (RCLike.ofReal_pos.mp hs), Complex.GammaIntegral_ofReal,
    Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
rw :
  (Complex.Gamma (↑s : ℂ)).re =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
⊢ Gamma s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
have rw₁ : (↑s : ℂ).GammaIntegral.re =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    rexp (-x) * x ^ (s - 1)
Tactic: rw [Gamma, Complex.Gamma_eq_integral (RCLike.ofReal_pos.mp hs), Complex.GammaIntegral_ofReal,
    Complex.ofReal_re]