awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
F_der_I :
  ∀ x ∈ Ioo 0 X,
    HasDerivAt (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) x
cont : Continuous (HMul.hMul (α := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) fun (x : ℝ) ↦ (↑x : ℂ) ^ s)
der_ible :
  IntervalIntegrable (ε := ℂ)
    (fun (x : ℝ) ↦ -((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s) + (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) volume 0 X
int_eval :
  HAdd.hAdd (α := ℂ) (∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ s)
      (-∫ (x : ℝ) in 0..X, (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1))) =
    -(HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) X -
        HMul.hMul (α := ℝ → ℂ) (β := ℝ → ℂ) (ofReal ∘ fun (y : ℝ) ↦ rexp (-y)) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) 0)
hn : s ≠ 0
x : ℝ
⊢ (↑(rexp (-x)) : ℂ) * (s * (↑x : ℂ) ^ (s - 1)) = s * ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral

Tactic:
tendsto_nhds_unique ?_ this

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
refine : Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral

Tactic:
refine tendsto_nhds_unique ?_ this

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
hs₁ : 0 < (s + 1).re
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s + 1).GammaIntegral)

Tactic:
apply tendsto_partialGamma

Premises used: Complex.tendsto_partialGamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
linarith : s.re + 1 ≤ 0 → -1 + (0 - s.re) + (s.re + 1 - 0) = 0
⊢ 0 < s.re + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
suffices : Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))
⊢ (s + 1).GammaIntegral = s * s.GammaIntegral

Tactic:
suffices Tendsto (s + 1).partialGamma atTop (𝓝 <| s * GammaIntegral s) by
    refine tendsto_nhds_unique ?_ this
    apply tendsto_partialGamma; rw [add_re, one_re]; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
apply : EqOn (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) (s + 1).partialGamma (Ici 0)
⊢ (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma

Tactic:
apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))

Premises used: Filter.eventuallyEq_of_mem, Filter.Ici_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : Membership.mem (γ := Set ℝ) (Ici 0) X
rw :
  (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) X =
    s * s.partialGamma X - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s
⊢ (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) X = (s + 1).partialGamma X

Tactic:
rw [partialGamma_add_one hs (mem_Ici.mp hX)]

Premises used: Complex.partialGamma_add_one, Set.mem_Ici, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : Membership.mem (γ := Set ℝ) (Ici 0) X
⊢ (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) X =
    s * s.partialGamma X - (↑(rexp (-X)) : ℂ) * (↑X : ℂ) ^ s

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
⊢ (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma

Tactic:
have : (fun X : ℝ => s * partialGamma s X - X ^ s * (-X).exp) =ᶠ[atTop]
      (s + 1).partialGamma := by
    apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))
    intro X hX
    rw [partialGamma_add_one hs (mem_Ici.mp hX)]
    ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))

Tactic:
Tendsto.congr' this ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
refine :
  Tendsto (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 (s * s.GammaIntegral))
⊢ Tendsto (s + 1).partialGamma atTop (𝓝 (s * s.GammaIntegral))

Tactic:
refine Tendsto.congr' this ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this_1 : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
this : Tendsto (β := ℂ) (fun (X : ℝ) ↦ -(↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 0)
⊢ Tendsto (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 (s * s.GammaIntegral))

Tactic:
simpa using Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this

Premises used: Filter.Tendsto.const_mul, Complex.tendsto_partialGamma, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
suffices : Tendsto (β := ℂ) (fun (X : ℝ) ↦ -(↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 0)
⊢ Tendsto (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 (s * s.GammaIntegral))

Tactic:
suffices Tendsto (fun X => -X ^ s * (-X).exp : ℝ → ℂ) atTop (𝓝 0) by
    simpa using Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖) atTop (𝓝 0)
⊢ Tendsto (β := ℂ) (fun (X : ℝ) ↦ -(↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦
    e ^ s.re * rexp (-1 * e)

Tactic:
eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
refine :
  EqOn (β := ℝ) (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) (fun (e : ℝ) ↦ e ^ s.re * rexp (-1 * e)) (Ioi 0)
⊢ EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦
    e ^ s.re * rexp (-1 * e)

Tactic:
refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw : ‖-(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₁ : ‖(↑x : ℂ) ^ s‖ * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₂ : x ^ s.re * ‖(↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)
rw₃ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-1 * x)
rw₄ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-(1 * x))
rw₅ rw₆ : x ^ s.re * rexp (-x) = x ^ s.re * rexp (-x)
⊢ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖ = x ^ s.re * rexp (-1 * x)

Tactic:
rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]

Premises used: LT.lt.le, norm_mul, Complex.norm_of_nonneg, norm_neg, neg_mul, Complex.norm_cpow_eq_rpow_re_of_pos, Neg.neg, one_mul, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
⊢ EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦
    e ^ s.re * rexp (-1 * e)

Tactic:
have :
      (fun e : ℝ => ‖-(e : ℂ) ^ s * (-e).exp‖) =ᶠ[atTop] fun e : ℝ => e ^ s.re * (-1 * e).exp := by
    refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_
    intro x hx; dsimp only
    rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx,
      Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this_1 : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
this :
  EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦
    e ^ s.re * rexp (-1 * e)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖) atTop (𝓝 0)

