awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
k : ℤ
hk : z = -(↑k : ℂ)
pos :
  ∀ (a : ℕ) (hk : z = -(↑(Int.ofNat a) : ℂ)),
    Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0
⊢ Gamma (-(↑k : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑k : ℂ))) = 0
have pos₁ : ∀ (a : ℕ) (hk : z = -(↑(Int.negSucc a) : ℂ)),
  Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.ofNat a) : ℂ)
⊢ Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0
have pos : Gamma (-(↑(↑a : ℤ) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(↑a : ℤ) : ℂ))) = 0
Tactic: rw [Int.ofNat_eq_natCast, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.ofNat a) : ℂ)
pos : Gamma (-(↑(↑a : ℤ) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(↑a : ℤ) : ℂ))) = 0
⊢ Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0
have pos₁ : Gamma (-(↑a : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑a : ℂ))) = 0
Tactic: rw [Int.ofNat_eq_natCast, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.ofNat a) : ℂ)
pos : Gamma (-(↑(↑a : ℤ) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(↑a : ℤ) : ℂ))) = 0
pos₁ : Gamma (-(↑a : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑a : ℂ))) = 0
⊢ Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0
have pos₂ : 0 * Gamma (HSub.hSub (α := ℂ) 1 (-(↑a : ℂ))) = 0
Tactic: rw [Int.ofNat_eq_natCast, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.ofNat a) : ℂ)
pos : Gamma (-(↑(↑a : ℤ) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(↑a : ℤ) : ℂ))) = 0
pos₁ : Gamma (-(↑a : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑a : ℂ))) = 0
pos₂ : 0 * Gamma (HSub.hSub (α := ℂ) 1 (-(↑a : ℂ))) = 0
⊢ Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0
have pos₃ : Eq (α := ℂ) 0 0
Tactic: rw [Int.ofNat_eq_natCast, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₂ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
pos₂ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₃ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
pos₂ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) = 0
pos₃ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₄ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
pos₂ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) = 0
pos₃ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) = 0
pos₄ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₅ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (-(↑a : ℂ)) = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
pos₂ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) = 0
pos₃ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) = 0
pos₄ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) = 0
pos₅ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (-(↑a : ℂ)) = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₆ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * 0 = 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
a : ℕ
hk : z = -(↑(Int.negSucc a) : ℂ)
pos : Gamma (- -(↑(a + 1) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (- -(↑(a + 1) : ℂ))) = 0
pos₁ : Gamma (↑(a + 1) : ℂ) * Gamma (HSub.hSub (α := ℂ) 1 (↑(a + 1) : ℂ)) = 0
pos₂ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑1 : ℂ)) = 0
pos₃ : Gamma (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) * Gamma (1 - HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) = 0
pos₄ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (1 - HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) = 0
pos₅ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * Gamma (-(↑a : ℂ)) = 0
pos₆ : Gamma (HAdd.hAdd (α := ℂ) 1 (↑a : ℂ)) * 0 = 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
have pos₇ : Eq (α := ℂ) 0 0
Tactic: rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
        Complex.Gamma_neg_nat_eq_zero, mul_zero]
