awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℕ
rw : j.succ ≠ 0
⊢ HAdd.hAdd (α := ℂ) (↑j : ℂ) 1 ≠ 0

Tactic:
rw [← Nat.cast_succ, Nat.cast_ne_zero]

Premises used: Nat.cast_succ, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℕ
⊢ j.succ ≠ 0

Tactic:
Nat.succ_ne_zero j

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℕ
⊢ j.succ ≠ 0

Tactic:
exact Nat.succ_ne_zero j

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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

Tactic:
have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
j : ℕ
this : HAdd.hAdd (α := ℂ) (↑j : ℂ) 1 ≠ 0
⊢ (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:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)

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
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)
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)))
⊢ (↑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:
simp_rw [this]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)
a b c d : ℂ
⊢ a * b * (c * d) = a * (d * (b * c))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)
hb : HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 ≠ 0
⊢ (↑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:
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]

Premises used: Finset.prod_mul_distrib, Nat.cast_prod, Finset.prod_range_add_one_eq_factorial, mul_div_cancel_right₀, mul_one_div, mul_comm, Nat.cast_pow, div_div, Finset.prod_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 ! ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)
⊢ HPow.hPow (α := ℂ) (β := ℕ) (↑n ! : ℂ) 2 ≠ 0

Tactic:
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr <| by positivity)

Premises used: pow_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
⊢ (↑π : ℂ) ≠ 0

Tactic:
have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
pos : ∀ (hs : sin ((↑π : ℂ) * z) = 0), Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
neg : ∀ (hs : ¬sin ((↑π : ℂ) * z) = 0), Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)

Tactic:
by_cases hs : sin (↑π * z) = 0

Premises used: HMul.hMul, Complex.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : sin ((↑π : ℂ) * z) = 0
pos : Gamma z * Gamma (1 - z) = 0
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)

Tactic:
rw [hs, div_zero]

Premises used: div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : sin ((↑π : ℂ) * z) = 0
⊢ ∃ (k : ℤ), -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)

Tactic:
rw [← neg_eq_zero, ← Complex.sin_neg, ← mul_neg, Complex.sin_eq_zero_iff, mul_comm] at hs

Premises used: Complex.sin_eq_zero_iff, neg_eq_zero, mul_comm, Complex.sin_neg, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ∃ (k : ℤ), -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)
pos : ∀ (k : ℤ) (hk : -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)), Gamma z * Gamma (1 - z) = 0
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
obtain ⟨k, hk⟩ := hs
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
k : ℤ
hk : -z * (↑π : ℂ) = (↑k : ℂ) * (↑π : ℂ)
⊢ 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

Premises used: Iff.mpr, eq_false, Complex.ofReal_ne_zero, neg_eq_iff_eq_neg, Real.pi_pos, mul_eq_mul_right_iff, LT.lt.ne', or_false
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
k : ℤ
hk : z = -(↑k : ℂ)
pos : Gamma (-(↑k : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑k : ℂ))) = 0
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
rw [hk]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
pos₁ :
  ∀ (a : ℕ) (hk : z = -(↑(Int.negSucc a) : ℂ)),
    Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc a) : ℂ))) = 0
⊢ Gamma (-(↑k : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑k : ℂ))) = 0

Tactic:
cases k
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
pos₃ pos₄ : Eq (α := ℂ) 0 0
⊢ Gamma (-(↑(Int.ofNat a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.ofNat a) : ℂ))) = 0

Tactic:
rw [Int.ofNat_eq_natCast, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]

Premises used: Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, MulZeroClass.zero_mul, Int.ofNat_eq_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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
pos₇ pos₈ : Eq (α := ℂ) 0 0
⊢ Gamma (-(↑(Int.negSucc a) : ℂ)) * Gamma (HSub.hSub (α := ℂ) 1 (-(↑(Int.negSucc 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]

Premises used: Complex.Gamma_neg_nat_eq_zero, neg_neg, Int.cast_negSucc, sub_add_cancel_left, add_comm, MulZeroClass.mul_zero, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)

Tactic:
tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) ?_

Premises used: Complex.GammaSeq_tendsto_Gamma, HSub.hSub, Filter.Tendsto.mul, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
neg : Tendsto (fun (x : ℕ) ↦ z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 ((↑π : ℂ) / sin ((↑π : ℂ) * z)))
⊢ Gamma z * Gamma (1 - z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)

Tactic:
refine tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) ?_

Premises used: Complex.GammaSeq_tendsto_Gamma, HSub.hSub, Filter.Tendsto.mul, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
rw rw₁ : (↑π : ℂ) / sin ((↑π : ℂ) * z) = (↑π : ℂ) / sin ((↑π : ℂ) * z)
⊢ (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
⊢ (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))

Tactic:
have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ Tendsto (fun (n : ℕ) ↦ z.GammaSeq n * (1 - z).GammaSeq n) atTop (𝓝 (1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))))

