awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hsre : -(↑0 : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ 0 < s.re

Tactic:
replace hsre : 0 < s.re := by simpa using hsre
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsre : 0 < s.re
⊢ IsOpen (X := ℂ) {s : ℂ | 0 < s.re}

Tactic:
have : IsOpen {s : ℂ | 0 < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsre : 0 < s.re
this : IsOpen (X := ℂ) {s : ℂ | 0 < s.re}
⊢ 0 < s.re

Tactic:
simpa using hsre
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsre : 0 < s.re
this : IsOpen (X := ℂ) {s : ℂ | 0 < s.re}
zero : Gamma =ᶠ[𝓝 s] GammaIntegral
⊢ DifferentiableAt ℂ Gamma s

Tactic:
apply (hasDerivAt_GammaIntegral (by simpa using hsre)).differentiableAt.congr_of_eventuallyEq

Premises used: DifferentiableAt.congr_of_eventuallyEq, Complex.hasDerivAt_GammaIntegral, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsre : 0 < s.re
this : IsOpen (X := ℂ) {s : ℂ | 0 < s.re}
a : ℂ
⊢ 0 < a.re → Gamma a = a.GammaIntegral

Tactic:
Gamma_eq_integral

Premises used: Complex.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsre : 0 < s.re
this : IsOpen (X := ℂ) {s : ℂ | 0 < s.re}
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {s : ℂ | 0 < s.re} x →
          Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ Gamma x = x.GammaIntegral) x} x}
      a
h₁ h₂ : ∀ (a : ℂ), 0 < a.re → Gamma a = a.GammaIntegral
⊢ Gamma =ᶠ[𝓝 s] GammaIntegral

Tactic:
filter_upwards [this.mem_nhds hsre] with a using Gamma_eq_integral

