case inl
z : ℂ
n✝ n : ℕ
⊢ Complex.sin (↑π * 0) =
    ((↑π * 0 * ∏ j in Finset.range n, (1 - 0 ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * 0 * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))

case inr
z✝ : ℂ
n✝ : ℕ
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
z✝ : ℂ
n✝ : ℕ
z : ℂ
n : ℕ
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
rcases eq_or_ne z 0 with (rfl | hz)
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range Nat.zero, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.zero)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.zero))

case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range (Nat.succ n), (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr
z✝ : ℂ
n✝ : ℕ
z : ℂ
n : ℕ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
induction' n with n hn
no goals
case inl
z : ℂ
n✝ n : ℕ
⊢ Complex.sin (↑π * 0) =
    ((↑π * 0 * ∏ j in Finset.range n, (1 - 0 ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * 0 * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
simp
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = (↑π * z * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x)) / ↑(π / 2)
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range Nat.zero, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.zero)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.zero))
simp_rw [Nat.zero_eq, MulZeroClass.mul_zero, pow_zero, mul_one, Finset.prod_range_zero, mul_one,
  integral_one, sub_zero]
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = ↑π * z * (Complex.sin (↑π * z) / (2 * z)) / ↑(π / 2)
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = (↑π * z * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x)) / ↑(π / 2)
rw [integral_cos_mul_complex (mul_ne_zero two_ne_zero hz), Complex.ofReal_zero,
  MulZeroClass.mul_zero, Complex.sin_zero, zero_div, sub_zero,
  (by push_cast ; field_simp; ring : 2 * z * ↑(π / 2) = π * z)]
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) * (2 * z * ↑π) = ↑π * z * Complex.sin (↑π * z) * 2
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = ↑π * z * (Complex.sin (↑π * z) / (2 * z)) / ↑(π / 2)
field_simp [Complex.ofReal_ne_zero.mpr pi_pos.ne']
no goals
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) * (2 * z * ↑π) = ↑π * z * Complex.sin (↑π * z) * 2
ring
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * (↑π / 2) = ↑π * z
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑(π / 2) = ↑π * z
push_cast
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑π = ↑π * z * 2
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * (↑π / 2) = ↑π * z
field_simp
no goals
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑π = ↑π * z * 2
ring
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)) =
    (↑π * z * ((∏ x in Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range (Nat.succ n), (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
rw [hn, Finset.prod_range_succ]
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
hn :
  Complex.sin (↑π * z) =
    (↑π * z * A * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ (↑π * z * A * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)) =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
hn :
  Complex.sin (↑π * z) =
    ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)) =
    (↑π * z * ((∏ x in Finset.range n, (1 - z ^ 2 / (↑x + 1) ^ 2)) * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
set A := ∏ j in Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ ↑π * z * A * B / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)) =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
hn :
  Complex.sin (↑π * z) =
    (↑π * z * A * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ (↑π * z * A * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)) =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
⊢ ↑π * z * A * B / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)) =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
have : (∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n.succ)) = (2 * (n : ℝ) + 1) / (2 * n + 2) * C := by
  rw [integral_cos_pow_eq]
  dsimp only
  rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ,
    MulZeroClass.zero_mul, MulZeroClass.zero_mul, MulZeroClass.zero_mul, sub_zero, zero_div,
    zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_eq_ofNat]
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n))
rw [this]
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
change
  π * z * A * B / C =
    (π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
        ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) /
      ((2 * n + 1) / (2 * n + 2) * C : ℝ)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