Tactic:
(tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one)

Premises used: Iff.mpr, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero, zero_lt_one, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
hs : 0 < s.re
this_1 : (fun (X : ℝ) ↦ s * s.partialGamma X - (↑X : ℂ) ^ s * (↑(rexp (-X)) : ℂ)) =ᶠ[atTop] (s + 1).partialGamma
this :
  EventuallyEq (β := ℝ) atTop (fun (e : ℝ) ↦ ‖-(↑e : ℂ) ^ s * (↑(rexp (-e)) : ℂ)‖) fun (e : ℝ) ↦
    e ^ s.re * rexp (-1 * e)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖-(↑x : ℂ) ^ s * (↑(rexp (-x)) : ℂ)‖) atTop (𝓝 0)

Tactic:
exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one)

Premises used: Iff.mpr, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero, zero_lt_one, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : -s.re < (↑0 : ℝ)
⊢ 0 < s.re

Tactic:
simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1

Premises used: CharP.cast_eq_zero, Left.neg_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : 0 < s.re
zero : s.GammaIntegral = s * s.GammaIntegral / s
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s

Tactic:
rw [GammaIntegral_add_one h1]

Premises used: Complex.GammaIntegral_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : 0 < s.re
zero : s ≠ 0
⊢ s.GammaIntegral = s * s.GammaIntegral / s

Tactic:
rw [mul_comm, mul_div_cancel_right₀]

Premises used: mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : 0 < s.re
zero : ∀ (h1 : s = 0), s.re ≤ 0
⊢ s ≠ 0

Tactic:
contrapose! h1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : s = 0
zero : re 0 ≤ 0
⊢ s.re ≤ 0

Tactic:
rw [h1]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : s = 0
⊢ re 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [Nat.cast_add, Nat.cast_one] at h1

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
linarith : (↑n : ℝ) ≤ -(s.re + 1) → -s.re - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + ((↑n : ℝ) - -(s.re + 1)) = 0
⊢ -(s.re + 1) < (↑n : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)

Tactic:
have hh1 : -(s + 1).re < n := by
      rw [Nat.cast_add, Nat.cast_one] at h1
      rw [add_re, one_re]; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
n : ℕ
hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < (↑(n + 1) : ℝ)
hh1 : -(s + 1).re < (↑n : ℝ)
succ succ₁ : GammaAux n (s + 1) / s = GammaAux n (s + 1) / s
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

Tactic:
rw [← hn (s + 1) hh1]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
zero : ∀ (s : ℂ) (h1 : -s.re < (↑0 : ℝ)), GammaAux 0 s = GammaAux 0 (s + 1) / s
succ :
  ∀ (n : ℕ) (hn : ∀ (s : ℂ) (h1 : -s.re < (↑n : ℝ)), GammaAux n s = GammaAux n (s + 1) / s) (s : ℂ)
    (h1 : -s.re < (↑(n + 1) : ℝ)), GammaAux (n + 1) s = GammaAux (n + 1) (s + 1) / s
⊢ GammaAux n s = GammaAux n (s + 1) / s

