awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * ((↑π : ℂ) / sin ((↑π : ℂ) * ((1 - s) / 2))) =
    (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * (↑π : ℂ) / sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
simp_rw : (↑π : ℂ) ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos ((↑π : ℂ) * s / 2) = (cos ((↑π : ℂ) * s / 2))⁻¹
⊢ (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * HPow.hPow (β := ℂ) (↑π : ℂ) 1 /
      sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2) =
    (cos ((↑π : ℂ) * s / 2))⁻¹

Tactic:
simp_rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero),
      Complex.sin_pi_div_two_sub]

Premises used: Iff.mpr, Complex.sin_pi_div_two_sub, Complex.ofReal_ne_zero, Complex.cpow_add, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
ring_nf : HPow.hPow (β := ℂ) (↑π : ℂ) 0 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
⊢ (↑π : ℂ) ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos ((↑π : ℂ) * s / 2) = (cos ((↑π : ℂ) * s / 2))⁻¹

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
rw : 1 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
rw₁ rw₂ : (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
⊢ HPow.hPow (β := ℂ) (↑π : ℂ) 0 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹

Tactic:
rw [cpow_zero, one_mul]

Premises used: Complex.cpow_zero, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
⊢ (s + 1).Gammaℝ ≠ 0

Tactic:
simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq,
      sub_eq_add_neg, ← neg_add]

Premises used: sub_eq_add_neg, eq_sub_iff_add_eq, not_exists, neg_add, Complex.Gammaℝ_eq_zero_iff, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
⊢ (s + 1).Gammaℝ ≠ 0

Tactic:
have : Gammaℝ (s + 1) ≠ 0 := by
    simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq,
      sub_eq_add_neg, ← neg_add]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
rw : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (s + 1).Gammaℝ)
rw₁ : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((s + 1).Gammaℝ * (1 - s).Gammaℝ)
rw₂ : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / (s + 1).Gammaℝ / (1 - s).Gammaℝ
rw₃ rw₄ : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ / (1 - s).Gammaℝ
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)

Tactic:
rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div,
      mul_div_cancel_right₀ _ this]

Premises used: Complex.Gammaℝ, HSub.hSub, add_comm, mul_div_cancel_right₀, HAdd.hAdd, mul_comm, div_div, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
rw :
  s.Gammaℝ * (s + 1).Gammaℝ / (cos ((↑π : ℂ) * s / 2))⁻¹ =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
rw₁ : s.Gammaℂ / (cos ((↑π : ℂ) * s / 2))⁻¹ = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
rw₂ rw₃ :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
⊢ s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹

Tactic:
rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]

Premises used: Complex.Gammaℂ_def, Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_add, Complex.Gammaℝ_mul_Gammaℝ_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
rw :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2)
rw₁ :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * (cos ((↑π : ℂ) * s / 2))⁻¹⁻¹ =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2)
rw₂ rw₃ :
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2)
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)

Tactic:
rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

Premises used: div_eq_mul_inv, Complex.Gammaℂ_def, inv_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
calc : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)
calc₁ :
  s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
calc₂ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)

Tactic:
calc Gammaℝ s / Gammaℝ (1 - s)
  _ = (Gammaℝ s * Gammaℝ (s + 1)) / (Gammaℝ (1 - s) * Gammaℝ (1 + s)) := by
    rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div,
      mul_div_cancel_right₀ _ this]
  _ = (2 * (2 * π) ^ (-s) * Gamma s) / ((cos (π * s / 2))⁻¹) := by
    rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
  _ = _ := by rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

Premises used: Real.pi, HMul.hMul, Complex.cos, Complex.Gammaℝ, HSub.hSub, Complex.Gamma, HDiv.hDiv, Complex.ofReal, Inv.inv, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
rw : ∀ (x : ℕ), ¬s = -HMul.hMul (α := ℂ) 2 (↑x : ℂ)
⊢ s.Gammaℝ ≠ 0

Tactic:
rw [Ne, Gammaℝ_eq_zero_iff, not_exists]

Premises used: not_exists, Complex.Gammaℝ_eq_zero_iff, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
n : ℕ
h : s = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
⊢ s ≠ -(↑(2 * n) : ℂ)

Tactic:
specialize hs (2 * n)

Premises used: HMul.hMul, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
n : ℕ
h : s = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
hs : s ≠ -(↑(2 * n) : ℂ)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ s.Gammaℝ ≠ 0

Tactic:
have h1 : Gammaℝ s ≠ 0 := by
    rw [Ne, Gammaℝ_eq_zero_iff, not_exists]
    intro n h
    specialize hs (2 * n)
    simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
⊢ s ≠ -(↑(2 * n + 1) : ℂ)