have :
  (π * z * (A * ((1 : ℂ) - z ^ 2 / ((n : ℂ) + 1) ^ 2)) *
      ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
    π * z * A *
      (((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
        ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) := by
  nth_rw 2 [Nat.succ_eq_add_one]
  rw [Nat.cast_add_one]
  ring
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ↑π * z * A * B / ↑C =
    ↑π * z * A *
        ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) *
          ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ↑π * z * A * B / ↑C =
    (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
rw [this]
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ↑π * z * A * B / ↑C =
    ↑π * z * A *
        ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) *
          ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
suffices
  (((1 : ℂ) - z ^ 2 / (n.succ : ℂ) ^ 2) *
      ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n.succ)) =
    (2 * n + 1) / (2 * n + 2) * B by
  rw [this, Complex.ofReal_mul, Complex.ofReal_div]
  have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
  have : 2 * (n : ℂ) + 1 ≠ 0 := by
    convert (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
    simp
  have : 2 * (n : ℂ) + 2 ≠ 0 := by
    convert (Nat.cast_add_one_ne_zero (2 * n + 1) : (↑(2 * n + 1) + 1 : ℂ) ≠ 0) using 1
    push_cast ; ring
  field_simp; ring
case h.e'_2.h.e'_5.h.e'_6.h.e'_6.h.e'_5
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ↑(Nat.succ n) = ↑n + 1
case inr.succ
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
convert integral_cos_mul_cos_pow_even n hz
no goals
case h.e'_2.h.e'_5.h.e'_6.h.e'_6.h.e'_5
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
⊢ ↑(Nat.succ n) = ↑n + 1
rw [Nat.cast_succ]
no goals
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
⊢ 2 * Nat.succ n = 2 * n + 2
rw [Nat.succ_eq_add_one, mul_add, mul_one]
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ (1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
rw [integral_cos_pow_eq]
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ (1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ (1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
dsimp only
no goals
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
⊢ (1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ,
  MulZeroClass.zero_mul, MulZeroClass.zero_mul, MulZeroClass.zero_mul, sub_zero, zero_div,
  zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_eq_ofNat]
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
nth_rw 2 [Nat.succ_eq_add_one]
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
rw [Nat.cast_add_one]
no goals
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
⊢ (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
ring
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝¹ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝¹ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
⊢ ↑π * z * A * B / ↑C =
    ↑π * z * A *
        ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) *
          ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)
rw [this, Complex.ofReal_mul, Complex.ofReal_div]
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝² : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝¹ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝² : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
have : 2 * (n : ℂ) + 1 ≠ 0 := by
  convert (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
  simp
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝⁴ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝³ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝² :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝¹ : ↑C ≠ 0
this✝ : 2 * ↑n + 1 ≠ 0
this : 2 * ↑n + 2 ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
have : 2 * (n : ℂ) + 2 ≠ 0 := by
  convert (Nat.cast_add_one_ne_zero (2 * n + 1) : (↑(2 * n + 1) + 1 : ℂ) ≠ 0) using 1
  push_cast ; ring
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝⁴ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝³ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝² :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝¹ : ↑C ≠ 0
this✝ : 2 * ↑n + 1 ≠ 0
this : 2 * ↑n + 2 ≠ 0
⊢ ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (2 * n)) *
      ((2 * ↑n + 1) * ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))) =
    (↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((2 * ↑n + 1) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (2 * n)) *
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝⁴ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝³ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝² :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝¹ : ↑C ≠ 0
this✝ : 2 * ↑n + 1 ≠ 0
this : 2 * ↑n + 2 ≠ 0
⊢ ↑π * z * A * B / ↑C = ↑π * z * A * ((2 * ↑n + 1) / (2 * ↑n + 2) * B) / (↑(2 * ↑n + 1) / ↑(2 * ↑n + 2) * ↑C)
field_simp
no goals
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝⁴ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝³ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝² :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝¹ : ↑C ≠ 0
this✝ : 2 * ↑n + 1 ≠ 0
this : 2 * ↑n + 2 ≠ 0
⊢ ((↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (2 * n)) *
      ((2 * ↑n + 1) * ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))) =
    (↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ((2 * ↑n + 1) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (2 * n)) *
      ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n))
ring
case h.e'_2.h.e'_5
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝² : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ 2 * ↑n = ↑(2 * n)
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝² : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ 2 * ↑n + 1 ≠ 0
convert (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
no goals
case h.e'_2.h.e'_5
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝² : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝¹ :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this : ↑C ≠ 0
⊢ 2 * ↑n = ↑(2 * n)
simp
case h.e'_2
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 1) + 1
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 ≠ 0
convert (Nat.cast_add_one_ne_zero (2 * n + 1) : (↑(2 * n + 1) + 1 : ℂ) ≠ 0) using 1
case h.e'_2
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 1 + 1
case h.e'_2
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 1) + 1
push_cast
no goals
case h.e'_2
z✝ : ℂ
n✝ : ℕ
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * Nat.succ n = 2 * n + 2
this✝³ : (∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * Nat.succ n)) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝² :
  (↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    ↑π * z * A *
      ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n))
this✝¹ :
  ((1 - z ^ 2 / ↑(Nat.succ n) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * Nat.succ n)) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
this✝ : ↑C ≠ 0
this : 2 * ↑n + 1 ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 1 + 1
ring