Tactic:
induction n generalizing s with
  | zero =>
    simp only [CharP.cast_eq_zero, Left.neg_neg_iff] at h1
    dsimp only [GammaAux]; rw [GammaIntegral_add_one h1]
    rw [mul_comm, mul_div_cancel_right₀]; contrapose! h1; rw [h1]
    simp
  | succ n hn =>
    dsimp only [GammaAux]
    have hh1 : -(s + 1).re < n := by
      rw [Nat.cast_add, Nat.cast_one] at h1
      rw [add_re, one_re]; linarith
    rw [← hn (s + 1) hh1]

Premises used: CharP.cast_eq_zero, Left.neg_neg_iff, mul_div_cancel_right₀, mul_comm, _private.0.Complex.GammaAux
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
zero : ∀ (h1 : -s.re < (↑0 : ℝ)), GammaAux 0 s = GammaAux (HAdd.hAdd (α := ℕ) 0 1) s
succ : ∀ (n : ℕ) (h1 : -s.re < (↑(n + 1) : ℝ)), GammaAux (n + 1) s = GammaAux (n + 1 + 1) s
⊢ GammaAux n s = GammaAux (n + 1) s

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
h1 : 0 < s.re
zero : s ≠ 0
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s

Tactic:
rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀, Complex.GammaIntegral_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
h1 : 0 < re 0
⊢ LT.lt (α := ℝ) 0 0

Tactic:
rw [zero_re] at h1

Premises used: Complex.zero_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
h1 : LT.lt (α := ℝ) 0 0
⊢ False

Tactic:
h1.false

Premises used: LT.lt.false
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
h1 : LT.lt (α := ℝ) 0 0
⊢ False

Tactic:
exact h1.false

Premises used: LT.lt.false
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [Nat.cast_add, Nat.cast_one] at h1

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
linarith : (↑n : ℝ) ≤ -(s.re + 1) → -s.re - HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + ((↑n : ℝ) - -(s.re + 1)) = 0
⊢ -(s.re + 1) < (↑n : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)

Tactic:
have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
hh1 : -(s + 1).re < (↑n : ℝ)
rw rw₁ : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1 + 1) / (s + 1)
⊢ GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)

Tactic:
rw [GammaAux_recurrence1 (s + 1) n hh1]

Premises used: _private.0.Complex.GammaAux_recurrence1, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
⊢ GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)

Tactic:
have : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1) := by
      have hh1 : -(s + 1).re < n := by
        rw [Nat.cast_add, Nat.cast_one] at h1
        rw [add_re, one_re]; linarith
      rw [GammaAux_recurrence1 (s + 1) n hh1]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑(n + 1) : ℝ)
this : GammaAux n (s + 1 + 1) / (s + 1) = GammaAux n (s + 1)
succ succ₁ : GammaAux n (s + 1) / s = GammaAux n (s + 1) / s
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

Tactic:
rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
⊢ GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s

Tactic:
simp [Gamma]

Premises used: Complex.Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
succ : GammaAux (⌊1 - s.re⌋₊ + k + 1) s = GammaAux (⌊1 - s.re⌋₊ + k) s
⊢ GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s

Tactic:
rw [← hk, ← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + k + 1) s = GammaAux (⌊1 - s.re⌋₊ + k) s

Tactic:
(GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm

Premises used: HSub.hSub, _private.0.Complex.GammaAux_recurrence2, Complex.re, HAdd.hAdd, Nat.floor, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
succ : -s.re < (↑(⌊1 - s.re⌋₊ + k) : ℝ)
⊢ GammaAux (⌊1 - s.re⌋₊ + k + 1) s = GammaAux (⌊1 - s.re⌋₊ + k) s

Tactic:
refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm

Premises used: HSub.hSub, _private.0.Complex.GammaAux_recurrence2, Complex.re, HAdd.hAdd, Nat.floor, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
succ : -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)
⊢ -s.re < (↑(⌊1 - s.re⌋₊ + k) : ℝ)

Tactic:
rw [Nat.cast_add]

Premises used: Nat.cast_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ 1 - s.re - 1 < (↑⌊1 - s.re⌋₊ : ℝ)

