awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
pos : (HSub.hSub (α := ℂ) 2 1).Gammaℝ⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₁ : (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₂ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₃ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-HAdd.hAdd (α := ℂ) 1 1 / 2) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₄ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-(HAdd.hAdd (α := ℂ) 1 1 / 2)) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₅ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * Gamma 1)⁻¹
pos₆ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₇ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₈ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₉ : 1⁻¹ = 1 / (↑π : ℂ) * 1 * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₀ : 1⁻¹ = 1 / (↑π : ℂ) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁₁ : 1⁻¹ = 1 / (↑π : ℂ) * ((↑π : ℂ)⁻¹ * 1)⁻¹
Tactic: rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
    neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
    mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
    div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
pos : (HSub.hSub (α := ℂ) 2 1).Gammaℝ⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₁ : (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₂ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₃ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-HAdd.hAdd (α := ℂ) 1 1 / 2) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₄ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-(HAdd.hAdd (α := ℂ) 1 1 / 2)) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₅ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * Gamma 1)⁻¹
pos₆ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₇ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₈ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₉ : 1⁻¹ = 1 / (↑π : ℂ) * 1 * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₀ : 1⁻¹ = 1 / (↑π : ℂ) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₁ : 1⁻¹ = 1 / (↑π : ℂ) * ((↑π : ℂ)⁻¹ * 1)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁₂ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)⁻¹⁻¹
Tactic: rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
    neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
    mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
    div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
pos : (HSub.hSub (α := ℂ) 2 1).Gammaℝ⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₁ : (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₂ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₃ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-HAdd.hAdd (α := ℂ) 1 1 / 2) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₄ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-(HAdd.hAdd (α := ℂ) 1 1 / 2)) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₅ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * Gamma 1)⁻¹
pos₆ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₇ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₈ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₉ : 1⁻¹ = 1 / (↑π : ℂ) * 1 * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₀ : 1⁻¹ = 1 / (↑π : ℂ) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₁ : 1⁻¹ = 1 / (↑π : ℂ) * ((↑π : ℂ)⁻¹ * 1)⁻¹
pos₁₂ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)⁻¹⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁₃ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)
Tactic: rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
    neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
    mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
    div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
pos : (HSub.hSub (α := ℂ) 2 1).Gammaℝ⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₁ : (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₂ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₃ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-HAdd.hAdd (α := ℂ) 1 1 / 2) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₄ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-(HAdd.hAdd (α := ℂ) 1 1 / 2)) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₅ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * Gamma 1)⁻¹
pos₆ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₇ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₈ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₉ : 1⁻¹ = 1 / (↑π : ℂ) * 1 * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₀ : 1⁻¹ = 1 / (↑π : ℂ) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₁ : 1⁻¹ = 1 / (↑π : ℂ) * ((↑π : ℂ)⁻¹ * 1)⁻¹
pos₁₂ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)⁻¹⁻¹
pos₁₃ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁₄ : Eq (α := ℂ) 1⁻¹ 1
Tactic: rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
    neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
    mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
    div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
