-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = GammaAux n s

Proof state:
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ Gamma s = GammaAux n s

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

Result:
case h.e'_3.h.e'_1
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)

Proof state:
s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s

Tactic:
intro k

Result:
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
⊢ GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s

Proof state:
case zero
s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s

Tactic:
simp [Gamma]

Result:
no goals

Proof state:
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
⊢ GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s

Tactic:
induction' k with k hk

Result:
case zero
s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ GammaAux (⌊1 - s.re⌋₊ + 0) s = Gamma s

case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s

Proof state:
case succ
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:
rw [← Nat.cast_zero, Nat.cast_le]

Result:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ 0 ≤ k

Proof state:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ -s.re < ↑(⌊1 - s.re⌋₊ + k)

Tactic:
rw [Nat.cast_add]

Result:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ -s.re < ↑⌊1 - s.re⌋₊ + ↑k

Proof state:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ -s.re < ↑⌊1 - s.re⌋₊ + ↑k

Tactic:
refine lt_add_of_lt_of_nonneg i0 ?_

Result:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ 0 ≤ ↑k

Proof state:
case pos.a
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)

Result:
no goals

Proof state:
case succ
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:
refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm

Result:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ -s.re < ↑(⌊1 - s.re⌋₊ + k)

Proof state:
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 + 1

Tactic:
linarith

Result:
no goals

Proof state:
case pos
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

Tactic:
apply Nat.le_of_lt_succ

Result:
case pos.a
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

Proof state:
case h.e'_3.h.e'_1
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ n = ⌊1 - s.re⌋₊ + (n - ⌊1 - s.re⌋₊)

Tactic:
rw [Nat.add_sub_of_le]

Result:
case h.e'_3.h.e'_1
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ ⌊1 - s.re⌋₊ ≤ n

Proof state:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ GammaAux (⌊1 - s.re⌋₊ + (k + 1)) s = Gamma s

Tactic:
rw [← hk, ← add_assoc]

Result:
case succ
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

Proof state:
case succ
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

Result:
no goals

Proof state:
case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 0 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 1 - s.re ≤ 0

Tactic:
linarith

Result:
no goals

Proof state:
case succ
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⌋₊ + ↑k

Tactic:
simp only [sub_sub_cancel_left] at i0

Result:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
i0 : -s.re < ↑⌊1 - s.re⌋₊
⊢ -s.re < ↑⌊1 - s.re⌋₊ + ↑k

Proof state:
case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑n
k : ℕ
hk : GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ -s.re < ↑⌊1 - s.re⌋₊ + ↑k

Tactic:
have i0 := Nat.sub_one_lt_floor (1 - s.re)

Result:
case succ
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⌋₊ + ↑k

Proof state:
case h.e'_3.h.e'_1
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
⊢ ⌊1 - s.re⌋₊ ≤ n

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

Result:
case pos
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

case neg
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

Proof state:
case neg
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

Tactic:
rw [Nat.floor_of_nonpos]

Result:
case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 0 ≤ n

case neg
s : ℂ
n : ℕ
h1 : -s.re < ↑n
u : ∀ (k : ℕ), GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s
h : ¬0 ≤ 1 - s.re
⊢ 1 - s.re ≤ 0