-- 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 neg : Tendsto (fun (x : ℕ) ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
Tactic: refine tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
⊢ (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
have rw : (↑π : ℂ) / sin ((↑π : ℂ) * z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
⊢ Tendsto (fun (x : ℕ) ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
have this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
Tactic: have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ Tendsto (fun (x : ℕ) ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
have neg : Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) atTop (𝓝 1)
Tactic: convert!
    Tendsto.congr'
      ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => (GammaSeq_mul z hn).symm))
      (Tendsto.mul _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
neg : Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) atTop (𝓝 1)
⊢ Tendsto (fun (x : ℕ) ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
have neg₁ : Tendsto
  (fun (n : ℕ) ↦
    1 / (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
  atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
Tactic: convert!
    Tendsto.congr'
      ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => (GammaSeq_mul z hn).symm))
      (Tendsto.mul _ _)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) atTop (𝓝 1)
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) fun (n : ℕ) ↦
  (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
Tactic: convert! tendsto_natCast_div_add_atTop (1 - z) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) fun (n : ℕ) ↦
    (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
have h : ∀ (n : ℕ), (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) = (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
n : ℕ
⊢ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) = (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
have h : (↑n : ℂ) / ((↑n : ℂ) + (1 - z)) = (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
Tactic: rw [add_sub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ Tendsto
    (fun (n : ℕ) ↦
      1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
    atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
have this₁ : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
Tactic: have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
⊢ Tendsto
    (fun (n : ℕ) ↦
      1 /
        (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)))
    atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
have neg : Tendsto
  (fun (x : ℕ) ↦
    z * ∏ j ∈ Finset.range x, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
  atTop (𝓝 (sin ((↑π : ℂ) * z) / (↑π : ℂ)))
Tactic: convert! tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
⊢ Tendsto
    (fun (x : ℕ) ↦
      z * ∏ j ∈ Finset.range x, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (sin ((↑π : ℂ) * z) / (↑π : ℂ)))
have neg : Tendsto
  (fun (n : ℕ) ↦
    (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      (↑π : ℂ))
  atTop (𝓝 (sin ((↑π : ℂ) * z)))
Tactic: rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
⊢ Tendsto
    (fun (n : ℕ) ↦
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        (↑π : ℂ))
    atTop (𝓝 (sin ((↑π : ℂ) * z)))
have h : Eq (α := ℕ → ℂ)
  (fun (n : ℕ) ↦
    (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      (↑π : ℂ))
  fun (n : ℕ) ↦
  (↑π : ℂ) * z *
    ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
Tactic: convert! tendsto_euler_sin_prod z using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
⊢ Eq (α := ℕ → ℂ)
    (fun (n : ℕ) ↦
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        (↑π : ℂ))
    fun (n : ℕ) ↦
    (↑π : ℂ) * z *
      ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
have h : ∀ (n : ℕ),
  (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      (↑π : ℂ) =
    (↑π : ℂ) * z *
      ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
n : ℕ
⊢ (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      (↑π : ℂ) =
    (↑π : ℂ) * z *
      ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
have h : (↑π : ℂ) *
    (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) =
  (↑π : ℂ) * z *
    ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
Tactic: rw [mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
n : ℕ
h :
  (↑π : ℂ) *
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) =
    (↑π : ℂ) * z *
      ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
⊢ (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      (↑π : ℂ) =
    (↑π : ℂ) * z *
      ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
have h₁ : (↑π : ℂ) * z *
    ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2) =
  (↑π : ℂ) * z *
    ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)
Tactic: rw [mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
⊢ Gamma s ≠ 0
have pos : ∀ (h_im : s.im = 0), Gamma s ≠ 0
Tactic: by_cases h_im : s.im = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
pos : ∀ (h_im : s.im = 0), Gamma s ≠ 0
⊢ Gamma s ≠ 0
have neg : ∀ (h_im : ¬s.im = 0), Gamma s ≠ 0
Tactic: by_cases h_im : s.im = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
| s
have rw : (↑s.re : ℂ) + (↑s.im : ℂ) * I
Tactic: rw [← Complex.re_add_im s]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
⊢ s = (↑s.re : ℂ)
have conv_lhs : (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)
Tactic: conv_lhs => rw [← Complex.re_add_im s]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
⊢ (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)
have rw : (↑s.re : ℂ) + (↑0 : ℂ) * I = (↑s.re : ℂ)
Tactic: rw [h_im, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
rw : (↑s.re : ℂ) + (↑0 : ℂ) * I = (↑s.re : ℂ)
⊢ (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)
have rw₁ : (↑s.re : ℂ) + 0 * I = (↑s.re : ℂ)
Tactic: rw [h_im, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
rw : (↑s.re : ℂ) + (↑0 : ℂ) * I = (↑s.re : ℂ)
rw₁ : (↑s.re : ℂ) + 0 * I = (↑s.re : ℂ)
⊢ (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)
have rw₂ : (↑s.re : ℂ) + 0 = (↑s.re : ℂ)
Tactic: rw [h_im, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
rw : (↑s.re : ℂ) + (↑0 : ℂ) * I = (↑s.re : ℂ)
rw₁ : (↑s.re : ℂ) + 0 * I = (↑s.re : ℂ)
rw₂ : (↑s.re : ℂ) + 0 = (↑s.re : ℂ)
⊢ (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)
have rw₃ : (↑s.re : ℂ) = (↑s.re : ℂ)
Tactic: rw [h_im, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
⊢ Gamma s ≠ 0
have this : s = (↑s.re : ℂ)
Tactic: have : s = ↑s.re := by
      conv_lhs => rw [← Complex.re_add_im s]
      rw [h_im, ofReal_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
⊢ Gamma s ≠ 0
have pos : Real.Gamma s.re ≠ 0
Tactic: rw [this, Gamma_ofReal, ofReal_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
⊢ Real.Gamma s.re ≠ 0
have pos : ∀ (n : ℕ), s.re ≠ -(↑n : ℝ)
Tactic: refine Real.Gamma_ne_zero fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
⊢ s.re ≠ -(↑n : ℝ)
have hs₁ : s ≠ -(↑n : ℂ)
Tactic: specialize hs n
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
hs : s ≠ -(↑n : ℂ)
⊢ s.re ≠ -(↑n : ℝ)
have pos : ∀ (hs : s.re = -(↑n : ℝ)), s = -(↑n : ℂ)
Tactic: contrapose hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
hs : s.re = -(↑n : ℝ)
⊢ s = -(↑n : ℂ)
have pos : (↑s.re : ℂ) = -(↑n : ℂ)
Tactic: rwa [this, ← ofReal_natCast, ← ofReal_neg, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
hs : s.re = -(↑n : ℝ)
pos : (↑s.re : ℂ) = -(↑n : ℂ)
⊢ s = -(↑n : ℂ)
have pos₁ : (↑s.re : ℂ) = -(↑(↑n : ℝ) : ℂ)
Tactic: rwa [this, ← ofReal_natCast, ← ofReal_neg, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h_im : s.im = 0
this : s = (↑s.re : ℂ)
n : ℕ
hs : s.re = -(↑n : ℝ)
pos : (↑s.re : ℂ) = -(↑n : ℂ)
pos₁ : (↑s.re : ℂ) = -(↑(↑n : ℝ) : ℂ)
⊢ s = -(↑n : ℂ)
have pos₂ : (↑s.re : ℂ) = (↑(-(↑n : ℝ)) : ℂ)
Tactic: rwa [this, ← ofReal_natCast, ← ofReal_neg, ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
⊢ sin ((↑π : ℂ) * s) ≠ 0
have rw : ∀ (k : ℤ), (↑π : ℂ) * s ≠ (↑k : ℂ) * (↑π : ℂ)
Tactic: rw [Complex.sin_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
k : ℤ
⊢ (↑π : ℂ) * s ≠ (↑k : ℂ) * (↑π : ℂ)
have apply_fun : ((↑π : ℂ) * s).im ≠ ((↑k : ℂ) * (↑π : ℂ)).im
Tactic: apply_fun im
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
k : ℤ
⊢ ((↑π : ℂ) * s).im ≠ ((↑k : ℂ) * (↑π : ℂ)).im
have rw : π * s.im ≠ 0
Tactic: rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
⊢ Gamma s ≠ 0
have this : sin ((↑π : ℂ) * s) ≠ 0
Tactic: have : sin (↑π * s) ≠ 0 := by
      rw [Complex.sin_ne_zero_iff]
      intro k
      apply_fun im
      rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]
      exact mul_ne_zero Real.pi_pos.ne' h_im