-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_mul_Gamma_one_sub (z : ℂ) : Gamma z * Gamma (1 - z) = π / sin (π * z)

Proof state:
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

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

Result:
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Tendsto (fun x => z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))

Proof state:
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun x => z * ∏ j ∈ Finset.range x, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (↑π * z) / ↑π))

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

Result:
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n => (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) atTop (𝓝 (sin (↑π * z)))

Proof state:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = 0

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

Result:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : ∃ k, -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0

Proof state:
case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n => 1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))

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

Result:
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun x => z * ∏ j ∈ Finset.range x, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (↑π * z) / ↑π))

Proof state:
case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n => 1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))

Tactic:
have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by field_simp

Result:
case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n => 1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))

Proof state:
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
case pos.intro.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (-↑(Int.negSucc a✝)) * Gamma (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]

Result:
no goals

Proof state:
z : ℂ
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero

Result:
z : ℂ
pi_ne : ↑π ≠ 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Proof state:
z : ℂ
pi_ne : ↑π ≠ 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

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

Result:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Proof state:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
rw [hs, div_zero]

Result:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = 0

Proof state:
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma (-↑k) * Gamma (1 - -↑k) = 0

Tactic:
cases k

Result:
case pos.intro.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ Gamma (-↑(Int.ofNat a✝)) * Gamma (1 - -↑(Int.ofNat a✝)) = 0

case pos.intro.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (-↑(Int.negSucc a✝)) * Gamma (1 - -↑(Int.negSucc a✝)) = 0

Proof state:
case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Tendsto (fun x => z.GammaSeq x * (1 - z).GammaSeq x) atTop (𝓝 (↑π / sin (↑π * z)))

Tactic:
have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]

Result:
case neg
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)))

Proof state:
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)

Tactic:
field_simp

Result:
no goals

Proof state:
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0

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

Result:
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma z * Gamma (1 - z) = 0

Proof state:
case h.e'_3.h
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
n : ℕ
⊢ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π =
    ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)

Tactic:
rw [mul_comm, ← mul_assoc]

Result:
no goals

Proof state:
case pos.intro.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ Gamma (-↑(Int.ofNat a✝)) * Gamma (1 - -↑(Int.ofNat a✝)) = 0

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

Result:
no goals

Proof state:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : ∃ k, -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
obtain ⟨k, hk⟩ := hs

Result:
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0

Proof state:
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
rw [hk]

Result:
case pos.intro
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : z = -↑k
⊢ Gamma (-↑k) * Gamma (1 - -↑k) = 0

Proof state:
case neg
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)))

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

Result:
case neg.convert_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n => ↑n / (↑n + 1 - z)) atTop (𝓝 1)

case neg.convert_4
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n => 1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2))) atTop (𝓝 (↑π / sin (↑π * z)))

Proof state:
case h.e'_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ (fun n => (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) = fun n =>
    ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)

Tactic:
ext1 n

Result:
case h.e'_3.h
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
n : ℕ
⊢ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π =
    ↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)