Tactic:
specialize hs (2 * n + 1)

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
hs : s ≠ -(↑(2 * n + 1) : ℂ)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h1 : s.Gammaℝ ≠ 0
⊢ ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)

Tactic:
have h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1) := by
    intro n h
    specialize hs (2 * n + 1)
    simp_all
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
rw : (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / (1 - s).Gammaℝ * s.Gammaℝ⁻¹
rw₁ : (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / (1 - s).Gammaℝ / s.Gammaℝ
rw₂ : (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / s.Gammaℝ / (1 - s).Gammaℝ
rw₃ : (1 - s).Gammaℝ⁻¹ = 1 / (1 - s).Gammaℝ
rw₄ rw₅ : (1 - s).Gammaℝ⁻¹ = (1 - s).Gammaℝ⁻¹
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹

Tactic:
rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]

Premises used: div_right_comm, div_eq_mul_inv, one_div, Complex.Gammaℝ_div_Gammaℝ_one_sub, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
pos : ∀ (h : s = 1), (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
neg : ∀ (h : ¬s = 1), (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹

Tactic:
by_cases h : s = 1
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
⊢ HSub.hSub (α := ℂ) 2 1 = 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
⊢ HAdd.hAdd (α := ℂ) 1 1 / 2 = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
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
pos₁₅ pos₁₆ : Eq (α := ℂ) 1 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹

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]

Premises used: Iff.mpr, div_mul_cancel₀, neg_div, Complex.cpow_neg_one, Complex.Gamma_one, inv_one, Complex.Gammaℝ, Complex.ofReal_ne_zero, Complex.Gammaℝ_one, Complex.sin_pi_div_two, inv_inv, mul_one, Real.pi_ne_zero, Complex.Gammaℂ_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : ¬s = 1
⊢ s - 1 ≠ 0

Tactic:
rw [← Ne, ← sub_ne_zero] at h

Premises used: sub_ne_zero, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
n : ℕ
zero : s - 1 ≠ -(↑0 : ℂ)
succ : ∀ (m : ℕ), s - 1 ≠ -(↑(m + 1) : ℂ)
⊢ s - 1 ≠ -(↑n : ℂ)

Tactic:
rcases n with - | m
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
zero : s - 1 ≠ -0
zero₁ zero₂ zero₃ zero₄ : s - 1 ≠ 0
⊢ s - 1 ≠ -(↑0 : ℂ)

Tactic:
rwa [Nat.cast_zero, neg_zero]

Premises used: Nat.cast_zero, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
succ : ¬s = HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1
⊢ s - 1 ≠ -(↑(m + 1) : ℂ)

Tactic:
rw [Ne, sub_eq_iff_eq_add]

Premises used: Ne, sub_eq_iff_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
⊢ s ≠ -(↑m : ℂ)

Tactic:
hs m
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
h₁ : HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1 = -(↑m : ℂ)
⊢ ¬s = HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1

Tactic:
convert! hs m using 2
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
h₁ : -HAdd.hAdd (α := ℂ) (↑m : ℂ) 1 + 1 = -(↑m : ℂ)
⊢ HAdd.hAdd (α := ℂ) (-(↑(m + 1) : ℂ)) 1 = -(↑m : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
m : ℕ
⊢ -HAdd.hAdd (α := ℂ) (↑m : ℂ) 1 + 1 = -(↑m : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
⊢ ∀ (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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
⊢ 2 - s = 1 - (s - 1)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
rw rw₁ : s.Gammaℂ = s.Gammaℂ
⊢ s.Gammaℂ = (s - 1 + 1).Gammaℂ

Tactic:
rw [sub_add_cancel]

Premises used: sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
⊢ s + 1 = s - 1 + 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
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 / (↑π : ℂ))⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹

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]

Premises used: mul_sub, sub_div, Complex.Gammaℂ_add_one, Complex.cos_sub_pi_div_two, Complex.Gammaℝ_add_two, mul_one, Complex.inv_Gammaℝ_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
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 / (↑π : ℂ))⁻¹)
⊢ (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]

Premises used: mul_inv, mul_div_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
neg :
  ∀ (A : ℂ),
    (s - 1).Gammaℂ * sin ((↑π : ℂ) * (s / 2)) * A =
      (s - 1).Gammaℂ * ((s - 1) / 2 / (↑π : ℂ)) * sin ((↑π : ℂ) * (s / 2)) * (A * ((s - 1) / 2 / (↑π : ℂ))⁻¹)
⊢ (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:
generalize (Gammaℝ (s - 1))⁻¹ = A

Premises used: Complex.Gammaℝ, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -(↑n : ℂ)
A : ℂ
⊢ (s - 1).Gammaℂ * sin ((↑π : ℂ) * (s / 2)) * A =
    (s - 1).Gammaℂ * ((s - 1) / 2 / (↑π : ℂ)) * sin ((↑π : ℂ) * (s / 2)) * (A * ((s - 1) / 2 / (↑π : ℂ))⁻¹)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
⊢ s.GammaIntegral = mellin (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) s

Tactic:
simp only [mellin, GammaIntegral, smul_eq_mul, mul_comm]

Premises used: Complex.GammaIntegral, mul_comm, smul_eq_mul, mellin
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
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
⊢ 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

Tactic:
rw [GammaIntegral_eq_mellin]

Premises used: Complex.GammaIntegral_eq_mellin
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (F := ℂ) (mellin fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ))
    (mellin (fun (t : ℝ) ↦ Real.log t • (↑(rexp (-t)) : ℂ)) s) s

Tactic:
(mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2

Premises used: lt_add_one, mellin_hasDerivAt_of_isBigO_rpow, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
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))
convert_4 : IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-0)
⊢ 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:
convert! (mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2

Premises used: lt_add_one, mellin_hasDerivAt_of_isBigO_rpow, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ MeasureTheory.LocallyIntegrableOn (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (Ioi 0) MeasureTheory.volume

Tactic:
(Continuous.continuousOn ?_).locallyIntegrableOn measurableSet_Ioi

Premises used: Continuous.continuousOn, measurableSet_Ioi, ContinuousOn.locallyIntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
convert_2 : Continuous (Y := ℂ) fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)
⊢ MeasureTheory.LocallyIntegrableOn (ε := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (Ioi 0) MeasureTheory.volume

Tactic:
refine (Continuous.continuousOn ?_).locallyIntegrableOn measurableSet_Ioi

Premises used: Continuous.continuousOn, measurableSet_Ioi, ContinuousOn.locallyIntegrableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)

Tactic:
continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, Real.continuous_exp, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ Continuous (Y := ℂ) fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)