Premises used: IsOpen.mem_nhds, Complex.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
IH : ∀ (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ s ≠ 0

Tactic:
grind [hs 0]

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
IH : ∀ (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ s ≠ 0

Tactic:
have hsne : s ≠ 0 := by grind [hs 0]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
IH : ∀ (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
⊢ -(↑n : ℝ) < (s + 1).re

Tactic:
grind [add_re, one_re]

Premises used: Complex.add_re, Complex.one_re
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
IH : ∀ (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
m : ℕ
⊢ s + 1 ≠ -(↑m : ℂ)

Tactic:
grind [hs (m + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
IH : ∀ (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
⊢ DifferentiableAt ℂ Gamma (s + 1)

Tactic:
specialize IH (s + 1) (by grind [add_re, one_re]) (fun m ↦ by grind [hs (m + 1)])

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
IH : DifferentiableAt ℂ Gamma (s + 1)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ s + 1) s

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
IH : DifferentiableAt ℂ Gamma (s + 1)
⊢ DifferentiableAt ℂ (Gamma ∘ fun (s : ℂ) ↦ s + 1) s

Tactic:
have := IH.comp s (show DifferentiableAt ℂ (fun s ↦ s + 1) s by fun_prop)
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
IH : DifferentiableAt ℂ Gamma (s + 1)
this : DifferentiableAt ℂ (Gamma ∘ fun (s : ℂ) ↦ s + 1) s
succ : Gamma =ᶠ[𝓝 s] fun (x : ℂ) ↦ (Gamma ∘ fun (s : ℂ) ↦ s + 1) x / id x
⊢ DifferentiableAt ℂ Gamma s

Tactic:
apply (this.fun_div differentiableAt_id hsne).congr_of_eventuallyEq

Premises used: DifferentiableAt.congr_of_eventuallyEq, DifferentiableAt.fun_div, differentiableAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
IH : DifferentiableAt ℂ Gamma (s + 1)
this : DifferentiableAt ℂ (Gamma ∘ fun (s : ℂ) ↦ s + 1) s
⊢ ∀ (a : ℂ), a ≠ 0 → Gamma a = (Gamma ∘ fun (s : ℂ) ↦ s + 1) a / id a

Tactic:
grind [Gamma_add_one]

Premises used: Complex.Gamma_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑(n + 1) : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsne : s ≠ 0
IH : DifferentiableAt ℂ Gamma (s + 1)
this : DifferentiableAt ℂ (Gamma ∘ fun (s : ℂ) ↦ s + 1) s
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {y : ℂ | y ≠ 0} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ | (fun (x : ℂ) ↦ Gamma x = (fun (x : ℂ) ↦ (Gamma ∘ fun (s : ℂ) ↦ s + 1) x / id x) x) x} x}
      a
h₁ : ∀ (a : ℂ), a ≠ 0 → Gamma a = (Gamma ∘ fun (s : ℂ) ↦ s + 1) a / id a
⊢ Gamma =ᶠ[𝓝 s] fun (x : ℂ) ↦ (Gamma ∘ fun (s : ℂ) ↦ s + 1) x / id x

Tactic:
filter_upwards [isOpen_ne.mem_nhds hsne] using by grind [Gamma_add_one]

Premises used: isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑n : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
zero : ∀ (s : ℂ) (hsre : -(↑0 : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
succ :
  ∀ (n : ℕ) (IH : ∀ (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s)
    (s : ℂ) (hsre : -(↑(n + 1) : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
⊢ DifferentiableAt ℂ Gamma s

Tactic:
induction n generalizing s with
  | zero =>
    -- Case `n = 0`: use relation to `gammaIntegral`
    replace hsre : 0 < s.re := by simpa using hsre
    have : IsOpen {s : ℂ | 0 < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
    apply (hasDerivAt_GammaIntegral (by simpa using hsre)).differentiableAt.congr_of_eventuallyEq
    filter_upwards [this.mem_nhds hsre] with a using Gamma_eq_integral
  | succ n IH =>
    -- Induction step: use recurrence relation
    have hsne : s ≠ 0 := by grind [hs 0]
    specialize IH (s + 1) (by grind [add_re, one_re]) (fun m ↦ by grind [hs (m + 1)])
    have := IH.comp s (show DifferentiableAt ℂ (fun s ↦ s + 1) s by fun_prop)
    apply (this.fun_div differentiableAt_id hsne).congr_of_eventuallyEq
    filter_upwards [isOpen_ne.mem_nhds hsne] using by grind [Gamma_add_one]

Premises used: DifferentiableAt.congr_of_eventuallyEq, Complex.hasDerivAt_GammaIntegral, HasDerivAt.differentiableAt, Complex.Gamma_eq_integral
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
norm_cast : ∀ (m : ℕ), ¬(False ∧ m = 0)
⊢ ∀ (m : ℕ), Ne (α := ℂ) 1 (-(↑m : ℂ))

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ∀ (m : ℕ), ¬(False ∧ m = 0)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ ContinuousAt Gamma s

Tactic:
(differentiableAt_Gamma s hs).continuousAt

Premises used: DifferentiableAt.continuousAt, Complex.differentiableAt_Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ContinuousAt Gamma 1

Tactic:
differentiableAt_Gamma_one.continuousAt

Premises used: DifferentiableAt.continuousAt, Complex.differentiableAt_Gamma_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ 𝓝 1 = 𝓝 (Gamma (HAdd.hAdd (α := ℂ) 0 1))

Tactic:
simp only [zero_add, Complex.Gamma_one]

Premises used: Complex.Gamma_one, zero_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
rw : Tendsto (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (HAdd.hAdd (α := ℂ) 0 1)))
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 1)

Tactic:
rw [show 𝓝 (1 : ℂ) = 𝓝 (Gamma (0 + 1)) by simp only [zero_add, Complex.Gamma_one]]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ Tendsto (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (HAdd.hAdd (α := ℂ) 0 1)))

Tactic:
tendsto_nhdsWithin_congr Gamma_add_one (continuousAt_iff_punctured_nhds.mp ?_)

Premises used: Complex.Gamma_add_one, continuousAt_iff_punctured_nhds, tendsto_nhdsWithin_congr, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
refine : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ Gamma (x + 1)) 0
⊢ Tendsto (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (HAdd.hAdd (α := ℂ) 0 1)))

Tactic:
refine tendsto_nhdsWithin_congr Gamma_add_one (continuousAt_iff_punctured_nhds.mp ?_)

Premises used: Complex.Gamma_add_one, continuousAt_iff_punctured_nhds, tendsto_nhdsWithin_congr, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ContinuousAt Gamma (HAdd.hAdd (α := ℂ) 0 1)

Tactic:
simp [continuousAt_Gamma_one]

Premises used: Complex.continuousAt_Gamma_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ Gamma (x + 1)) 0

Tactic:
exact ContinuousAt.comp' (by simp [continuousAt_Gamma_one]) (continuous_add_const 1).continuousAt

Premises used: ContinuousAt.comp', Continuous.continuousAt, continuous_add_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ Disjoint (𝓝 1) (𝓝 (0 * Gamma 0))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ¬DifferentiableAt ℂ Gamma 0

Tactic:
mt DifferentiableAt.continuousAt not_continuousAt_Gamma_zero

Premises used: DifferentiableAt.continuousAt, mt, Complex.not_continuousAt_Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
induction : ¬ContinuousAt Gamma (-(↑0 : ℂ))
succ : ∀ (n : ℕ), ¬ContinuousAt Gamma (-(↑n : ℂ)) → ¬ContinuousAt Gamma (-(↑(n + 1) : ℂ))
⊢ ¬ContinuousAt Gamma (-(↑n : ℂ))

Tactic:
induction n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
rw : ¬ContinuousAt Gamma 0
⊢ ¬ContinuousAt Gamma (-(↑0 : ℂ))

Tactic:
rw [Nat.cast_zero, neg_zero]

Premises used: Nat.cast_zero, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ¬ContinuousAt Gamma 0

Tactic:
not_continuousAt_Gamma_zero

Premises used: Complex.not_continuousAt_Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ¬ContinuousAt Gamma 0

Tactic:
exact not_continuousAt_Gamma_zero

Premises used: Complex.not_continuousAt_Gamma_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
⊢ ¬ContinuousAt Gamma (-(↑0 : ℂ))

Tactic:
case zero =>
    rw [Nat.cast_zero, neg_zero]
    exact not_continuousAt_Gamma_zero

Premises used: Complex.not_continuousAt_Gamma_zero, Nat.cast_zero, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ¬ContinuousAt Gamma (-(↑n : ℂ))
contrapose : ∀ (ih : ContinuousAt Gamma (-(↑(n + 1) : ℂ))), ContinuousAt Gamma (-(↑n : ℂ))
⊢ ¬ContinuousAt Gamma (-(↑(n + 1) : ℂ))

Tactic:
contrapose ih
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-(↑(n + 1) : ℂ))
⊢ ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

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

Premises used: Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
this : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s - 1 + 1)) (-(↑n : ℂ))
⊢ ContinuousAt Gamma (-(↑n : ℂ))

Tactic:
simpa using this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
suffices : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s - 1 + 1)) (-(↑n : ℂ))
⊢ ContinuousAt Gamma (-(↑n : ℂ))

