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

Proof state:
case zero
s : ℂ
h1 : 0 < s.re
⊢ GammaAux 0 s = GammaAux 0 (s + 1) / s

Tactic:
dsimp only [GammaAux]

Result:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s

Proof state:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
⊢ -(s + 1).re < ↑n

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

Result:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s + 1).re < ↑n

Proof state:
case zero.hb
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0

Tactic:
contrapose! h1

Result:
case zero.hb
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0

Proof state:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s * s.GammaIntegral / s

Tactic:
rw [mul_comm, mul_div_cancel_right₀]

Result:
case zero.hb
s : ℂ
h1 : 0 < s.re
⊢ s ≠ 0

Proof state:
s : ℂ
n : ℕ
h1 : -s.re < ↑n
⊢ GammaAux n s = GammaAux n (s + 1) / s

Tactic:
induction' n with n hn generalizing s

Result:
case zero
s : ℂ
h1 : -s.re < ↑0
⊢ GammaAux 0 s = GammaAux 0 (s + 1) / s

case succ
n : ℕ
hn : ∀ (s : ℂ), -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

Proof state:
case zero.hb
s : ℂ
h1 : s = 0
⊢ re 0 ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s + 1).re < ↑n

Tactic:
rw [add_re, one_re]

Result:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n

Proof state:
case succ
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

Tactic:
have hh1 : -(s + 1).re < n := by
  rw [Nat.cast_add, Nat.cast_one] at h1
  rw [add_re, one_re]; linarith

Result:
case succ
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
hh1 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

Proof state:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = (s + 1).GammaIntegral / s

Tactic:
rw [GammaIntegral_add_one h1]

Result:
case zero
s : ℂ
h1 : 0 < s.re
⊢ s.GammaIntegral = s * s.GammaIntegral / s

Proof state:
case succ
n : ℕ
hn : ∀ (s : ℂ), -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

Tactic:
dsimp only [GammaAux]

Result:
case succ
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

Proof state:
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n

Tactic:
linarith

Result:
no goals

Proof state:
case succ
n : ℕ
hn : ∀ (s : ℂ), -s.re < ↑n → GammaAux n s = GammaAux n (s + 1) / s
s : ℂ
h1 : -s.re < ↑(n + 1)
hh1 : -(s + 1).re < ↑n
⊢ GammaAux n (s + 1) / s = GammaAux n (s + 1 + 1) / (s + 1) / s

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

Result:
no goals

Proof state:
case zero
s : ℂ
h1 : -s.re < ↑0
⊢ GammaAux 0 s = GammaAux 0 (s + 1) / s

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

Result:
case zero
s : ℂ
h1 : 0 < s.re
⊢ GammaAux 0 s = GammaAux 0 (s + 1) / s

Proof state:
case zero.hb
s : ℂ
h1 : s = 0
⊢ s.re ≤ 0

Tactic:
rw [h1]

Result:
case zero.hb
s : ℂ
h1 : s = 0
⊢ re 0 ≤ 0