awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw₁ :
  (↑s : ℂ).GammaIntegral.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₂ : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          rexp (-x) * x ^ (s - 1)) :
      ℂ).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)
rw₁ :
  (↑s : ℂ).GammaIntegral.re =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1)
rw₂ :
  (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
            rexp (-x) * x ^ (s - 1)) :
        ℂ).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₃ : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    rexp (-x) * x ^ (s - 1))
  (@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 : s ≠ 0
⊢ (Complex.Gamma (↑(s + 1) : ℂ)).re = s * (Complex.Gamma (↑s : ℂ)).re
have h2 : (↑s : ℂ) ≠ 0
Tactic: rw [Complex.ofReal_add, Complex.ofReal_one, Complex.Gamma_add_one, Complex.re_ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
⊢ Gamma 1 = 1
have rw : (Complex.Gamma (↑1 : ℂ)).re = 1
Tactic: rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
rw : (Complex.Gamma (↑1 : ℂ)).re = 1
⊢ Gamma 1 = 1
have rw₁ : (Complex.Gamma 1).re = 1
Tactic: rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
rw : (Complex.Gamma (↑1 : ℂ)).re = 1
rw₁ : (Complex.Gamma 1).re = 1
⊢ Gamma 1 = 1
have rw₂ : Complex.re 1 = 1
Tactic: rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
rw : (Complex.Gamma (↑1 : ℂ)).re = 1
rw₁ : (Complex.Gamma 1).re = 1
rw₂ : Complex.re 1 = 1
⊢ Gamma 1 = 1
have rw₃ : Eq (α := ℝ) 1 1
Tactic: rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
⊢ Complex.Gamma (↑s : ℂ) = (↑(Gamma s) : ℂ)
have rw : Complex.Gamma (↑s : ℂ) = (↑(Complex.Gamma (↑s : ℂ)).re : ℂ)
Tactic: rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
rw : Complex.Gamma (↑s : ℂ) = (↑(Complex.Gamma (↑s : ℂ)).re : ℂ)
⊢ Complex.Gamma (↑s : ℂ) = (↑(Gamma s) : ℂ)
have rw₁ : (↑(Complex.Gamma (↑s : ℂ)).re : ℂ) = Complex.Gamma (↑s : ℂ)
Tactic: rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
rw : Complex.Gamma (↑s : ℂ) = (↑(Complex.Gamma (↑s : ℂ)).re : ℂ)
rw₁ : (↑(Complex.Gamma (↑s : ℂ)).re : ℂ) = Complex.Gamma (↑s : ℂ)
⊢ Complex.Gamma (↑s : ℂ) = (↑(Gamma s) : ℂ)
have rw₂ : (starRingEnd ℂ : (a : ℂ) → ℂ) (Complex.Gamma (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
Tactic: rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
rw : Complex.Gamma (↑s : ℂ) = (↑(Complex.Gamma (↑s : ℂ)).re : ℂ)
rw₁ : (↑(Complex.Gamma (↑s : ℂ)).re : ℂ) = Complex.Gamma (↑s : ℂ)
rw₂ : (starRingEnd ℂ : (a : ℂ) → ℂ) (Complex.Gamma (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
⊢ Complex.Gamma (↑s : ℂ) = (↑(Gamma s) : ℂ)
have rw₃ : Complex.Gamma ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
Tactic: rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
rw : Complex.Gamma (↑s : ℂ) = (↑(Complex.Gamma (↑s : ℂ)).re : ℂ)
rw₁ : (↑(Complex.Gamma (↑s : ℂ)).re : ℂ) = Complex.Gamma (↑s : ℂ)
rw₂ : (starRingEnd ℂ : (a : ℂ) → ℂ) (Complex.Gamma (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
rw₃ : Complex.Gamma ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑s : ℂ)) = Complex.Gamma (↑s : ℂ)
⊢ Complex.Gamma (↑s : ℂ) = (↑(Gamma s) : ℂ)
have rw₄ : Complex.Gamma (↑s : ℂ) = Complex.Gamma (↑s : ℂ)
Tactic: rw [Gamma, eq_comm, ← Complex.conj_eq_iff_re, ← Complex.Gamma_conj, Complex.conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw₂ : (Complex.Gamma ((↑n : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₂ : (Complex.Gamma ((↑n : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw₃ : (Complex.Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)).re = (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₂ : (Complex.Gamma ((↑n : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₃ : (Complex.Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)).re = (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw₄ : Complex.re (↑n ! : ℂ) = (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₂ : (Complex.Gamma ((↑n : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₃ : (Complex.Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)).re = (↑n ! : ℝ)
rw₄ : Complex.re (↑n ! : ℂ) = (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw₅ : (↑(↑n ! : ℝ) : ℂ).re = (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
rw : (Complex.Gamma (↑(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) : ℂ)).re = (↑n ! : ℝ)
rw₁ : (Complex.Gamma ((↑(↑n : ℝ) : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₂ : (Complex.Gamma ((↑n : ℂ) + (↑1 : ℂ))).re = (↑n ! : ℝ)
rw₃ : (Complex.Gamma (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)).re = (↑n ! : ℝ)
rw₄ : Complex.re (↑n ! : ℂ) = (↑n ! : ℝ)
rw₅ : (↑(↑n ! : ℝ) : ℂ).re = (↑n ! : ℝ)
⊢ Gamma (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) = (↑n ! : ℝ)
have rw₆ : Eq (α := ℝ) (↑n ! : ℝ) (↑n ! : ℝ)
Tactic: rw [Gamma, Complex.ofReal_add, Complex.ofReal_natCast, Complex.ofReal_one,
    Complex.Gamma_nat_eq_factorial, ← Complex.ofReal_natCast, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ 0 < Gamma s
have rw : LT.lt (α := ℝ) 0
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    rexp (-x) * x ^ (s - 1))
Tactic: rw [Gamma_eq_integral hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
have rw : Subset (α := Set ℝ) (Ioi 0) (Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1))
Tactic: rw [inter_eq_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℝ
hs : 0 < s
⊢ LT.lt (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
have this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
Tactic: have : (Function.support fun x : ℝ => exp (-x) * x ^ (s - 1)) ∩ Ioi 0 = Ioi 0 := by
    rw [inter_eq_right]
    intro x hx
    rw [Function.mem_support]
    exact mul_ne_zero (exp_pos _).ne' (rpow_pos_of_pos hx _).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ LT.lt (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
have rw : LT.lt (α := ENNReal) (0 : ENNReal)
  ((volume : (a : Set ℝ) → ENNReal) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) :
    ENNReal)
Tactic: rw [setIntegral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
rw :
  LT.lt (α := ENNReal) (0 : ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) :
      ENNReal)
⊢ LT.lt (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
have hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)
Tactic: rw [setIntegral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
rw :
  LT.lt (α := ENNReal) (0 : ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) :
      ENNReal)
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)
⊢ LT.lt (α := ℝ) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      rexp (-x) * x ^ (s - 1))
have hfi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 0) volume
Tactic: rw [setIntegral_pos_iff_support_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ LT.lt (α := ENNReal) (0 : ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) :
      ENNReal)
have rw : ENNReal.ofReal 0 < ⊤
Tactic: rw [this, volume_Ioi, ← ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 < s
this : Eq (α := Set ℝ) ((Function.support (M := ℝ) fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) ∩ Ioi 0) (Ioi 0)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)
have hf : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) x)
Tactic: refine eventually_of_mem (self_mem_ae_restrict measurableSet_Ioi) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 ≤ s
⊢ 0 ≤ Gamma s
have inl : ∀ (hs : LE.le (α := ℝ) 0 0), 0 ≤ Gamma 0
Tactic: obtain rfl | h := eq_or_lt_of_le hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : 0 ≤ s
inl : ∀ (hs : LE.le (α := ℝ) 0 0), 0 ≤ Gamma 0
⊢ 0 ≤ Gamma s
have inr : ∀ (h : 0 < s), 0 ≤ Gamma s
Tactic: obtain rfl | h := eq_or_lt_of_le hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (a - 1) * rexp (-(r * t))) =
    (1 / r) ^ a * Gamma a
have rw : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        t ^ (a - 1) * rexp (-(r * t))) :
    ℂ) =
  ((↑1 : ℂ) / (↑r : ℂ)) ^ (↑a : ℂ) * Complex.Gamma (↑a : ℂ)
Tactic: rw [← ofReal_inj, ofReal_mul, ← Gamma_ofReal, ofReal_cpow (by positivity), ofReal_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    ((↑1 : ℂ) / (↑r : ℂ)) ^ (↑a : ℂ) * Complex.Gamma (↑a : ℂ)
have h : (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        t ^ (a - 1) * rexp (-(r * t))) :
    ℂ) =
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))
Tactic: convert! integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ (↑(@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
          t ^ (a - 1) * rexp (-(r * t))) :
      ℂ) =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))
Tactic: refine integral_ofReal.symm.trans <| setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ ((↑a : ℂ) - 1) * cexp (-((↑r : ℂ) * (↑t : ℂ)))
have h : (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
have h : (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑(t ^ (a - 1)) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
Tactic: simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑(t ^ (a - 1)) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
⊢ (↑(t ^ (a - 1) * rexp (-(r * t))) : ℂ) = (↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
have h₁ : HMul.hMul (α := ℂ) (↑(t ^ (a - 1)) : ℂ) (↑(rexp (-(r * t))) : ℂ) = (↑(t ^ (a - 1)) : ℂ) * (↑(rexp (-(r * t))) : ℂ)
Tactic: simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
⊢ Gamma s ≠ 0
have a : -(↑(⌊-s⌋₊ + 1) : ℝ) < s
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
a : -(↑(⌊-s⌋₊ + 1) : ℝ) < s
⊢ Gamma s ≠ 0
have n : ℕ
Tactic: apply this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
this : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
⊢ -(↑(⌊-s⌋₊ + 1) : ℝ) < s
have a : -s < HAdd.hAdd (α := ℝ) (↑⌊-s⌋₊ : ℝ) 1
Tactic: rw [neg_lt, Nat.cast_add, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
⊢ Gamma s ≠ 0
have suffices : ∀ {n : ℕ}, -(↑n : ℝ) < s → Gamma s ≠ 0
Tactic: suffices ∀ {n : ℕ}, -(n : ℝ) < s → Gamma s ≠ 0 by
    apply this
    swap
    · exact ⌊-s⌋₊ + 1
    rw [neg_lt, Nat.cast_add, Nat.cast_one]
    exact Nat.lt_floor_add_one _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs_1 : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs : -(↑0 : ℝ) < s
⊢ Gamma s ≠ 0
have zero : 0 < s
Tactic: refine (Gamma_pos_of_pos ?_).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs_1 : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs : -(↑0 : ℝ) < s
⊢ 0 < s
have zero : ∀ (hs : -0 < s), 0 < s
Tactic: rwa [Nat.cast_zero, neg_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
hs_1 : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs : -(↑0 : ℝ) < s
zero : ∀ (hs : -0 < s), 0 < s
⊢ 0 < s
have zero₁ : ∀ (hs : 0 < s), 0 < s
Tactic: rwa [Nat.cast_zero, neg_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
⊢ Gamma (s + 1) ≠ 0
have hs₁ : ∀ (m : ℕ), s + 1 ≠ -(↑m : ℝ)
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
hs₁ : ∀ (m : ℕ), s + 1 ≠ -(↑m : ℝ)
⊢ Gamma (s + 1) ≠ 0
have a : -(↑n : ℝ) < s + 1
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
⊢ s + 1 ≠ -(↑m : ℝ)
have hs₁ : s ≠ -(↑(1 + m) : ℝ)
Tactic: specialize hs (1 + m)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s ≠ -(↑(1 + m) : ℝ)
⊢ s + 1 ≠ -(↑m : ℝ)
have hs₁ : ∀ (hs : s + 1 = -(↑m : ℝ)), s = -(↑(1 + m) : ℝ)
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s + 1 = -(↑m : ℝ)
⊢ s = -(↑(1 + m) : ℝ)
have hs₁ : s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1
Tactic: rw [← eq_sub_iff_add_eq] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1
⊢ s = -(↑(1 + m) : ℝ)
have hs₁ : HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -(↑(1 + m) : ℝ)
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs' : -(↑(n + 1) : ℝ) < s
m : ℕ
hs : s = HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1
⊢ HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -(↑(1 + m) : ℝ)
have hs₁ : HSub.hSub (α := ℝ) (-(↑m : ℝ)) 1 = -HAdd.hAdd (α := ℝ) 1 (↑m : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
⊢ -(↑n : ℝ) < s + 1
have hs'₁ : HAdd.hAdd (α := ℝ) (-(↑n : ℝ)) (-1) < s
Tactic: rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : HAdd.hAdd (α := ℝ) (-(↑n : ℝ)) (-1) < s
⊢ -(↑n : ℝ) < s + 1
have linarith : s + 1 ≤ -(↑n : ℝ) → HAdd.hAdd (α := ℝ) (-(↑n : ℝ)) (-1) - s + (s + 1 - -(↑n : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
⊢ Gamma s ≠ 0
have this : Gamma (s + 1) ≠ 0
Tactic: have : Gamma (s + 1) ≠ 0 := by
      apply n_ih
      · intro m
        specialize hs (1 + m)
        contrapose hs
        rw [← eq_sub_iff_add_eq] at hs
        rw [hs]
        push_cast
        ring
      · rw [Nat.cast_add, Nat.cast_one, neg_add] at hs'
        linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
n : ℕ
n_ih : ∀ {s : ℝ} (hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)), -(↑n : ℝ) < s → Gamma s ≠ 0
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
hs' : -(↑(n + 1) : ℝ) < s
this : Gamma (s + 1) ≠ 0
⊢ Gamma s ≠ 0
have succ : ∀ (this : s ≠ 0 ∧ Gamma s ≠ 0), Gamma s ≠ 0
Tactic: rw [Gamma_add_one, mul_ne_zero_iff] at this
Cleared hypotheses: this