Tactic:
suffices ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-n) by simpa using this
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
suffices : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s - 1 + 1)) (-(↑n : ℂ))

Tactic:
suffices ContinuousAt (fun s ↦ Gamma (s + 1)) (-n - 1) from
      this.comp' (f := fun s ↦ s - 1) (continuous_sub_right 1).continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
rw : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1)

Tactic:
rw [← neg_add']

Premises used: neg_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ -HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
have h0 : -(n + 1) ≠ (0 : ℂ) := neg_ne_zero.mpr n.cast_add_one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
h0 : -HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
((continuousAt_id.mul ih).continuousWithinAt.congr Gamma_add_one
      (Gamma_add_one (-(n + 1)) h0)).continuousAt (compl_singleton_mem_nhds h0)

Premises used: Complex.Gamma_add_one, ContinuousAt.continuousWithinAt, compl_singleton_mem_nhds, Nat.cast, HAdd.hAdd, ContinuousAt.mul, OfNat.ofNat, ContinuousWithinAt.continuousAt, continuousAt_id, Neg.neg, ContinuousWithinAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
h0 : -HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)

Tactic:
exact ((continuousAt_id.mul ih).continuousWithinAt.congr Gamma_add_one
      (Gamma_add_one (-(n + 1)) h0)).continuousAt (compl_singleton_mem_nhds h0)

Premises used: Complex.Gamma_add_one, ContinuousAt.continuousWithinAt, compl_singleton_mem_nhds, Nat.cast, HAdd.hAdd, ContinuousAt.mul, OfNat.ofNat, ContinuousWithinAt.continuousAt, continuousAt_id, Neg.neg, ContinuousWithinAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
n : ℕ
⊢ ¬DifferentiableAt ℂ Gamma (-(↑n : ℂ))

