awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
have rw : s.Gammaℝ * (s + 1).Gammaℝ / (cos ((↑π : ℂ) * s / 2))⁻¹ =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
Tactic: rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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))⁻¹
⊢ s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
have rw₁ : s.Gammaℂ / (cos ((↑π : ℂ) * s / 2))⁻¹ = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
Tactic: rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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))⁻¹
⊢ s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
have rw₂ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹
Tactic: rw [Gammaℝ_one_sub_mul_Gammaℝ_one_add, Gammaℝ_mul_Gammaℝ_add_one, Gammaℂ_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have rw : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2)
Tactic: rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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)
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have rw₁ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * (cos ((↑π : ℂ) * s / 2))⁻¹⁻¹ =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2)
Tactic: rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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)
⊢ 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have rw₂ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2) =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * cos ((↑π : ℂ) * s / 2)
Tactic: rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have calc : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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ℝ)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have calc₁ : s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) =
  2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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))⁻¹
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have calc₂ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s / (cos ((↑π : ℂ) * s / 2))⁻¹ = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ s.Gammaℝ ≠ 0
have rw : ∀ (x : ℕ), ¬s = -HMul.hMul (α := ℂ) 2 (↑x : ℂ)
Tactic: rw [Ne, Gammaℝ_eq_zero_iff, not_exists]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
n : ℕ
h : s = -HMul.hMul (α := ℂ) 2 (↑n : ℂ)
⊢ False
have hs₁ : s ≠ -(↑(2 * n) : ℂ)
Tactic: specialize hs (2 * n)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have h1 : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
⊢ False
have hs₁ : s ≠ -(↑(2 * n + 1) : ℂ)
Tactic: specialize hs (2 * n + 1)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h1 : s.Gammaℝ ≠ 0
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have h2 : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have rw : (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / (1 - s).Gammaℝ * s.Gammaℝ⁻¹
Tactic: rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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ℝ⁻¹
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have rw₁ : (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / (1 - s).Gammaℝ / s.Gammaℝ
Tactic: rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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ℝ
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have rw₂ : (1 - s).Gammaℝ⁻¹ = s.Gammaℝ / s.Gammaℝ / (1 - s).Gammaℝ
Tactic: rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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ℝ
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have rw₃ : (1 - s).Gammaℝ⁻¹ = 1 / (1 - s).Gammaℝ
Tactic: rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
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ℝ
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2) * s.Gammaℝ⁻¹
have rw₄ : (1 - s).Gammaℝ⁻¹ = (1 - s).Gammaℝ⁻¹
Tactic: rw [← Gammaℝ_div_Gammaℝ_one_sub h2, ← div_eq_mul_inv, div_right_comm, div_self h1, one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos : ∀ (h : s = 1), (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
Tactic: by_cases h : s = 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
pos : ∀ (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ℝ⁻¹
have neg : ∀ (h : ¬s = 1), (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
Tactic: by_cases h : s = 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(↑n : ℂ)
h : s = 1
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos : (HSub.hSub (α := ℂ) 2 1).Gammaℝ⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 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]
-- 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ℝ⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁ : (Gammaℝ 1)⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 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]
-- 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ℝ⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₂ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HAdd.hAdd (α := ℂ) 1 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]
-- 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ℝ⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₃ : 1⁻¹ =
  Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * ((↑π : ℂ) ^ (-HAdd.hAdd (α := ℂ) 1 1 / 2) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
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))⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₄ : 1⁻¹ =
  Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) *
    ((↑π : ℂ) ^ (-(HAdd.hAdd (α := ℂ) 1 1 / 2)) * Gamma (HAdd.hAdd (α := ℂ) 1 1 / 2))⁻¹
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))⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₅ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-1) * Gamma 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)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₆ : 1⁻¹ = Gammaℂ 1 * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-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)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₇ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) * 1 / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-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)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₈ : 1⁻¹ = 1 / (↑π : ℂ) * sin ((↑π : ℂ) / 2) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-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)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₉ : 1⁻¹ = 1 / (↑π : ℂ) * 1 * (HPow.hPow (β := ℂ) (↑π : ℂ) (-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)⁻¹
⊢ (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * sin ((↑π : ℂ) * s / 2) * (s + 1).Gammaℝ⁻¹
have pos₁₀ : 1⁻¹ = 1 / (↑π : ℂ) * (HPow.hPow (β := ℂ) (↑π : ℂ) (-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]