awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  (fun (n : ℕ) ↦ (∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1) : ℂ))
                      x =
                    s.GammaSeq x)
                x}
            x}
      a
⊢ (fun (n : ℕ) ↦ ∫ (x : ℝ) in 0..(↑n : ℝ), (↑((1 - x / (↑n : ℝ)) ^ n) : ℂ) * (↑x : ℂ) ^ (s - 1)) =ᶠ[atTop] s.GammaSeq
have h₁ : ∀ (a : ℕ), a ≠ 0 → ∫ (x : ℝ) in 0..(↑a : ℝ), (↑((1 - x / (↑a : ℝ)) ^ a) : ℂ) * (↑x : ℂ) ^ (s - 1) = s.GammaSeq a
Tactic: filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have succ : ∀ (hs : ⌊1 - re 0⌋₊ = m + 1), Tendsto (GammaSeq 0) atTop (𝓝 (Gamma 0))
Tactic: rcases eq_or_ne s 0 with rfl | hsne
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
succ : ∀ (hs : ⌊1 - re 0⌋₊ = m + 1), Tendsto (GammaSeq 0) atTop (𝓝 (Gamma 0))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have succ₁ : ∀ (hsne : s ≠ 0), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Tactic: rcases eq_or_ne s 0 with rfl | hsne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have succ : ⌊1 - (s + 1).re⌋₊ = m
Tactic: specialize IH (s + 1) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
succ : ⌊1 - (s + 1).re⌋₊ = m
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have succ₁ : ∀ (IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (Gamma (s + 1)))), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Tactic: specialize IH (s + 1) ?_
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
⊢ ⌊1 - (s + 1).re⌋₊ = m
have hs₁ : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
Tactic: rw [Nat.floor_eq_iff' (by lia)] at hs
Cleared hypotheses: hs, hsne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
⊢ ⌊1 - (s + 1).re⌋₊ = m
have this : s.re ≤ -(↑m : ℝ)
Tactic: have : s.re ≤ -m := by grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
s : ℂ
hs : (↑(m + 1) : ℝ) ≤ 1 - s.re ∧ 1 - s.re < HAdd.hAdd (α := ℝ) (↑(m + 1) : ℝ) 1
hsne : s ≠ 0
this : s.re ≤ -(↑m : ℝ)
⊢ ⌊1 - (s + 1).re⌋₊ = m
have succ : (↑m : ℝ) ≤ 1 - (s + 1).re ∧ 1 - (s + 1).re < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (Gamma (s + 1)))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have IH₁ : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
Tactic: rw [Gamma_add_one _ hsne] at IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
⊢ EventuallyEq (β := ℂ) atTop (fun (a : ℕ) ↦ (s + 1).GammaSeq a / s) fun (n : ℕ) ↦
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
have h : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ |
      Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℕ)
          {x : ℕ |
            (fun (x : ℕ) ↦
                (fun (a : ℕ) ↦ (s + 1).GammaSeq a / s) x =
                  (↑x : ℂ) / (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 + s) * s.GammaSeq x)
              x}
          x}
    a
Tactic: filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              (fun (x : ℕ) ↦
                  (fun (a : ℕ) ↦ (s + 1).GammaSeq a / s) x =
                    (↑x : ℂ) / (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 + s) * s.GammaSeq x)
                x}
            x}
      a
⊢ EventuallyEq (β := ℂ) atTop (fun (a : ℕ) ↦ (s + 1).GammaSeq a / s) fun (n : ℕ) ↦
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n
have h₁ : ∀ (a : ℕ), a ≠ 0 → (s + 1).GammaSeq a / s = (↑a : ℂ) / (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + s) * s.GammaSeq a
Tactic: filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have this : Tendsto (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n) atTop (𝓝 (s * Gamma s / s))
Tactic: have := (IH.div_const s).congr' <| by
      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this : Tendsto (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s) * s.GammaSeq n) atTop (𝓝 (s * Gamma s / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have this₁ : Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (s * Gamma s / s))
Tactic: simp only [mul_comm _ (s.GammaSeq _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this :
  Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (s * Gamma s / s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have rwa : ∀
  (this :
    Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (Gamma s * 1))),
  Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s)) atTop (𝓝 1)
Tactic: rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
s : ℂ
hs : ⌊1 - s.re⌋₊ = m + 1
hsne : s ≠ 0
IH : Tendsto (s + 1).GammaSeq atTop (𝓝 (s * Gamma s))
this : Tendsto (fun (n : ℕ) ↦ s.GammaSeq n * ((↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s))) atTop (𝓝 (Gamma s * 1))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + s)) atTop (𝓝 1)
have simp_rw : Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / ((↑n : ℂ) + (1 + s))) atTop (𝓝 1)
Tactic: simp_rw [add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
m : ℕ
⊢ ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have zero : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = 0 → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Tactic: induction m generalizing s with intro hs
  | zero => -- Base case: `0 < re s`, so Gamma is given by the integral formula
    rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
    apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm
  | succ m IH => -- Induction step: use recurrence formulae in `s` for Gamma and GammaSeq
    -- Silly case `s = 0`: both sides are zero
    rcases eq_or_ne s 0 with rfl | hsne
    · unfold GammaSeq
      simp [Finset.prod_range_succ']
    specialize IH (s + 1) ?_
    · rw [Nat.floor_eq_iff' (by lia)] at hs
      have : s.re ≤ -m := by grind
      rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]
      grind [add_re, one_re]
    rw [Gamma_add_one _ hsne] at IH
    have := (IH.div_const s).congr' <| by
      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
    simp only [mul_comm _ (s.GammaSeq _)] at this
    rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
    simp_rw [add_assoc]
    exact tendsto_natCast_div_add_atTop (1 + s)
Cleared hypotheses: s, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
m : ℕ
zero zero₁ : ∀ (s : ℂ) (hs : ⌊1 - s.re⌋₊ = 0), Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
⊢ ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have succ : ∀ (m : ℕ) (IH : ∀ (s : ℂ), ⌊1 - s.re⌋₊ = m → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))) (s : ℂ),
  ⌊1 - s.re⌋₊ = m + 1 → Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