pos : (HSub.hSub (α := ℂ) 2 1).Gammaℝ⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₁ : (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₂ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 1).Gammaℝ⁻¹
pos₃ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-HAdd.hAdd (α := ℂ) 1 1 / 2) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₄ :
  1⁻¹ =
    Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
      ((↑π : ℂ) ^ (-(HAdd.hAdd (α := ℂ) 1 1 / 2)) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
pos₅ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * Gamma 1)⁻¹
pos₆ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₇ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₈ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₉ : 1⁻¹ = 1 / (↑π : ℂ) * 1 * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₀ : 1⁻¹ = 1 / (↑π : ℂ) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * 1)⁻¹
pos₁₁ : 1⁻¹ = 1 / (↑π : ℂ) * ((↑π : ℂ)⁻¹ * 1)⁻¹
pos₁₂ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)⁻¹⁻¹
pos₁₃ : 1⁻¹ = 1 / (↑π : ℂ) * (↑π : ℂ)
pos₁₄ : Eq (α := ℂ) 1⁻¹ 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁₅ : Eq (α := ℂ) 1 1
Tactic: rw [h, (by ring : 2 - 1 = (1 : ℂ)), Gammaℝ_one, Gammaℝ,
    neg_div, (by simp : (1 + 1) / 2 = (1 : ℂ)), Complex.Gamma_one, Gammaℂ_one,
    mul_one, Complex.sin_pi_div_two, mul_one, cpow_neg_one, mul_one, inv_inv,
    div_mul_cancel₀ _ (ofReal_ne_zero.mpr pi_ne_zero), inv_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : ¬s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have h₁ : s - 1 ≠ 0
Tactic: rw [← Ne, ← sub_ne_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
n : ℕ
⊢ s - 1 ≠ -(↑n : ℂ)
have zero : s - 1 ≠ -(↑0 : ℂ)
Tactic: rcases n with - | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
n : ℕ
zero : s - 1 ≠ -(↑0 : ℂ)
⊢ s - 1 ≠ -(↑n : ℂ)
have succ : ∀ (m : ℕ), s - 1 ≠ -(↑(m + 1) : ℂ)
Tactic: rcases n with - | m
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
⊢ s - 1 ≠ -(↑0 : ℂ)
have zero : s - 1 ≠ -0
Tactic: rwa [Nat.cast_zero, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
⊢ s - 1 ≠ -(↑(m + 1) : ℂ)
have succ : ¬s = HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1
Tactic: rw [Ne, sub_eq_iff_eq_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
⊢ ¬s = HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1
have h₁ : HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1 = -(↑m : ℂ)
Tactic: convert! hs m using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
⊢ HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1 = -(↑m : ℂ)
have h₁ : -HAdd.hAdd (α := ℂ) (↑m : ℂ) 1 + 1 = -(↑m : ℂ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
Tactic: have h' (n : ℕ) : s - 1 ≠ -n := by
    rcases n with - | m
    · rwa [Nat.cast_zero, neg_zero]
    · rw [Ne, sub_eq_iff_eq_add]
      convert! hs m using 2
      push_cast
      ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
⊢ s.Gammaℂ = (s - 1 + 1).Gammaℂ
have rw : s.Gammaℂ = s.Gammaℂ
Tactic: rw [sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have neg : (s - 1).Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s - 1).Gammaℝ⁻¹ =
  (s - 1).Gammaℂ * (s - 1) / 2 / (↑π : ℂ) * sin ((↑π : ℂ) * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / (↑π : ℂ))⁻¹
Tactic: rw [(by ring : 2 - s = 1 - (s - 1)), inv_Gammaℝ_one_sub h',
    (by rw [sub_add_cancel] : Gammaℂ s = Gammaℂ (s - 1 + 1)), Gammaℂ_add_one h,
    (by ring : s + 1 = (s - 1) + 2), Gammaℝ_add_two h, mul_sub, sub_div, mul_one,
      Complex.cos_sub_pi_div_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
⊢ (s - 1).Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * (s - 1) / 2 / (↑π : ℂ) * sin ((↑π : ℂ) * s / 2) * ((s - 1).Gammaℝ * (s - 1) / 2 / (↑π : ℂ))⁻¹
have neg : (s - 1).Gammaℂ * sin ((↑π : ℂ) * (s / 2)) * (s - 1).Gammaℝ⁻¹ =
  (s - 1).Gammaℂ * ((s - 1) / 2 / (↑π : ℂ)) * sin ((↑π : ℂ) * (s / 2)) * ((s - 1).Gammaℝ⁻¹ * ((s - 1) / 2 / (↑π : ℂ))⁻¹)
Tactic: simp_rw [mul_div_assoc, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
⊢ (s - 1).Gammaℂ * sin ((↑π : ℂ) * (s / 2)) * (s - 1).Gammaℝ⁻¹ =
    (s - 1).Gammaℂ * ((s - 1) / 2 / (↑π : ℂ)) * sin ((↑π : ℂ) * (s / 2)) *
      ((s - 1).Gammaℝ⁻¹ * ((s - 1) / 2 / (↑π : ℂ))⁻¹)
have neg : ∀ (A : ℂ),
  (s - 1).Gammaℂ * sin ((↑π : ℂ) * (s / 2)) * A =
    (s - 1).Gammaℂ * ((s - 1) / 2 / (↑π : ℂ)) * sin ((↑π : ℂ) * (s / 2)) * (A * ((s - 1) / 2 / (↑π : ℂ))⁻¹)
Tactic: generalize (Gammaℝ (s - 1))⁻¹ = A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt GammaIntegral
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * ((↑(Real.log t) : ℂ) * (↑(rexp (-t)) : ℂ)))
    s
have rw : HasDerivAt (F := ℂ) (mellin fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ))
  (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
    (MeasureTheory.Measure.restrict MeasureTheory.volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) * ((↑(Real.log t) : ℂ) * (↑(rexp (-t)) : ℂ)))
  s
Tactic: rw [GammaIntegral_eq_mellin]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (F := ℂ) (mellin fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * ((↑(Real.log t) : ℂ) * (↑(rexp (-t)) : ℂ)))
    s
have convert_2 : MeasureTheory.LocallyIntegrableOn (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (Ioi 0) MeasureTheory.volume
Tactic: convert! (mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
convert_2 : MeasureTheory.LocallyIntegrableOn (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (Ioi 0) MeasureTheory.volume
⊢ HasDerivAt (F := ℂ) (mellin fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * ((↑(Real.log t) : ℂ) * (↑(rexp (-t)) : ℂ)))
    s
have convert_3 : IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
Tactic: convert! (mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
convert_2 : MeasureTheory.LocallyIntegrableOn (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (Ioi 0) MeasureTheory.volume
convert_3 : IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
⊢ HasDerivAt (F := ℂ) (mellin fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ))
    (@MeasureTheory.integral _ _ _ _ MeasureTheory.MeasureSpace.toMeasurableSpace
      (MeasureTheory.Measure.restrict MeasureTheory.volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * ((↑(Real.log t) : ℂ) * (↑(rexp (-t)) : ℂ)))
    s
have convert_4 : IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-0)
Tactic: convert! (mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ MeasureTheory.LocallyIntegrableOn (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (Ioi 0) MeasureTheory.volume
have convert_2 : Continuous (Y := ℂ) fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)
Tactic: refine (Continuous.continuousOn ?_).locallyIntegrableOn measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
have convert_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑(rexp (-x)) : ℂ)‖) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
Tactic: rw [← isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑(rexp (-x)) : ℂ)‖) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
have convert_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
Tactic: simp_rw [norm_real, isBigO_norm_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-0)
have convert_4 : IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ 1
Tactic: simp_rw [neg_zero, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ 1
have convert_4 : Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 1)
Tactic: refine isBigO_const_of_tendsto (?_ : Tendsto _ _ (𝓝 (1 : ℂ))) one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 1)
have convert_4 : Tendsto (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 (↑(rexp (-0)) : ℂ))
Tactic: rw [(by simp : (1 : ℂ) = Real.exp (-0))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ DifferentiableAt ℂ Gamma s
have suffices : ∀ (n : ℕ) (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
Tactic: suffices ∀ (n : ℕ) (s : ℂ) (hsre : -n < s.re) (hs : ∀ m : ℕ, s ≠ -m), DifferentiableAt ℂ _ s from
    this (⌊-s.re⌋₊ + 1) s (by grind [Nat.lt_floor_add_one (-s.re)]) hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hsre : -(↑0 : ℝ) < s.re
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ DifferentiableAt ℂ Gamma s
have hsre₁ : 0 < s.re
Tactic: replace hsre : 0 < s.re := by simpa using hsre
Cleared hypotheses: hsre
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
Goal:
s_1 : ℂ
hs_1 : ∀ (m : ℕ), s_1 ≠ -(↑m : ℂ)
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
hsre : 0 < s.re
⊢ DifferentiableAt ℂ Gamma s
have this : IsOpen (X := ℂ) {s : ℂ | 0 < s.re}
Tactic: have : IsOpen {s : ℂ | 0 < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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}
⊢ DifferentiableAt ℂ Gamma s
have zero : Gamma =ᶠ[𝓝 s] GammaIntegral
Tactic: apply (hasDerivAt_GammaIntegral (by simpa using hsre)).differentiableAt.congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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}
⊢ Gamma =ᶠ[𝓝 s] GammaIntegral
have 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
Tactic: filter_upwards [this.mem_nhds hsre] with a using Gamma_eq_integral
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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
⊢ Gamma =ᶠ[𝓝 s] GammaIntegral
have h₁ : ∀ (a : ℂ), 0 < a.re → Gamma a = a.GammaIntegral
Tactic: filter_upwards [this.mem_nhds hsre] with a using Gamma_eq_integral
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
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 : ℂ)
⊢ DifferentiableAt ℂ Gamma s
have hsne : s ≠ 0
Tactic: have hsne : s ≠ 0 := by grind [hs 0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
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
have IH₁ : DifferentiableAt ℂ Gamma (s + 1)
Tactic: specialize IH (s + 1) (by grind [add_re, one_re]) (fun m ↦ by grind [hs (m + 1)])
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (hypothesis)
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 s
have this : DifferentiableAt ℂ (Gamma ∘ fun (s : ℂ) ↦ s + 1) s
Tactic: have := IH.comp s (show DifferentiableAt ℂ (fun s ↦ s + 1) s by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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
⊢ DifferentiableAt ℂ Gamma s
have succ : Gamma =ᶠ[𝓝 s] fun (x : ℂ) ↦ (Gamma ∘ fun (s : ℂ) ↦ s + 1) x / id x
Tactic: apply (this.fun_div differentiableAt_id hsne).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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
⊢ Gamma =ᶠ[𝓝 s] fun (x : ℂ) ↦ (Gamma ∘ fun (s : ℂ) ↦ s + 1) x / id x
have 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
Tactic: filter_upwards [isOpen_ne.mem_nhds hsne] using by grind [Gamma_add_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deriv (goal)
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
⊢ Gamma =ᶠ[𝓝 s] fun (x : ℂ) ↦ (Gamma ∘ fun (s : ℂ) ↦ s + 1) x / id x
have h₁ : ∀ (a : ℂ), a ≠ 0 → Gamma a = (Gamma ∘ fun (s : ℂ) ↦ s + 1) a / id a
Tactic: filter_upwards [isOpen_ne.mem_nhds hsne] using by grind [Gamma_add_one]