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

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

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

Result:
no goals

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

Tactic:
dsimp only [GammaAux]

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

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

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

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

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

Tactic:
rw [add_re, one_re]

Result:
s : ℂ
n : ℕ
h1 : -s.re < ↑n + 1
⊢ -(s.re + 1) < ↑n

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

Tactic:
linarith

Result:
no goals

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

Tactic:
rw [GammaIntegral_add_one h1, mul_div_cancel_left₀]

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

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

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]

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

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

Tactic:
rcases n with - | n

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

case succ
s : ℂ
n : ℕ
h1 : -s.re < ↑(n + 1)
⊢ GammaAux (n + 1) s = GammaAux (n + 1 + 1) s

Proof state:
case zero.ha
h1 : 0 < re 0
⊢ False

Tactic:
rw [zero_re] at h1

Result:
case zero.ha
h1 : 0 < 0
⊢ False

Proof state:
case zero
s : ℂ
h1 : -s.re < ↑0
⊢ GammaAux 0 s = GammaAux (0 + 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 + 1) s

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

Tactic:
dsimp only [GammaAux]

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

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

Tactic:
rw [this]

Result:
no goals

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

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

Result:
s : ℂ
n : ℕ
h1 : -s.re < ↑n + 1
⊢ -(s + 1).re < ↑n

Proof state:
case zero.ha
h1 : 0 < 0
⊢ False

Tactic:
exact h1.false

Result:
no goals

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

Tactic:
rintro rfl

Result:
case zero.ha
h1 : 0 < re 0
⊢ False