Tactic: induction m generalizing s with intro hs
  | zero => -- Base case: `0 < re s`, so Gamma is given by the integral formula
    rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
    apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm
  | succ m IH => -- Induction step: use recurrence formulae in `s` for Gamma and GammaSeq
    -- Silly case `s = 0`: both sides are zero
    rcases eq_or_ne s 0 with rfl | hsne
    · unfold GammaSeq
      simp [Finset.prod_range_succ']
    specialize IH (s + 1) ?_
    · rw [Nat.floor_eq_iff' (by lia)] at hs
      have : s.re ≤ -m := by grind
      rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]
      grind [add_re, one_re]
    rw [Gamma_add_one _ hsne] at IH
    have := (IH.div_const s).congr' <| by
      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
    simp only [mul_comm _ (s.GammaSeq _)] at this
    rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
    simp_rw [add_assoc]
    exact tendsto_natCast_div_add_atTop (1 + s)
Cleared hypotheses: s, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
⊢ z.GammaSeq n * (1 - z).GammaSeq n =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
Tactic: have aux : ∀ a b c d : ℂ, a * b * (c * d) = a * c * (b * d) := by intros; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ z.GammaSeq n * (1 - z).GammaSeq n =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have rw : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
    HMul.hMul (α := ℂ) (∏ j ∈ Finset.range (n + 1), (z + (↑j : ℂ))) (∏ j ∈ Finset.range (n + 1), (1 - z + (↑j : ℂ))) =
  (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
    (1 /
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
Tactic: rw [GammaSeq, GammaSeq, div_mul_div_comm, aux, ← pow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
have rw : HPow.hPow (α := ℂ) (↑n : ℂ) (z + (1 - z)) = (↑n : ℂ)
Tactic: rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
rw : HPow.hPow (α := ℂ) (↑n : ℂ) (z + (1 - z)) = (↑n : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
have rw₁ : HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ)
Tactic: rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
rw : HPow.hPow (α := ℂ) (↑n : ℂ) (z + (1 - z)) = (↑n : ℂ)
rw₁ : HPow.hPow (α := ℂ) (β := ℂ) (↑n : ℂ) 1 = (↑n : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
have rw₂ : Eq (α := ℂ) (↑n : ℂ) (↑n : ℂ)
Tactic: rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      HMul.hMul (α := ℂ) (∏ j ∈ Finset.range (n + 1), (z + (↑j : ℂ))) (∏ j ∈ Finset.range (n + 1), (1 - z + (↑j : ℂ))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
Tactic: have : (n : ℂ) ^ z * (n : ℂ) ^ (1 - z) = n := by
    rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
⊢ HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      HMul.hMul (α := ℂ) (∏ j ∈ Finset.range (n + 1), (z + (↑j : ℂ))) (∏ j ∈ Finset.range (n + 1), (1 - z + (↑j : ℂ))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have rw : (↑n : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
    ((∏ x ∈ Finset.range n, (z + (↑(x + 1) : ℂ)) * (1 - z + (↑x : ℂ))) * (z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z))) =
  (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
    (1 /
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
Tactic: rw [this, Finset.prod_range_succ', Finset.prod_range_succ, aux, ← Finset.prod_mul_distrib,
    Nat.cast_zero, add_zero, add_comm (1 - z) n, ← add_sub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
j : ℕ
⊢ (z + (↑(j + 1) : ℂ)) * (1 - z + (↑j : ℂ)) =
    (↑(HPow.hPow (β := ℕ) (j + 1) 2) : ℂ) *
      (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
have push_cast : (z + HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) * (1 - z + (↑j : ℂ)) =
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2 *
    (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
j : ℕ
⊢ HAdd.hAdd (α := ℂ) (↑j : ℂ) 1 ≠ 0
have rw : j.succ ≠ 0
Tactic: rw [← Nat.cast_succ, Nat.cast_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
j : ℕ
⊢ (z + HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) * (1 - z + (↑j : ℂ)) =
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2 *
      (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
have this₁ : HAdd.hAdd (α := ℂ) (↑j : ℂ) 1 ≠ 0
Tactic: have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
⊢ (↑n : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      ((∏ x ∈ Finset.range n, (z + (↑(x + 1) : ℂ)) * (1 - z + (↑x : ℂ))) * (z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have this₁ : ∀ (j : ℕ),
  (z + (↑(j + 1) : ℂ)) * (1 - z + (↑j : ℂ)) =
    (↑(HPow.hPow (β := ℕ) (j + 1) 2) : ℂ) *
      (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
Tactic: have : ∀ j : ℕ, (z + ↑(j + 1)) * (↑1 - z + ↑j) =
      ((j + 1) ^ 2 :) * (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2) := by
    intro j
    push_cast
    have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j
    field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this_1 : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
this :
  ∀ (j : ℕ),
    (z + (↑(j + 1) : ℂ)) * (1 - z + (↑j : ℂ)) =
      (↑(HPow.hPow (β := ℕ) (j + 1) 2) : ℂ) *
        (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
⊢ (↑n : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      ((∏ x ∈ Finset.range n, (z + (↑(x + 1) : ℂ)) * (1 - z + (↑x : ℂ))) * (z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have simp_rw : (↑n : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
    ((∏ x ∈ Finset.range n,
        (↑(HPow.hPow (β := ℕ) (x + 1) 2) : ℂ) *
          (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1) 2)) *
      (z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z))) =
  (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
    (1 /
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
this_1 : HPow.hPow (α := ℂ) (↑n : ℂ) z * HPow.hPow (α := ℂ) (↑n : ℂ) (1 - z) = (↑n : ℂ)
this :
  ∀ (j : ℕ),
    (z + (↑(j + 1) : ℂ)) * (1 - z + (↑j : ℂ)) =
      (↑(HPow.hPow (β := ℕ) (j + 1) 2) : ℂ) *
        (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
⊢ (↑n : ℂ) * HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 /
      ((∏ x ∈ Finset.range n,
          (↑(HPow.hPow (β := ℕ) (x + 1) 2) : ℂ) *
            (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1) 2)) *
        (z * (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z))) =
    (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) *
      (1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
have hb : HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 ≠ 0
Tactic: rw [Finset.prod_mul_distrib, ← Nat.cast_prod, Finset.prod_pow,
    Finset.prod_range_add_one_eq_factorial, Nat.cast_pow,
    (by intros; ring : ∀ a b c d : ℂ, a * b * (c * d) = a * (d * (b * c))), ← div_div,
    mul_div_cancel_right₀, ← div_div, mul_comm z _, mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
have pi_ne : (↑π : ℂ) ≠ 0
Tactic: have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
have pos : ∀ (hs : sin ((↑π : ℂ) * z) = 0), Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
Tactic: by_cases hs : sin (↑π * z) = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
pos : ∀ (hs : sin ((↑π : ℂ) * z) = 0), Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
have neg : ∀ (hs : ¬sin ((↑π : ℂ) * z) = 0), Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
Tactic: by_cases hs : sin (↑π * z) = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : sin ((↑π : ℂ) * z) = 0
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
have pos : Gamma z * Gamma (1 - z) = 0
Tactic: rw [hs, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : sin ((↑π : ℂ) * z) = 0
⊢ Gamma z * Gamma (1 - z) = 0
have hs₁ : ∃ (k : ℤ), -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)
Tactic: rw [← neg_eq_zero, ← Complex.sin_neg, ← mul_neg, Complex.sin_eq_zero_iff, mul_comm] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ∃ (k : ℤ), -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)
⊢ Gamma z * Gamma (1 - z) = 0
have pos : ∀ (k : ℤ) (hk : -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)), Gamma z * Gamma (1 - z) = 0
Tactic: obtain ⟨k, hk⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
k : ℤ
hk : -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)
⊢ Gamma z * Gamma (1 - z) = 0
have hk₁ : z = -(↑k : ℂ)
Tactic: rw [mul_eq_mul_right_iff, eq_false (ofReal_ne_zero.mpr pi_pos.ne'), or_false,
      neg_eq_iff_eq_neg] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
k : ℤ
hk : z = -(↑k : ℂ)
⊢ Gamma z * Gamma (1 - z) = 0
have pos : Gamma (-(↑k : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑k : ℂ))) = 0
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
k : ℤ
hk : z = -(↑k : ℂ)
⊢ Gamma (-(↑k : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑k : ℂ))) = 0
have pos : ∀ (a : ℕ) (hk : z = -(↑(Int.ofNat a) : ℂ)),
  Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0
Tactic: cases k
Cleared hypotheses: k, hk