awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
h₁ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (0 - 1 / 2))
h₂ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (-(1 / 2)))
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))
have h₃ : Ioi (-1) = Ioi (-(1 / 2) / (1 / 2))
Tactic: rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
h₁ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (0 - 1 / 2))
h₂ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (-(1 / 2)))
h₃ : Ioi (-1) = Ioi (-(1 / 2) / (1 / 2))
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))
have h₄ : Ioi (-1) = Ioi (-(1 / 2 / (1 / 2)))
Tactic: rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
h :
  Eq (α := Set ℝ) (Ioi (-1))
    (preimage (β := ℝ) (fun (x : ℝ) ↦ 1 / 2 * x) (preimage (β := ℝ) (fun (x : ℝ) ↦ x + 1 / 2) (Ioi 0)))
h₁ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (0 - 1 / 2))
h₂ : Eq (α := Set ℝ) (Ioi (-1)) ((fun (x : ℝ) ↦ 1 / 2 * x) ⁻¹' Ioi (-(1 / 2)))
h₃ : Ioi (-1) = Ioi (-(1 / 2) / (1 / 2))
h₄ : Ioi (-1) = Ioi (-(1 / 2 / (1 / 2)))
⊢ Eq (α := Set ℝ) (Ioi (-1)) (preimage (β := ℝ) ((fun (x : ℝ) ↦ x + 1 / 2) ∘ fun (x : ℝ) ↦ 1 / 2 * x) (Ioi 0))
have h₅ : Eq (α := Set ℝ) (Ioi (-1)) (Ioi (-1))
Tactic: rw [preimage_comp, preimage_add_const_Ioi, zero_sub,
        preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos, neg_div, div_self (@one_half_pos ℝ _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
⊢ Eq (α := ℝ → ℝ) (fun (s : ℝ) ↦ log (Γ (s / 2 + 1 / 2)))
    ((log ∘ Γ) ∘
      (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
            (AffineMap.const ℝ ℝ (1 / 2))) :
        (a : ℝ) → ℝ))
have h : ∀ (x : ℝ),
  log (Γ (x / 2 + 1 / 2)) =
    ((log ∘ Γ) ∘
        (⇑(HAdd.hAdd (α := ℝ →ᵃ[ℝ] ℝ) (LinearMap.toAffineMap (DistribSMul.toLinearMap ℝ ℝ (1 / 2)))
              (AffineMap.const ℝ ℝ (1 / 2))) :
          (a : ℝ) → ℝ))
      x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
⊢ log (Γ (x / 2 + 1 / 2)) = log (Γ ((1 / 2) • x + 1 / 2))
have h : log (Γ (x / 2 + 1 / 2)) = log (Γ (1 / 2 * x + 1 / 2))
Tactic: rw [smul_eq_mul, mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
h : log (Γ (x / 2 + 1 / 2)) = log (Γ (1 / 2 * x + 1 / 2))
⊢ log (Γ (x / 2 + 1 / 2)) = log (Γ ((1 / 2) • x + 1 / 2))
have h₁ : log (Γ (x / 2 + 1 / 2)) = log (Γ (x * (1 / 2) + 1 / 2))
Tactic: rw [smul_eq_mul, mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
x : ℝ
h : log (Γ (x / 2 + 1 / 2)) = log (Γ (1 / 2 * x + 1 / 2))
h₁ : log (Γ (x / 2 + 1 / 2)) = log (Γ (x * (1 / 2) + 1 / 2))
⊢ log (Γ (x / 2 + 1 / 2)) = log (Γ ((1 / 2) • x + 1 / 2))
have h₂ : log (Γ (x / 2 + 1 / 2)) = log (Γ (x / 2 + 1 / 2))
Tactic: rw [smul_eq_mul, mul_comm, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ s.doublingGamma = Γ s
have eq_Gamma_of_log_convex : ∀ {y : ℝ} (hy : 0 < y), 0 < y.doublingGamma
Tactic: refine
    eq_Gamma_of_log_convex doublingGamma_log_convex_Ioi
      (fun {y} hy => doublingGamma_add_one y hy.ne') (fun {y} hy => ?_) doublingGamma_one hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s : ℝ
hs : 0 < s
⊢ Γ s * Γ (s + 1 / 2) = Γ (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π
have rw : Γ s * Γ (s + 1 / 2) =
  Γ s * Γ (s + 1 / 2) * HPow.hPow (α := ℝ) 2 (2 * s - 1) / √π * (HPow.hPow (α := ℝ) 2 (2 * s - 1))⁻¹ * √π
Tactic: rw [← doublingGamma_eq_Gamma (mul_pos two_pos hs), doublingGamma,
    mul_div_cancel_left₀ _ (two_ne_zero' ℝ), (by abel : 1 - 2 * s = -(2 * s - 1)),
    rpow_neg zero_le_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : s ≠ 0
⊢ (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / (↑π : ℂ)
have rw : (↑π : ℂ) ^ (-(s / 2)) * (↑π : ℂ)⁻¹ * (s / 2 * Gamma (s / 2)) = (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * s / 2 / (↑π : ℂ)
Tactic: rw [Gammaℝ_def, Gammaℝ_def, neg_div, add_div, neg_add, div_self two_ne_zero,
    Gamma_add_one _ (div_ne_zero hs two_ne_zero),
    cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), cpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : s ≠ 0
⊢ (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / (↑π : ℂ)
have rw : 2 * ((2 * (↑π : ℂ)) ^ (-s) * (2 * (↑π : ℂ))⁻¹) * (s * Gamma s) = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s * s / 2 / (↑π : ℂ)
Tactic: rw [Gammaℂ_def, Gammaℂ_def, Gamma_add_one _ hs, neg_add,
    cpow_add _ _ (mul_ne_zero two_ne_zero (ofReal_ne_zero.mpr pi_ne_zero)), cpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ s.Gammaℝ ≠ 0
have ha : (↑π : ℂ) ^ (-s / 2) ≠ 0
Tactic: apply mul_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : 0 < s.re
ha : (↑π : ℂ) ^ (-s / 2) ≠ 0
⊢ s.Gammaℝ ≠ 0
have hb : Gamma (s / 2) ≠ 0
Tactic: apply mul_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0
have hb : 0 < (s / 2).re
Tactic: apply Gamma_ne_zero_of_re_pos
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ 0 < (s / 2).re
have hb : 0 < s.re / 2
Tactic: rw [div_ofNat_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
⊢ Gammaℝ 1 = 1
have rw : (↑π : ℂ) ^ (-1 / 2) * (↑π : ℂ) ^ (1 / 2) = 1
Tactic: rw [Gammaℝ_def, Complex.Gamma_one_half_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
⊢ Gammaℂ 1 = 1 / (↑π : ℂ)
have rw : 2 * (2 * (↑π : ℂ))⁻¹ * 1 = 1 / (↑π : ℂ)
Tactic: rw [Gammaℂ_def, cpow_neg_one, Complex.Gamma_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
| Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ s.Gammaℝ⁻¹
have h : ∀ (s : ℂ), s.Gammaℝ⁻¹
Tactic: enter [2, s]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
| s.Gammaℝ⁻¹
have h : ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
Tactic: rw [Gammaℝ, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
| Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ s.Gammaℝ⁻¹
have h : ∀ (s : ℂ), ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
Tactic: enter [2, s]; rw [Gammaℝ, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ s.Gammaℝ⁻¹
have conv : Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
Tactic: conv => enter [2, s]; rw [Gammaℝ, mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
have refine_1 : ∀ (s : ℂ), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)) s
Tactic: refine Differentiable.mul (fun s ↦ .inv ?_ (by simp [pi_ne_zero])) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
refine_1 : ∀ (s : ℂ), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)) s
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ ((↑π : ℂ) ^ (-s / 2))⁻¹ * (Gamma (s / 2))⁻¹
have refine_2 : Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ (Gamma (s / 2))⁻¹
Tactic: refine Differentiable.mul (fun s ↦ .inv ?_ (by simp [pi_ne_zero])) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)) s
have refine_1 : (↑π : ℂ) ≠ 0 ∨ -s / 2 ≠ 0
Tactic: refine ((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
have refine : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝[≠] 0)
Tactic: refine tendsto_self_mul_Gamma_nhds_zero.comp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
⊢ Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝[≠] 0)
have rw : Tendsto (fun (z : ℂ) ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, Membership.mem (γ := Set ℂ) {0}ᶜ (n / 2)
Tactic: rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
have h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
Tactic: have h : Tendsto (fun z : ℂ ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1) := by
    refine tendsto_self_mul_Gamma_nhds_zero.comp ?_
    rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]
    exact ⟨(tendsto_id.div_const _).mono_left nhdsWithin_le_nhds,
      eventually_of_mem self_mem_nhdsWithin fun x hx ↦ div_ne_zero hx two_ne_zero⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
have rw : Tendsto (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * (↑π : ℂ) ^ (-0 / 2)))
Tactic: rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * (↑π : ℂ) ^ (-0 / 2)))
have refine : ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) 0
Tactic: refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (Y := ℂ) (fun (s : ℂ) ↦ -s / 2) 0
have funProp : Ne (α := ℂ) 2 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
have h' : Tendsto (β := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
Tactic: have h' : Tendsto (fun s : ℂ ↦ 2 * (π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2) := by
    rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
    refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds
    exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
      (by fun_prop))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
h : Tendsto (β := ℂ) (fun (z : ℂ) ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (β := ℂ) (fun (s : ℂ) ↦ 2 * (↑π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
⊢ Tendsto (β := ℂ) (fun (s : ℂ) ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
have h₁ : ∀ (z : ℂ), z * z.Gammaℝ = 2 * (↑π : ℂ) ^ (-z / 2) * (z / 2 * Gamma (z / 2))
Tactic: convert! mul_one (2 : ℂ) ▸ (h'.mul h) using 2 with z
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
have rw : (↑π : ℂ) ^ (-s / 2 + -(s + 1) / 2) *
    (Gamma (2 * (s / 2)) * HPow.hPow (α := ℂ) 2 (1 - 2 * (s / 2)) * (↑π : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2) =
  HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
Tactic: rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s =
    2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s
have rw : 2 * HPow.hPow (α := ℂ) 2 (-s) * (↑π : ℂ) ^ (-1 / 2 - s + 1 / 2) * Gamma s =
  2 * (HPow.hPow (α := ℂ) 2 (-s) * (↑π : ℂ) ^ (-s)) * Gamma s
Tactic: rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ 2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
have rw : 2 * ((↑2 : ℂ) * (↑π : ℂ)) ^ (-s) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
Tactic: rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
rw : 2 * ((↑2 : ℂ) * (↑π : ℂ)) ^ (-s) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
⊢ 2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
have rw₁ : 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
Tactic: rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
have _ : (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
  (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))
Tactic: calc
  _ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
_ :
  (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
have _₁ : (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
  HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
Tactic: calc
  _ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
_ :
  (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))
_₁ :
  (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
have _₂ : HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s =
  2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s
Tactic: calc
  _ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
_ :
  (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))
_₁ :
  (↑π : ℂ) ^ (-s / 2) * (↑π : ℂ) ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s
_₂ :
  HPow.hPow (α := ℂ) 2 (1 - s) * ((↑π : ℂ) ^ (-1 / 2 - s) * (↑π : ℂ) ^ (1 / 2)) * Gamma s =
    2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s
⊢ (↑π : ℂ) ^ (-s / 2) * Gamma (s / 2) * ((↑π : ℂ) ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
have _₃ : 2 * ((↑2 : ℂ) ^ (-s) * (↑π : ℂ) ^ (-s)) * Gamma s = 2 * (2 * (↑π : ℂ)) ^ (-s) * Gamma s
Tactic: calc
  _ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
  _ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
    rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
      sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
    ring_nf
  _ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
    rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
      ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
    ring_nf
  _ = 2 * (2 * π) ^ (-s) * Gamma s := by
    rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) =
    (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * HPow.hPow (β := ℂ) (↑π : ℂ) 1 /
      sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2)
have rw : (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * ((↑π : ℂ) / sin ((↑π : ℂ) * ((1 - s) / 2))) =
  (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * (↑π : ℂ) / sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2)
Tactic: rw [Complex.Gamma_mul_Gamma_one_sub, cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ ((s - 1) / 2) * (↑π : ℂ) ^ ((-1 - s) / 2) * HPow.hPow (β := ℂ) (↑π : ℂ) 1 /
      sin ((↑π : ℂ) / 2 - (↑π : ℂ) * s / 2) =
    (cos ((↑π : ℂ) * s / 2))⁻¹
have simp_rw : (↑π : ℂ) ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos ((↑π : ℂ) * s / 2) = (cos ((↑π : ℂ) * s / 2))⁻¹
Tactic: simp_rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero),
      Complex.sin_pi_div_two_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ (↑π : ℂ) ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos ((↑π : ℂ) * s / 2) = (cos ((↑π : ℂ) * s / 2))⁻¹
have ring_nf : HPow.hPow (β := ℂ) (↑π : ℂ) 0 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
⊢ HPow.hPow (β := ℂ) (↑π : ℂ) 0 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
have rw : 1 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
Tactic: rw [cpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (goal)
Goal:
s : ℂ
rw : 1 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
⊢ HPow.hPow (β := ℂ) (↑π : ℂ) 0 * (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
have rw₁ : (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹ = (cos (s * (↑π : ℂ) * (1 / 2)))⁻¹
Tactic: rw [cpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Deligne (hypothesis)
Goal:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(HMul.hMul (α := ℂ) 2 (↑n : ℂ) + 1)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos ((↑π : ℂ) * s / 2)
have this : (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]
-- 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ℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)
have rw : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (s + 1).Gammaℝ)
Tactic: rw [add_comm 1 s, mul_comm (Gammaℝ (1 - s)) (Gammaℝ (s + 1)), ← div_div,
      mul_div_cancel_right₀ _ this]
-- 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ℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (s + 1).Gammaℝ)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)
have rw₁ : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((s + 1).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]
-- 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ℝ / (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ℝ)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)
have rw₂ : s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / (s + 1).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]
-- 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ℝ / (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ℝ
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)
have rw₃ : s.Gammaℝ / (1 - s).Gammaℝ = 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]