awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
n : ℕ
s : ℂ
hsre : -(↑n : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ DifferentiableAt ℂ Gamma s
have zero : ∀ (s : ℂ) (hsre : -(↑0 : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), 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]
Cleared hypotheses: n, s, hsre, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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
⊢ DifferentiableAt ℂ Gamma s
have 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
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]
Cleared hypotheses: n, s, hsre, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
⊢ ∀ (m : ℕ), Ne (α := ℂ) 1 (-(↑m : ℂ))
have norm_cast : ∀ (m : ℕ), ¬(False ∧ m = 0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 1)
have rw : Tendsto (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (HAdd.hAdd (α := ℂ) 0 1)))
Tactic: rw [show 𝓝 (1 : ℂ) = 𝓝 (Gamma (0 + 1)) by simp only [zero_add, Complex.Gamma_one]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
⊢ Tendsto (fun (z : ℂ) ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (HAdd.hAdd (α := ℂ) 0 1)))
have refine : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ Gamma (x + 1)) 0
Tactic: refine tendsto_nhdsWithin_congr Gamma_add_one (continuousAt_iff_punctured_nhds.mp ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
n : ℕ
⊢ ¬ContinuousAt Gamma (-(↑n : ℂ))
have induction : ¬ContinuousAt Gamma (-(↑0 : ℂ))
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
n : ℕ
induction : ¬ContinuousAt Gamma (-(↑0 : ℂ))
⊢ ¬ContinuousAt Gamma (-(↑n : ℂ))
have succ : ∀ (n : ℕ), ¬ContinuousAt Gamma (-(↑n : ℂ)) → ¬ContinuousAt Gamma (-(↑(n + 1) : ℂ))
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
⊢ ¬ContinuousAt Gamma (-(↑0 : ℂ))
have rw : ¬ContinuousAt Gamma 0
Tactic: rw [Nat.cast_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
n : ℕ
ih : ¬ContinuousAt Gamma (-(↑n : ℂ))
⊢ ¬ContinuousAt Gamma (-(↑(n + 1) : ℂ))
have contrapose : ∀ (ih : ContinuousAt Gamma (-(↑(n + 1) : ℂ))), ContinuousAt Gamma (-(↑n : ℂ))
Tactic: contrapose ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
Goal:
n : ℕ
ih : ContinuousAt Gamma (-(↑(n + 1) : ℂ))
⊢ ContinuousAt Gamma (-(↑n : ℂ))
have ih₁ : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
Tactic: rw [Nat.cast_add, Nat.cast_one] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ ContinuousAt Gamma (-(↑n : ℂ))
have suffices : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s - 1 + 1)) (-(↑n : ℂ))
Tactic: suffices ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-n) by simpa using this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s - 1 + 1)) (-(↑n : ℂ))
have suffices : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1)
Tactic: suffices ContinuousAt (fun s ↦ Gamma (s + 1)) (-n - 1) from
      this.comp' (f := fun s ↦ s - 1) (continuous_sub_right 1).continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1)
