-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < n) (h2 : ∀ m : ℕ, s ≠ -m) :
    DifferentiableAt ℂ (GammaAux n) s

Proof state:
case succ.refine_3
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ s ≠ 0

Tactic:
simpa using h2 0

Result:
no goals

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

Tactic:
have a : 1 - (s + 1).re < ↑n := by
  rw [Nat.cast_succ] at h1; rw [Complex.add_re, Complex.one_re]; linarith

Result:
case succ
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
⊢ DifferentiableAt ℂ (fun s => GammaAux n (s + 1) / s) s

Proof state:
case zero
s : ℂ
h1 : 1 - s.re < 0
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ 0 < s.re

Tactic:
linarith

Result:
no goals

Proof state:
case succ.refine_1
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => s) s

Tactic:
exact differentiableAt_id

Result:
no goals

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
this : s + 1 = -↑m
⊢ s = -↑(1 + m)

Tactic:
rw [← eq_sub_iff_add_eq] at this

Result:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
this : s = -↑m - 1
⊢ s = -↑(1 + m)

Proof state:
case zero
s : ℂ
h1 : 1 - s.re < ↑0
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ 0 < s.re

Tactic:
rw [Nat.cast_zero] at h1

Result:
case zero
s : ℂ
h1 : 1 - s.re < 0
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ 0 < s.re

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
⊢ ∀ (m : ℕ), s + 1 ≠ -↑m

Tactic:
intro m

Result:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
⊢ s + 1 ≠ -↑m

Proof state:
case zero
s : ℂ
h1 : 1 - s.re < ↑0
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ (GammaAux 0) s

Tactic:
refine (hasDerivAt_GammaIntegral ?_).differentiableAt

Result:
case zero
s : ℂ
h1 : 1 - s.re < ↑0
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ 0 < s.re

Proof state:
case succ
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
⊢ DifferentiableAt ℂ (fun s => GammaAux n (s + 1) / s) s

Tactic:
have b : ∀ m : ℕ, s + 1 ≠ -m := by
  intro m; have := h2 (1 + m)
  contrapose! this
  rw [← eq_sub_iff_add_eq] at this
  simpa using this

Result:
case succ
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => GammaAux n (s + 1) / s) s

Proof state:
s : ℂ
n : ℕ
h1 : 1 - s.re < ↑n
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ (GammaAux n) s

Tactic:
induction' n with n hn generalizing s

Result:
case zero
s : ℂ
h1 : 1 - s.re < ↑0
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ (GammaAux 0) s

case succ
n : ℕ
hn : ∀ (s : ℂ), 1 - s.re < ↑n → (∀ (m : ℕ), s ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) s
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
⊢ DifferentiableAt ℂ (GammaAux (n + 1)) s

Proof state:
case succ.refine_2
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => s) s

Tactic:
exact differentiableAt_id

Result:
no goals

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
this : s ≠ -↑(1 + m)
⊢ s + 1 ≠ -↑m

Tactic:
contrapose! this

Result:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
this : s + 1 = -↑m
⊢ s = -↑(1 + m)

Proof state:
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
m : ℕ
this : s = -↑m - 1
⊢ s = -↑(1 + m)

Tactic:
simpa using this

Result:
no goals

Proof state:
case succ
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => GammaAux n (s + 1) / s) s

Tactic:
refine DifferentiableAt.div (DifferentiableAt.comp _ (hn a b) ?_) ?_ ?_

Result:
case succ.refine_1
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => s + 1) s

case succ.refine_2
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => s) s

case succ.refine_3
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ s ≠ 0

Proof state:
case succ.refine_1
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => s + 1) s

Tactic:
rw [differentiableAt_add_const_iff (1 : ℂ)]

Result:
case succ.refine_1
n : ℕ
s : ℂ
h1 : 1 - s.re < ↑(n + 1)
h2 : ∀ (m : ℕ), s ≠ -↑m
hn : 1 - (s + 1).re < ↑n → (∀ (m : ℕ), s + 1 ≠ -↑m) → DifferentiableAt ℂ (GammaAux n) (s + 1)
a : 1 - (s + 1).re < ↑n
b : ∀ (m : ℕ), s + 1 ≠ -↑m
⊢ DifferentiableAt ℂ (fun s => s) s

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

Tactic:
dsimp only [GammaAux]

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

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

Tactic:
specialize hn (s + 1)

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