Tactic:
mt DifferentiableAt.continuousAt (not_continuousAt_Gamma_neg_nat n)

Premises used: DifferentiableAt.continuousAt, mt, Complex.not_continuousAt_Gamma_neg_nat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
pos : ∀ (h : ∃ (m : ℕ), s = -(↑m : ℂ)), deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
neg : ∀ (h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

Tactic:
by_cases! h : ∃ m : ℕ, s = -m
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∃ (m : ℕ), s = -(↑m : ℂ)
pos :
  ∀ (m : ℕ) (hs : Ne (α := ℂ) (-(↑m : ℂ)) 0),
    deriv Gamma (HAdd.hAdd (α := ℂ) (-(↑m : ℂ)) 1) = Gamma (-(↑m : ℂ)) + -(↑m : ℂ) * deriv Gamma (-(↑m : ℂ))
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

Tactic:
obtain ⟨m, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
m : ℕ
hs : Ne (α := ℂ) (-(↑m : ℂ)) 0
pos : 1 ≤ m
⊢ deriv Gamma (HAdd.hAdd (α := ℂ) (-(↑m : ℂ)) 1) = Gamma (-(↑m : ℂ)) + -(↑m : ℂ) * deriv Gamma (-(↑m : ℂ))

Tactic:
rw [← sub_neg_eq_add, ← neg_sub', ← Nat.cast_one, ← Nat.cast_sub,
      deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat m),
      deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat (m - 1)),
      Gamma_neg_nat_eq_zero, zero_add, mul_zero]

Premises used: Complex.Gamma_neg_nat_eq_zero, Complex.not_differentiableAt_Gamma_neg_nat, deriv_zero_of_not_differentiableAt, Nat.cast_sub, HSub.hSub, zero_add, MulZeroClass.mul_zero, neg_sub', OfNat.ofNat, Nat.cast_one, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
m : ℕ
hs : Ne (α := ℂ) (-(↑m : ℂ)) 0
pos : ∀ (hs : Ne (α := ℂ) (↑m : ℂ) 0), 1 ≤ m
pos₁ : ∀ (hs : m ≠ 0), 1 ≤ m
pos₂ pos₃ pos₄ pos₅ : ∀ (hs : 1 ≤ m), 1 ≤ m
⊢ 1 ≤ m

Tactic:
rwa [neg_ne_zero, Nat.cast_ne_zero, ← Nat.one_le_iff_ne_zero] at hs

Premises used: neg_ne_zero, Nat.one_le_iff_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
this : HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
rw : deriv (fun (x : ℂ) ↦ Gamma (x + 1)) s = Gamma s + s * deriv Gamma s
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

Tactic:
rw [← deriv_comp_add_const]

Premises used: deriv_comp_add_const
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
this : HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
⊢ deriv (fun (x : ℂ) ↦ Gamma (x + 1)) s = Gamma s + s * deriv Gamma s

Tactic:
(this.hasDerivAt (compl_singleton_mem_nhds hs)).deriv

Premises used: HasDerivAt.deriv, compl_singleton_mem_nhds, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
this : HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
⊢ deriv (fun (x : ℂ) ↦ Gamma (x + 1)) s = Gamma s + s * deriv Gamma s

Tactic:
exact (this.hasDerivAt (compl_singleton_mem_nhds hs)).deriv

Premises used: HasDerivAt.deriv, compl_singleton_mem_nhds, HasDerivWithinAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
neg : HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

Tactic:
suffices HasDerivWithinAt (fun s ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s by
      rw [← deriv_comp_add_const]
      exact (this.hasDerivAt (compl_singleton_mem_nhds hs)).deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s

Tactic:
HasDerivWithinAt.congr ?_ Gamma_add_one (Gamma_add_one s hs)

Premises used: Complex.Gamma_add_one, HasDerivWithinAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
neg : HasDerivWithinAt (fun (x : ℂ) ↦ x * Gamma x) (Gamma s + s * deriv Gamma s) {0}ᶜ s
⊢ HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s

Tactic:
refine HasDerivWithinAt.congr ?_ Gamma_add_one (Gamma_add_one s hs)

Premises used: Complex.Gamma_add_one, HasDerivWithinAt.congr
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ x * Gamma x) (Gamma s + s * deriv Gamma s) {0}ᶜ s