Tactic:
Tendsto.congr'
      ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => (GammaSeq_mul z hn).symm))
      (Tendsto.mul _ _)

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.of_forall, Filter.Tendsto.mul, Filter.Eventually.mp, Complex.GammaSeq_mul, Filter.Tendsto.congr', OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)
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)))
⊢ Tendsto (fun (x : ℕ) ↦ z.GammaSeq x * (1 - z).GammaSeq x) 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 _ _)

Premises used: Filter.eventually_ne_atTop, Filter.Eventually.of_forall, Filter.Tendsto.mul, Filter.Eventually.mp, Complex.GammaSeq_mul, Filter.Tendsto.congr', OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / ((↑n : ℂ) + (1 - z))) atTop (𝓝 1)

Tactic:
tendsto_natCast_div_add_atTop (1 - z)

Premises used: HSub.hSub, tendsto_natCast_div_add_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) fun (n : ℕ) ↦
    (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) atTop (𝓝 1)

Tactic:
convert! tendsto_natCast_div_add_atTop (1 - z) using 1

Premises used: HSub.hSub, tendsto_natCast_div_add_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
h : ∀ (n : ℕ), (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) = (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z)) fun (n : ℕ) ↦
    (↑n : ℂ) / ((↑n : ℂ) + (1 - z))

Tactic:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
n : ℕ
h h₁ : (↑n : ℂ) / ((↑n : ℂ) + (1 - z)) = (↑n : ℂ) / ((↑n : ℂ) + (1 - z))
⊢ (↑n : ℂ) / (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 - z) = (↑n : ℂ) / ((↑n : ℂ) + (1 - z))

Tactic:
rw [add_sub_assoc]

Premises used: add_sub_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
⊢ (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))

Tactic:
have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → ℂ) (fun (x : ℕ) ↦ 1) fun (x : ℕ) ↦
      z * ∏ j ∈ Finset.range x, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))))

Tactic:
tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)

Premises used: tendsto_const_nhds, Filter.Tendsto.div, div_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
neg :
  Tendsto
    (fun (x : ℕ) ↦
      z * ∏ j ∈ Finset.range x, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2))
    atTop (𝓝 (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)))

Tactic:
convert! tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)

Premises used: tendsto_const_nhds, Filter.Tendsto.div, div_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
neg :
  Tendsto
    (fun (n : ℕ) ↦
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        (↑π : ℂ))
    atTop (𝓝 (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) / (↑π : ℂ)))

Tactic:
rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne]

Premises used: div_mul_cancel₀, Filter.tendsto_mul_iff_of_ne_zero, tendsto_const_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)))

Tactic:
tendsto_euler_sin_prod z

Premises used: Complex.tendsto_euler_sin_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
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)
⊢ Tendsto
    (fun (n : ℕ) ↦
      (z * ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) z 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        (↑π : ℂ))
    atTop (𝓝 (sin ((↑π : ℂ) * z)))

Tactic:
convert! tendsto_euler_sin_prod z using 1

Premises used: Complex.tendsto_euler_sin_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
z : ℂ
pi_ne : (↑π : ℂ) ≠ 0
hs : ¬sin ((↑π : ℂ) * z) = 0
this_1 : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 * ((↑π : ℂ) / sin ((↑π : ℂ) * z))
this : (↑π : ℂ) / sin ((↑π : ℂ) * z) = 1 / (sin ((↑π : ℂ) * z) / (↑π : ℂ))
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)
⊢ 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:
ext1 n
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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)
h₁ 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)

Tactic:
rw [mul_comm, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
pos : ∀ (h_im : s.im = 0), Gamma s ≠ 0
neg : ∀ (h_im : ¬s.im = 0), Gamma s ≠ 0
⊢ Gamma s ≠ 0

Tactic:
by_cases h_im : s.im = 0

Premises used: Complex.im
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
rw : (↑s.re : ℂ) + (↑s.im : ℂ) * I
| s

Tactic:
rw [← Complex.re_add_im s]

Premises used: Complex.re_add_im
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
conv_lhs : (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)
⊢ s = (↑s.re : ℂ)

Tactic:
conv_lhs => rw [← Complex.re_add_im s]

Premises used: Complex.re_add_im
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
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 : ℂ)
rw₃ rw₄ : (↑s.re : ℂ) = (↑s.re : ℂ)
⊢ (↑s.re : ℂ) + (↑s.im : ℂ) * I = (↑s.re : ℂ)

Tactic:
rw [h_im, ofReal_zero, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, Complex.ofReal_zero, add_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
⊢ 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
pos : Real.Gamma s.re ≠ 0
⊢ Gamma s ≠ 0

Tactic:
rw [this, Gamma_ofReal, ofReal_ne_zero]

Premises used: Complex.ofReal_ne_zero, Complex.Gamma_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : s.im = 0
this : s = (↑s.re : ℂ)
⊢ Real.Gamma s.re ≠ 0

Tactic:
Real.Gamma_ne_zero fun n => ?_

Premises used: Real.Gamma_ne_zero