awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
⊢ HDiv.hDiv (β := ℂ) (GammaAux n (HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)))
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n (s + 1)) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ)
have succ : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1)
Tactic: suffices conj s + 1 = conj (s + 1) by rw [this, IH]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1)
have succ : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
Tactic: rw [map_add, map_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s_1 : ℂ
n : ℕ
IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
s : ℂ
succ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ)
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) = (starRingEnd ℂ : (a : ℂ) → ℂ) (s + 1)
have succ₁ : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)
Tactic: rw [map_add, map_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
have zero : ∀ (s : ℂ), GammaAux 0 ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux 0 s)
Tactic: induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [map_add, map_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
n : ℕ
zero : ∀ (s : ℂ), GammaAux 0 ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux 0 s)
⊢ ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s)
have succ : ∀ (n : ℕ) (IH : ∀ (s : ℂ), GammaAux n ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux n s))
  (s : ℂ), GammaAux (n + 1) ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) (GammaAux (n + 1) s)
Tactic: induction n with
  | zero => rw [GammaAux]; exact GammaIntegral_conj
  | succ n IH =>
    intro s
    rw [GammaAux]
    dsimp only
    rw [div_eq_mul_inv _ s, map_mul, conj_inv, ← div_eq_mul_inv]
    suffices conj s + 1 = conj (s + 1) by rw [this, IH]
    rw [map_add, map_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
have nth_rewrite : (1 / (↑r : ℂ)) ^ a = HPow.hPow (β := ℂ) (1 / (↑r : ℂ)) 1 * (1 / (↑r : ℂ)) ^ (a - 1)
Tactic: nth_rewrite 2 [← cpow_one (1 / r : ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (1 / (↑r : ℂ)) ^ a = HPow.hPow (β := ℂ) (1 / (↑r : ℂ)) 1 * (1 / (↑r : ℂ)) ^ (a - 1)
have rw : (1 / (↑r : ℂ)) ^ a = (1 / (↑r : ℂ)) ^ (1 + (a - 1))
Tactic: rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
rw : (1 / (↑r : ℂ)) ^ a = (1 / (↑r : ℂ)) ^ (1 + (a - 1))
⊢ (1 / (↑r : ℂ)) ^ a = HPow.hPow (β := ℂ) (1 / (↑r : ℂ)) 1 * (1 / (↑r : ℂ)) ^ (a - 1)
have rw₁ : (1 / (↑r : ℂ)) ^ a = (1 / (↑r : ℂ)) ^ a
Tactic: rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))) =
    (1 / (↑r : ℂ)) ^ a * Gamma a
have aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
Tactic: have aux : (1 / r : ℂ) ^ a = 1 / r * (1 / r) ^ (a - 1) := by
    nth_rewrite 2 [← cpow_one (1 / r : ℂ)]
    rw [← cpow_add _ _ (one_div_ne_zero <| ofReal_ne_zero.mpr hr.ne'), add_sub_cancel]
-- 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 : ℂ))))
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
a : ℂ
r : ℝ
ha : 0 < a.re
hr : 0 < r
aux : (1 / (↑r : ℂ)) ^ a = 1 / (↑r : ℂ) * (1 / (↑r : ℂ)) ^ (a - 1)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have hx₁ : 0 < x
Tactic: rw [mem_Ioi] at hx
Cleared hypotheses: hx
-- 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 : ℝ
hx : 0 < x
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₁ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₂ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₃ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₄ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₄ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₅ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  (↑(r⁻¹ * r) : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₄ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₅ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑(r⁻¹ * r) : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₆ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  (↑1 : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₄ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₅ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑(r⁻¹ * r) : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₆ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑1 : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₇ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
  HPow.hPow (α := ℂ) 1 (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₄ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₅ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑(r⁻¹ * r) : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₆ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑1 : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₇ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    HPow.hPow (α := ℂ) 1 (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₈ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) = 1 * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ
hx : 0 < x
rw :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1)) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₁ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₂ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r : ℂ)⁻¹ ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₃ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑r⁻¹ : ℂ) ^ (a - 1) * (↑r : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₄ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    ((↑r⁻¹ : ℂ) * (↑r : ℂ)) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₅ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑(r⁻¹ * r) : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₆ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (↑1 : ℂ) ^ (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₇ :
  (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    HPow.hPow (α := ℂ) 1 (a - 1) * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
rw₈ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) = 1 * (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
⊢ (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) =
    (1 / (↑r : ℂ)) ^ (a - 1) * ((↑r : ℂ) * (↑x : ℂ)) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
have rw₉ : (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ))) = (↑x : ℂ) ^ (a - 1) * cexp (-((↑r : ℂ) * (↑x : ℂ)))
Tactic: 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]
-- 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 : ℝ) ↦
      (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 simp_rw : (@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: simp_rw [← ofReal_mul]
-- 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 : ℝ) ↦
      (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 : 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 : ℂ))
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 : ℂ))
⊢ (@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₁ : 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 : ℂ))
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]