have rw : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
Tactic: rw [← neg_add']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
Goal:
n : ℕ
ih : ContinuousAt Gamma (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ Gamma (s + 1)) (-HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have h0 : -HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: have h0 : -(n + 1) ≠ (0 : ℂ) := neg_ne_zero.mpr n.cast_add_one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : s ≠ 0
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
have pos : ∀ (h : ∃ (m : ℕ), s = -(↑m : ℂ)), deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
Tactic: by_cases! h : ∃ m : ℕ, s = -m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : s ≠ 0
pos : ∀ (h : ∃ (m : ℕ), s = -(↑m : ℂ)), deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
have neg : ∀ (h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
Tactic: by_cases! h : ∃ m : ℕ, s = -m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : s ≠ 0
h : ∃ (m : ℕ), s = -(↑m : ℂ)
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
have pos : ∀ (m : ℕ) (hs : Ne (α := ℂ) (-(↑m : ℂ)) 0),
  deriv Gamma (HAdd.hAdd (α := ℂ) (-(↑m : ℂ)) 1) = Gamma (-(↑m : ℂ)) + -(↑m : ℂ) * deriv Gamma (-(↑m : ℂ))
Tactic: obtain ⟨m, rfl⟩ := h
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
m : ℕ
hs : Ne (α := ℂ) (-(↑m : ℂ)) 0
⊢ deriv Gamma (HAdd.hAdd (α := ℂ) (-(↑m : ℂ)) 1) = Gamma (-(↑m : ℂ)) + -(↑m : ℂ) * deriv Gamma (-(↑m : ℂ))
have pos : 1 ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
m : ℕ
hs : Ne (α := ℂ) (-(↑m : ℂ)) 0
⊢ 1 ≤ m
have pos : ∀ (hs : Ne (α := ℂ) (↑m : ℂ) 0), 1 ≤ m
Tactic: rwa [neg_ne_zero, Nat.cast_ne_zero, ← Nat.one_le_iff_ne_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
m : ℕ
hs : Ne (α := ℂ) (-(↑m : ℂ)) 0
pos : ∀ (hs : Ne (α := ℂ) (↑m : ℂ) 0), 1 ≤ m
⊢ 1 ≤ m
have pos₁ : ∀ (hs : m ≠ 0), 1 ≤ m
Tactic: rwa [neg_ne_zero, Nat.cast_ne_zero, ← Nat.one_le_iff_ne_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
m : ℕ
hs : Ne (α := ℂ) (-(↑m : ℂ)) 0
pos : ∀ (hs : Ne (α := ℂ) (↑m : ℂ) 0), 1 ≤ m
pos₁ : ∀ (hs : m ≠ 0), 1 ≤ m
⊢ 1 ≤ m
have pos₂ : ∀ (hs : 1 ≤ m), 1 ≤ m
Tactic: rwa [neg_ne_zero, Nat.cast_ne_zero, ← Nat.one_le_iff_ne_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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 Gamma (s + 1) = Gamma s + s * deriv Gamma s
have rw : deriv (fun (x : ℂ) ↦ Gamma (x + 1)) s = Gamma s + s * deriv Gamma s
Tactic: rw [← deriv_comp_add_const]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
have neg : HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ HasDerivWithinAt (fun (s : ℂ) ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
have neg : HasDerivWithinAt (fun (x : ℂ) ↦ x * Gamma x) (Gamma s + s * deriv Gamma s) {0}ᶜ s
Tactic: refine HasDerivWithinAt.congr ?_ Gamma_add_one (Gamma_add_one s hs)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
⊢ DifferentiableAt ℝ Gamma s
have refine : ∀ (m : ℕ), (↑s : ℂ) ≠ -(↑m : ℂ)
Tactic: refine (Complex.differentiableAt_Gamma _ ?_).hasDerivAt.real_of_complex.differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℝ)
⊢ ∀ (m : ℕ), (↑s : ℂ) ≠ -(↑m : ℂ)
have simp_rw : ∀ (m : ℕ), ¬s = -(↑m : ℝ)
Tactic: simp_rw [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ∀ (m : ℕ), x ≠ -(↑m : ℝ)
have bound : 0 < x → ∀ (m : ℕ), x ≠ -(↑m : ℝ)
Tactic: bound [mem_Ioi.mp h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
⊢ digamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
have rw : logDeriv Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
Tactic: rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
rw : logDeriv Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
⊢ digamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
have rw₁ : deriv Gamma 1 / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
Tactic: rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
rw : logDeriv Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₁ : deriv Gamma 1 / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
⊢ digamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
have rw₂ : -(↑Real.eulerMascheroniConstant : ℂ) / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
Tactic: rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
rw : logDeriv Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₁ : deriv Gamma 1 / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
rw₂ : -(↑Real.eulerMascheroniConstant : ℂ) / Gamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
⊢ digamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
have rw₃ : -(↑Real.eulerMascheroniConstant : ℂ) / 1 = -(↑Real.eulerMascheroniConstant : ℂ)
Tactic: rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
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 : ℂ)
⊢ digamma 1 = -(↑Real.eulerMascheroniConstant : ℂ)
have rw₄ : -(↑Real.eulerMascheroniConstant : ℂ) = -(↑Real.eulerMascheroniConstant : ℂ)
Tactic: rw [digamma_def, logDeriv_apply, hasDerivAt_Gamma_one.deriv, Gamma_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
⊢ (1 / 2).digamma = -2 * log 2 - (↑Real.eulerMascheroniConstant : ℂ)
have rw : (↑Real.pi : ℂ) ^ (↑(1 / 2) : ℂ) * (-(2 * log 2) - (↑Real.eulerMascheroniConstant : ℂ)) / (↑Real.pi : ℂ) ^ (1 / 2) =
  -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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (hypothesis)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ (s + 1).digamma = s.digamma + s⁻¹
have hs0 : s ≠ 0
Tactic: have hs0 : s ≠ 0 := by simpa using hs 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₄ : (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₄ : (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₅ : Gamma s / (s * Gamma s) + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₄ : (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₅ : Gamma s / (s * Gamma s) + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₆ : s⁻¹ + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₄ : (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₅ : Gamma s / (s * Gamma s) + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₆ : s⁻¹ + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₇ : s⁻¹ + deriv Gamma s / Gamma s = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Digamma (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hs0 : s ≠ 0
rw : logDeriv Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₁ : deriv Gamma (s + 1) / Gamma (s + 1) = logDeriv Gamma s + s⁻¹
rw₂ : deriv Gamma (s + 1) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₃ : (Gamma s + s * deriv Gamma s) / Gamma (s + 1) = deriv Gamma s / Gamma s + s⁻¹
rw₄ : (Gamma s + s * deriv Gamma s) / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₅ : Gamma s / (s * Gamma s) + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₆ : s⁻¹ + s * deriv Gamma s / (s * Gamma s) = deriv Gamma s / Gamma s + s⁻¹
rw₇ : s⁻¹ + deriv Gamma s / Gamma s = deriv Gamma s / Gamma s + s⁻¹
⊢ (s + 1).digamma = s.digamma + s⁻¹
have rw₈ : deriv Gamma s / Gamma s + s⁻¹ = deriv Gamma s / Gamma s + s⁻¹
Tactic: rw [digamma_def, logDeriv_apply, logDeriv_apply, deriv_Gamma_add_one s hs0, Gamma_add_one s hs0,
    add_div, div_mul_cancel_right₀ (Gamma_ne_zero hs), mul_div_mul_left _ _ hs0, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
c T : ℝ
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2)‖ =
    rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2))
have rw : rexp (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I) * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2).re) =
  rexp
    (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) T 2 - 2 * ((↑b.re : ℂ) + (↑b.im : ℂ) * I).im * c * T -
        ((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) c 2))
Tactic: rw [Complex.norm_exp, neg_mul, neg_re, ← re_add_im b]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
c T : ℝ
⊢ rexp (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I) * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2).re) =
    rexp
      (-(((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) T 2 - 2 * ((↑b.re : ℂ) + (↑b.im : ℂ) * I).im * c * T -
          ((↑b.re : ℂ) + (↑b.im : ℂ) * I).re * HPow.hPow (β := ℕ) c 2))
have simp : rexp
    (-(b.re *
          ((T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) * (T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) -
            (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) * (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0))) -
        b.im *
          ((T + (c * 0 - HMul.hMul (α := ℝ) 0 1)) * (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) +
            (0 + (c * 1 + HMul.hMul (α := ℝ) 0 0)) * (T + (c * 0 - HMul.hMul (α := ℝ) 0 1))))) =
  rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))
Tactic: simp only [sq, re_add_im, mul_re, mul_im, add_re, add_im, ofReal_re, ofReal_im, I_re, I_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (hypothesis)
Goal:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2)‖ =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
have this : b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2 =
  b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 - HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)
Tactic: have :
    b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2 =
      b.re * (T - b.im * c / b.re) ^ 2 - c ^ 2 * (b.im ^ 2 / b.re + b.re) := by
    field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform (goal)
Goal:
b : ℂ
hb : b.re ≠ 0
c T : ℝ
this :
  b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2 =
    b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
      HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)
⊢ ‖cexp (-b * HPow.hPow (β := ℕ) ((↑T : ℂ) + (↑c : ℂ) * I) 2)‖ =
    rexp
      (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
          HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
have rw : rexp (-(b.re * HPow.hPow (β := ℕ) T 2 - 2 * b.im * c * T - b.re * HPow.hPow (β := ℕ) c 2)) =
  rexp
    (-(b.re * HPow.hPow (β := ℕ) (T - b.im * c / b.re) 2 -
        HPow.hPow (β := ℕ) c 2 * (HPow.hPow (β := ℕ) b.im 2 / b.re + b.re)))
Tactic: rw [norm_cexp_neg_mul_sq_add_mul_I, this]