-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem differentiable_one_div_Gamma : Differentiable ℂ fun s : ℂ => (Gamma s)⁻¹ := fun s ↦ by
  rcases exists_nat_gt (-s.re) with ⟨n, hs⟩
  induction n generalizing s with
  | zero =>
    rw [Nat.cast_zero, neg_lt_zero] at hs
    suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
    rintro m rfl
    apply hs.not_le
    simp
  | succ n ihn =>
    rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
    specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
    exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))

Proof state:
case intro
s : ℂ
n : ℕ
hs : -s.re < ↑n
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Tactic:
induction n generalizing s with
| zero =>
  rw [Nat.cast_zero, neg_lt_zero] at hs
  suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
  rintro m rfl
  apply hs.not_le
  simp
| succ n ihn =>
  rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
  specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
  exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
    differentiableAt_id.add_const (1 : ℂ))

Result:
no goals

Proof state:
case intro.succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Tactic:
rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]

Result:
case intro.succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun x => x * (Gamma (x + 1))⁻¹) s

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

Tactic:
rintro m rfl

Result:
case intro.zero
m : ℕ
hs : 0 < (-↑m).re
⊢ False

Proof state:
case intro.zero
m : ℕ
hs : 0 < (-↑m).re
⊢ False

Tactic:
apply hs.not_le

Result:
case intro.zero
m : ℕ
hs : 0 < (-↑m).re
⊢ (-↑m).re ≤ 0

Proof state:
case intro.succ
n : ℕ
s : ℂ
hs : -s.re < ↑(n + 1)
ihn : DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) (s + 1)
⊢ DifferentiableAt ℂ (fun x => x * (Gamma (x + 1))⁻¹) s

Tactic:
exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
  differentiableAt_id.add_const (1 : ℂ))

Result:
no goals

Proof state:
s : ℂ
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Tactic:
rcases exists_nat_gt (-s.re) with ⟨n, hs⟩

Result:
case intro
s : ℂ
n : ℕ
hs : -s.re < ↑n
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Proof state:
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -(s + 1).re < ↑n

Tactic:
rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]

Result:
no goals

Proof state:
case intro.zero
s : ℂ
hs : 0 < s.re
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Tactic:
suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)

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

Proof state:
case intro.zero
s : ℂ
hs : -s.re < ↑0
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Tactic:
rw [Nat.cast_zero, neg_lt_zero] at hs

Result:
case intro.zero
s : ℂ
hs : 0 < s.re
⊢ DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s

Proof state:
case intro.zero
m : ℕ
hs : 0 < (-↑m).re
⊢ (-↑m).re ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case intro.succ
n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ DifferentiableAt ℂ (fun x => x * (Gamma (x + 1))⁻¹) s

Tactic:
specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])

Result:
case intro.succ
n : ℕ
s : ℂ
hs : -s.re < ↑(n + 1)
ihn : DifferentiableAt ℂ (fun s => (Gamma s)⁻¹) (s + 1)
⊢ DifferentiableAt ℂ (fun x => x * (Gamma (x + 1))⁻¹) s