Tactic:
exact continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, Real.continuous_exp, Complex.continuous_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
convert_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑(rexp (-x)) : ℂ)‖) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))

Tactic:
rw [← isBigO_norm_left]

Premises used: Asymptotics.isBigO_norm_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
convert_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑(rexp (-x)) : ℂ)‖) fun (x : ℝ) ↦ x ^ (-(s.re + 1))

Tactic:
simp_rw [norm_real, isBigO_norm_left]

Premises used: Complex.norm_real, Asymptotics.isBigO_norm_left
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ rexp (-x)) fun (x : ℝ) ↦ x ^ (-(s.re + 1))

Tactic:
simpa only [neg_one_mul] using (isLittleO_exp_neg_mul_rpow_atTop zero_lt_one _).isBigO

Premises used: neg_one_mul, isLittleO_exp_neg_mul_rpow_atTop, Asymptotics.IsLittleO.isBigO, zero_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
convert_4 : IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ 1
⊢ IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x (-0)

Tactic:
simp_rw [neg_zero, rpow_zero]

Premises used: Real.rpow_zero, neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ 1

Tactic:
isBigO_const_of_tendsto (?_ : Tendsto _ _ (𝓝 (1 : ℂ))) one_ne_zero

Premises used: Asymptotics.isBigO_const_of_tendsto, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
convert_4 : Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 1)
⊢ IsBigO (E := ℂ) (F := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) fun (x : ℝ) ↦ 1

Tactic:
refine isBigO_const_of_tendsto (?_ : Tendsto _ _ (𝓝 (1 : ℂ))) one_ne_zero

Premises used: Asymptotics.isBigO_const_of_tendsto, one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ 1 = (↑(rexp (-0)) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
convert_4 : Tendsto (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 (↑(rexp (-0)) : ℂ))
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 1)

Tactic:
rw [(by simp : (1 : ℂ) = Real.exp (-0))]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 (↑(rexp (-0)) : ℂ))

Tactic:
(continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)).continuousWithinAt

Premises used: ContinuousWithinAt, ContinuousNeg.continuous_neg, Continuous.comp, Real.exp, Real.continuous_exp, Complex.continuous_ofReal, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ)) (𝓝[>] 0) (𝓝 (↑(rexp (-0)) : ℂ))

Tactic:
exact (continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)).continuousWithinAt

Premises used: ContinuousNeg.continuous_neg, Continuous.comp, Real.continuous_exp, Complex.continuous_ofReal, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
this : ∀ (n : ℕ) (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
⊢ -(↑(⌊-s.re⌋₊ + 1) : ℝ) < s.re

Tactic:
grind [Nat.lt_floor_add_one (-s.re)]

Premises used: Complex.re, Neg.neg, Nat.lt_floor_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
suffices : ∀ (n : ℕ) (s : ℂ) (hsre : -(↑n : ℝ) < s.re) (hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)), DifferentiableAt ℂ Gamma s
⊢ 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
-- 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:
simpa using hsre