Tactic:
have i0 := Nat.sub_one_lt_floor (1 - s.re)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : 1 - s.re - 1 < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ -s.re < (↑⌊1 - s.re⌋₊ : ℝ)

Tactic:
simp only [sub_sub_cancel_left] at i0

Premises used: sub_sub_cancel_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)

Tactic:
lt_add_of_lt_of_nonneg i0 ?_

Premises used: lt_add_of_lt_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
succ : LE.le (α := ℝ) 0 (↑k : ℝ)
⊢ -s.re < HAdd.hAdd (α := ℝ) (↑⌊1 - s.re⌋₊ : ℝ) (↑k : ℝ)

Tactic:
refine lt_add_of_lt_of_nonneg i0 ?_

Premises used: lt_add_of_lt_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
succ : 0 ≤ k
⊢ LE.le (α := ℝ) 0 (↑k : ℝ)

Tactic:
rw [← Nat.cast_zero, Nat.cast_le]

Premises used: Nat.cast_zero, Nat.cast_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ 0 ≤ k

Tactic:
Nat.zero_le k

Premises used: Nat.zero_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < (↑⌊1 - s.re⌋₊ : ℝ)
⊢ 0 ≤ k

Tactic:
exact Nat.zero_le k

Premises used: Nat.zero_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
k : ℕ
zero : GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s
succ : ∀ (k : ℕ) (hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s), GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s

Tactic:
induction k with
    | zero => simp [Gamma]
    | succ k hk =>
      rw [← hk, ← add_assoc]
      refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
      rw [Nat.cast_add]
      have i0 := Nat.sub_one_lt_floor (1 - s.re)
      simp only [sub_sub_cancel_left] at i0
      refine lt_add_of_lt_of_nonneg i0 ?_
      rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k

Premises used: Nat.zero_le, add_assoc, HSub.hSub, sub_sub_cancel_left, Complex.Gamma, _private.0.Complex.GammaAux_recurrence2, Complex.re, Nat.cast_add, HAdd.hAdd, Nat.floor, Nat.cast_zero, Nat.cast_le, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
⊢ ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s

Tactic:
have u : ∀ k : ℕ, GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s := fun k ↦ by
    induction k with
    | zero => simp [Gamma]
    | succ k hk =>
      rw [← hk, ← add_assoc]
      refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
      rw [Nat.cast_add]
      have i0 := Nat.sub_one_lt_floor (1 - s.re)
      simp only [sub_sub_cancel_left] at i0
      refine lt_add_of_lt_of_nonneg i0 ?_
      rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ Gamma s = GammaAux (⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)) s

Tactic:
(u <| n - ⌊1 - s.re⌋₊).symm

Premises used: HSub.hSub, Complex.re, Nat.floor, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)
⊢ Gamma s = GammaAux n s

Tactic:
convert! (u <| n - ⌊1 - s.re⌋₊).symm

Premises used: HSub.hSub, Complex.re, Nat.floor, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ⌊1 - s.re⌋₊ ≤ n
⊢ n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)

Tactic:
rw [Nat.add_sub_of_le]

Premises used: Nat.add_sub_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
pos : ∀ (h : 0 ≤ 1 - s.re), ⌊1 - s.re⌋₊ ≤ n
neg : ∀ (h : ¬0 ≤ 1 - s.re), ⌊1 - s.re⌋₊ ≤ n
⊢ ⌊1 - s.re⌋₊ ≤ n

Tactic:
by_cases h : 0 ≤ 1 - s.re

Premises used: Complex.re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : 0 ≤ 1 - s.re
pos : ⌊1 - s.re⌋₊ < n.succ
⊢ ⌊1 - s.re⌋₊ ≤ n

Tactic:
apply Nat.le_of_lt_succ

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : 0 ≤ 1 - s.re
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ 1 - s.re → -s.re - (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (1 - s.re)) = 0
⊢ 1 - s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
n : ℕ
h1 : -s.re < (↑n : ℝ)
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : 0 ≤ 1 - s.re
⊢ ⌊1 - s.re⌋₊ < n.succ

Tactic:
exact_mod_cast lt_of_le_of_lt (Nat.floor_le h) (by linarith : 1 - s.re < n + 1)

Premises used: lt_of_le_of_lt, Nat.floor_le