Tactic:
simpa using HasDerivWithinAt.mul (hasDerivWithinAt_id s {0}ᶜ)
      (differentiableAt_Gamma s h).hasDerivAt.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, DifferentiableAt.hasDerivAt, Compl.compl, HasDerivWithinAt.mul, Complex.differentiableAt_Gamma, hasDerivWithinAt_id, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
⊢ DifferentiableAt ℝ Gamma s

Tactic:
(Complex.differentiableAt_Gamma _ ?_).hasDerivAt.real_of_complex.differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, Real.Gamma, HasDerivAt.real_of_complex, Complex.differentiableAt_Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
refine : ∀ (m : ℕ), (↑s : ℂ) ≠ -(↑m : ℂ)
⊢ DifferentiableAt ℝ Gamma s

Tactic:
refine (Complex.differentiableAt_Gamma _ ?_).hasDerivAt.real_of_complex.differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.real_of_complex, Complex.differentiableAt_Gamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
simp_rw : ∀ (m : ℕ), ¬s = -(↑m : ℝ)
⊢ ∀ (m : ℕ), (↑s : ℂ) ≠ -(↑m : ℂ)

Tactic:
simp_rw [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]

Premises used: Complex.ofReal_neg, Ne, Complex.ofReal_natCast, Complex.ofReal_inj
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
⊢ ∀ (m : ℕ), ¬s = -(↑m : ℝ)

Tactic:
hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
⊢ ∀ (m : ℕ), ¬s = -(↑m : ℝ)

Tactic:
exact hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
bound bound₁ bound₂ bound₃ : 0 < x → ∀ (m : ℕ), x ≠ -(↑m : ℝ)
⊢ ∀ (m : ℕ), x ≠ -(↑m : ℝ)

Tactic:
bound [mem_Ioi.mp h]

Premises used: Set.mem_Ioi, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
⊢ digamma = logDeriv Gamma

Tactic:
rfl

Premises used: rfl, Complex.digamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
⊢ digamma 0 = 0

Tactic:
logDeriv_eq_zero_of_not_differentiableAt Gamma 0 not_differentiableAt_Gamma_zero

Premises used: Complex.Gamma, logDeriv_eq_zero_of_not_differentiableAt, Complex.not_differentiableAt_Gamma_zero, OfNat.ofNat, Complex.digamma
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
rw : logDeriv Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₁ : deriv Gamma 1 / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₂ : -(↑Real.eulerMascheroniConstant : ℂ) / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₃ : -(↑Real.eulerMascheroniConstant : ℂ) / 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₄ rw₅ : -(↑Real.eulerMascheroniConstant : ℂ) = -(↑Real.eulerMascheroniConstant : ℂ)
⊢ digamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)

Tactic:
rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]

Premises used: Complex.Gamma_one, HasDerivAt.deriv, logDeriv_apply, Complex.digamma_def, Complex.hasDerivAt_Gamma_one, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
rw :
  (↑Real.pi : ℂ) ^ (↑(1 / 2) : ℂ) * (-(2 * log 2) - (↑Real.eulerMascheroniConstant : ℂ)) / (↑Real.pi : ℂ) ^ (1 / 2) =
    -2 * log 2 - (↑Real.eulerMascheroniConstant : ℂ)
⊢ (1 / 2).digamma = -2 * log 2 - (↑Real.eulerMascheroniConstant : ℂ)

Tactic:
rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one_half.deriv, add_comm, Gamma_one_half_eq,
    neg_mul, ← mul_neg, neg_add', Real.sqrt_eq_rpow, ofReal_cpow Real.pi_nonneg]

Premises used: Real.pi_nonneg, Complex.ofReal_cpow, HasDerivAt.deriv, logDeriv_apply, add_comm, neg_add', Complex.digamma_def, Complex.hasDerivAt_Gamma_one_half, neg_mul, Complex.Gamma_one_half_eq, Real.sqrt_eq_rpow, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Digamma
Goal:
⊢ (↑Real.pi : ℂ) ^ (↑(1 / 2) : ℂ) * (-(2 * log 2) - (↑Real.eulerMascheroniConstant : ℂ)) / (↑Real.pi : ℂ) ^ (1 / 2) =
    -2 * log 2 - (↑Real.eulerMascheroniConstant : ℂ)

Tactic:
simp