[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
[PROOFSTEP]
have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
⊢ HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
[PROOFSTEP]
have b : HasDerivAt (fun y : ℂ => Complex.sin (y * (2 * z))) _ x :=
  HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_sin (x * (2 * z))) a
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x
⊢ HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
[PROOFSTEP]
have c := b.comp_ofReal.div_const (2 * z)
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun x => Complex.sin (↑x * (2 * z)) / (2 * z)) (Complex.cos (↑x * (2 * z)) * (2 * z) / (2 * z)) x
⊢ HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
[PROOFSTEP]
field_simp at c
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun x => Complex.sin (↑x * (2 * z)) / (2 * z)) (Complex.cos (↑x * (2 * z))) x
⊢ HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
[PROOFSTEP]
simp only [fun y => mul_comm y (2 * z)] at c
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.sin (y * (2 * z))) (Complex.cos (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun x => Complex.sin (2 * z * ↑x) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
⊢ HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
[PROOFSTEP]
exact c
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
[PROOFSTEP]
have a : HasDerivAt (fun y : ℂ => y * (2 * z)) _ x := hasDerivAt_mul_const _
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
⊢ HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
[PROOFSTEP]
have b : HasDerivAt (fun y : ℂ => Complex.cos (y * (2 * z))) _ x :=
  HasDerivAt.comp (x : ℂ) (Complex.hasDerivAt_cos (x * (2 * z))) a
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x
⊢ HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
[PROOFSTEP]
have c := (b.comp_ofReal.div_const (2 * z)).neg
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun x => -(Complex.cos (↑x * (2 * z)) / (2 * z))) (-(-Complex.sin (↑x * (2 * z)) * (2 * z) / (2 * z))) x
⊢ HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
[PROOFSTEP]
field_simp at c
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun x => -Complex.cos (↑x * (2 * z)) / (2 * z)) (Complex.sin (↑x * (2 * z))) x
⊢ HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
[PROOFSTEP]
simp only [fun y => mul_comm y (2 * z)] at c
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y => y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (fun y => Complex.cos (y * (2 * z))) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun x => -Complex.cos (2 * z * ↑x) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
⊢ HasDerivAt (fun y => -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x
[PROOFSTEP]
exact c
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
[PROOFSTEP]
have der1 :
  ∀ x : ℝ, x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y : ℝ => (cos y : ℂ) ^ n) (-n * sin x * (cos x : ℂ) ^ (n - 1)) x :=
  by
  intro x _
  have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by simpa using (hasDerivAt_cos x).ofReal_comp
  convert HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
  ring
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
[PROOFSTEP]
intro x _
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
[PROOFSTEP]
have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by simpa using (hasDerivAt_cos x).ofReal_comp
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
[PROOFSTEP]
simpa using (hasDerivAt_cos x).ofReal_comp
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
⊢ HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
[PROOFSTEP]
convert HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
[GOAL]
case h.e'_7
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
⊢ -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑n * ↑(cos x) ^ (n - 1) * -↑(sin x)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
[PROOFSTEP]
convert (config := { sameFun := true })
  integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
[GOAL]
case h.e'_2.h.e'_4
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (fun x => Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) = fun x => ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
[PROOFSTEP]
ext1 x
[GOAL]
case h.e'_2.h.e'_4.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
⊢ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    ↑(cos (π / 2)) ^ n * (Complex.sin (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(cos 0) ^ n * (Complex.sin (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0 ..π / 2, -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z))
[PROOFSTEP]
rw [Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div, mul_zero, sub_zero, cos_pi_div_two, Complex.ofReal_zero,
  zero_pow (by positivity : 0 < n), zero_mul, zero_sub, ← integral_neg, ← integral_const_mul]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ 0 < n
[PROOFSTEP]
positivity
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0 ..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ∫ (x : ℝ) in 0 ..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
[PROOFSTEP]
refine' integral_congr fun x _ => _
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.sin (2 * z * ↑x) * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1)) =
    ↑n * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1) * Complex.sin (2 * z * ↑x)
[PROOFSTEP]
ring
[GOAL]
case convert_1
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ IntervalIntegrable (fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) volume 0 (π / 2)
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case convert_1.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)
[PROOFSTEP]
exact
  (continuous_const.mul (Complex.continuous_ofReal.comp continuous_sin)).mul
    ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 1))
[GOAL]
case convert_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ IntervalIntegrable (fun x => Complex.cos (2 * z * ↑x)) volume 0 (π / 2)
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case convert_2.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => Complex.cos (2 * z * ↑x)
[PROOFSTEP]
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
have der1 :
  ∀ x : ℝ,
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y : ℝ => sin y * (cos y : ℂ) ^ (n - 1))
        ((cos x : ℂ) ^ n - (n - 1) * (sin x : ℂ) ^ 2 * (cos x : ℂ) ^ (n - 2)) x :=
  by
  intro x _
  have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
  convert ((Complex.hasDerivAt_sin x).mul c).comp_ofReal using 1
  · ext1 y; simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]
  · simp only [Complex.ofReal_cos, Complex.ofReal_sin]
    rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
    congr 1
    · rw [← pow_succ, Nat.sub_add_cancel (by linarith : 1 ≤ n)]
    · have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
      rw [Nat.sub_sub, this]
      ring
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
[PROOFSTEP]
intro x _
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
[PROOFSTEP]
have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
[PROOFSTEP]
convert ((Complex.hasDerivAt_sin x).mul c).comp_ofReal using 1
[GOAL]
case h.e'_6
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) = fun y => Complex.sin ↑y * ((fun x => x ^ (n - 1)) ∘ Complex.cos) ↑y
[PROOFSTEP]
ext1 y
[GOAL]
case h.e'_6.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
y : ℝ
⊢ ↑(sin y) * ↑(cos y) ^ (n - 1) = Complex.sin ↑y * ((fun x => x ^ (n - 1)) ∘ Complex.cos) ↑y
[PROOFSTEP]
simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]
[GOAL]
case h.e'_7
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2) =
    Complex.cos ↑x * ((fun x => x ^ (n - 1)) ∘ Complex.cos) ↑x +
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x)
[PROOFSTEP]
simp only [Complex.ofReal_cos, Complex.ofReal_sin]
[GOAL]
case h.e'_7
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ Complex.cos ↑x ^ n - (↑n - ↑1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.cos ↑x * ((fun x => x ^ (n - 1)) ∘ Complex.cos) ↑x +
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x)
[PROOFSTEP]
rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
[GOAL]
case h.e'_7
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ Complex.cos ↑x ^ n - (↑n - ↑1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.cos ↑x * Complex.cos ↑x ^ (n - 1) -
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * Complex.sin ↑x)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_7.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ Complex.cos ↑x ^ n = Complex.cos ↑x * Complex.cos ↑x ^ (n - 1)
[PROOFSTEP]
rw [← pow_succ, Nat.sub_add_cancel (by linarith : 1 ≤ n)]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ 1 ≤ n
[PROOFSTEP]
linarith
[GOAL]
case h.e'_7.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ (↑n - ↑1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * Complex.sin ↑x)
[PROOFSTEP]
have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑(n - 1) = ↑n - 1
[PROOFSTEP]
rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
[GOAL]
case h.e'_7.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
this : ↑(n - 1) = ↑n - 1
⊢ (↑n - ↑1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * Complex.sin ↑x)
[PROOFSTEP]
rw [Nat.sub_sub, this]
[GOAL]
case h.e'_7.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
this : ↑(n - 1) = ↑n - 1
⊢ (↑n - ↑1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.sin ↑x * ((↑n - 1) * Complex.cos ↑x ^ (n - (1 + 1)) * Complex.sin ↑x)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
convert integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1
[GOAL]
case h.e'_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    ∫ (x : ℝ) in 0 ..π / 2, ↑(sin x) * ↑(cos x) ^ (n - 1) * Complex.sin (2 * z * ↑x)
[PROOFSTEP]
refine' integral_congr fun x _ => _
[GOAL]
case h.e'_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑(sin x) * ↑(cos x) ^ (n - 1) * Complex.sin (2 * z * ↑x)
[PROOFSTEP]
ring_nf
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    ↑(sin (π / 2)) * ↑(cos (π / 2)) ^ (n - 1) * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(sin 0) * ↑(cos 0) ^ (n - 1) * (-Complex.cos (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0 ..π / 2,
        (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))
[PROOFSTEP]
rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, zero_mul, mul_zero, zero_mul, zero_mul, sub_zero, zero_sub,
  ← integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ ∫ (x : ℝ) in 0 ..π / 2,
      ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
        (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    ∫ (x : ℝ) in 0 ..π / 2,
      -((↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))
case h.e'_3.hf
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ IntervalIntegrable (fun x => ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)) volume 0 (π / 2)
case h.e'_3.hg
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ IntervalIntegrable (fun x => (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))) volume 0 (π / 2)
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ 0 < n - 1
[PROOFSTEP]
rotate_left
[GOAL]
case h.e'_3.hf
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ IntervalIntegrable (fun x => ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)) volume 0 (π / 2)
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case h.e'_3.hf.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ Continuous fun x => ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)
[PROOFSTEP]
exact
  continuous_const.mul
    ((Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).mul
      ((Complex.continuous_ofReal.comp continuous_cos).pow n))
[GOAL]
case h.e'_3.hg
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ IntervalIntegrable (fun x => (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))) volume 0 (π / 2)
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case h.e'_3.hg.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ Continuous fun x => (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
[PROOFSTEP]
exact
  continuous_const.mul
    ((Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).mul
      ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 2)))
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ 0 < n - 1
[PROOFSTEP]
apply Nat.sub_pos_of_lt
[GOAL]
case h.e'_3.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ 1 < n
[PROOFSTEP]
exact one_lt_two.trans_le hn
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ ∫ (x : ℝ) in 0 ..π / 2,
      ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
        (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    ∫ (x : ℝ) in 0 ..π / 2,
      -((↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))
[PROOFSTEP]
refine' integral_congr fun x _ => _
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    -((↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))
[PROOFSTEP]
dsimp only
  -- get rid of real trig functions and divisions by 2 * z:
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)) =
    -((↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z)))
[PROOFSTEP]
rw [Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq, ← mul_div_right_comm, ← mul_div_right_comm, ← sub_div,
  mul_div, ← neg_div]
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ (↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) -
        (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2))) /
      (2 * z) =
    -((Complex.cos ↑x ^ n - (↑n - ↑1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
          -Complex.cos (2 * z * ↑x)) /
      (2 * z)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_3.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) -
      (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) =
    -((Complex.cos ↑x ^ n - (↑n - ↑1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        -Complex.cos (2 * z * ↑x))
[PROOFSTEP]
have : Complex.cos x ^ n = Complex.cos x ^ (n - 2) * Complex.cos x ^ 2 := by
  conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ Complex.cos ↑x ^ n = Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2
[PROOFSTEP]
conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
| Complex.cos ↑x ^ n
[PROOFSTEP]
rw [← Nat.sub_add_cancel hn, pow_add]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
| Complex.cos ↑x ^ n
[PROOFSTEP]
rw [← Nat.sub_add_cancel hn, pow_add]
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
| Complex.cos ↑x ^ n
[PROOFSTEP]
rw [← Nat.sub_add_cancel hn, pow_add]
[GOAL]
case h.e'_3.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
this : Complex.cos ↑x ^ n = Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2
⊢ ↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) -
      (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) =
    -((Complex.cos ↑x ^ n - (↑n - ↑1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        -Complex.cos (2 * z * ↑x))
[PROOFSTEP]
rw [this]
[GOAL]
case h.e'_3.e_a
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
this : Complex.cos ↑x ^ n = Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2
⊢ ↑n * (Complex.cos (2 * z * ↑x) * (Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2)) -
      (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) =
    -((Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2 -
          (↑n - ↑1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        -Complex.cos (2 * z * ↑x))
[PROOFSTEP]
ring
[GOAL]
case convert_1
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ IntervalIntegrable (fun x => ↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) volume 0 (π / 2)
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case convert_1.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ Continuous fun x => ↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
exact
  ((Complex.continuous_ofReal.comp continuous_cos).pow n).sub
    ((continuous_const.mul ((Complex.continuous_ofReal.comp continuous_sin).pow 2)).mul
      ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 2)))
[GOAL]
case convert_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ IntervalIntegrable (fun x => Complex.sin (2 * z * ↑x)) volume 0 (π / 2)
[PROOFSTEP]
apply Continuous.intervalIntegrable
[GOAL]
case convert_2.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ (x : ℝ),
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - ↑1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2))
        x
⊢ Continuous fun x => Complex.sin (2 * z * ↑x)
[PROOFSTEP]
exact Complex.continuous_sin.comp (continuous_const.mul Complex.continuous_ofReal)
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
have nne : (n : ℂ) ≠ 0 := by contrapose! hn; rw [Nat.cast_eq_zero] at hn ; rw [hn]; exact zero_lt_two
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
contrapose! hn
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
hn : ↑n = 0
⊢ n < 2
[PROOFSTEP]
rw [Nat.cast_eq_zero] at hn
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ n < 2
[PROOFSTEP]
rw [hn]
[GOAL]
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
have := integral_cos_mul_cos_pow_aux hn hz
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
rw [integral_sin_mul_sin_mul_cos_pow_eq hn hz, sub_eq_neg_add, mul_add, ← sub_eq_iff_eq_add] at this
[GOAL]
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2)
[PROOFSTEP]
convert congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this using 1
[GOAL]
case h.e'_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ (1 - 4 * z ^ 2 / ↑n ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n =
    -((∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
            ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n)) *
        (2 * z) ^ 2 /
      ↑(n ^ 2)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ (↑n - 1) / ↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    -(↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))) *
        (2 * z) ^ 2 /
      ↑(n ^ 2)
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ ((↑n ^ 2 - 4 * z ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) *
      (2 * z * (2 * z) * ↑n ^ 2) =
    (↑n * (↑n * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) -
          (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) * (2 * z * (2 * z))) *
        (2 * z) ^ 2 *
      ↑n ^ 2
[PROOFSTEP]
ring
[GOAL]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
nne : ↑n ≠ 0
this :
  (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      ↑n / (2 * z) * (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * -((↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))
⊢ ((↑n - 1) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) *
      (2 * z * (2 * z) * ↑n ^ 2) =
    ↑n * ((↑n - 1) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) * (2 * z) ^ 2 * ↑n
[PROOFSTEP]
ring
[GOAL]
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ (1 - z ^ 2 / (↑n + 1) ^ 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n + 2) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
[PROOFSTEP]
convert integral_cos_mul_cos_pow (by linarith : 2 ≤ 2 * n + 2) hz using 3
[GOAL]
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ 2 ≤ 2 * n + 2
[PROOFSTEP]
linarith
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / ↑(2 * n + 2) ^ 2
[PROOFSTEP]
simp only [Nat.cast_add, Nat.cast_mul, Nat.cast_two]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2) ^ 2
[PROOFSTEP]
nth_rw 2 [← mul_one (2 : ℂ)]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / (2 * ↑n + 2 * 1) ^ 2
[PROOFSTEP]
rw [← mul_add, mul_pow, ← div_div]
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ z ^ 2 / (↑n + 1) ^ 2 = 4 * z ^ 2 / 2 ^ 2 / (↑n + 1) ^ 2
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_5.h.e'_5
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = ↑(2 * n + 2) - 1
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h.e'_5.h.e'_5
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 1 = 2 * ↑n + 2 - 1
[PROOFSTEP]
ring
[GOAL]
case h.e'_3.h.e'_5.h.e'_6
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = ↑(2 * n + 2)
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.h.e'_5.h.e'_6
z : ℂ
n✝ n : ℕ
hz : z ≠ 0
⊢ 2 * ↑n + 2 = 2 * ↑n + 2
[PROOFSTEP]
ring
[GOAL]
z : ℂ
n✝ n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
rw [mul_comm (1 / 2 : ℝ), ← div_eq_iff (one_div_ne_zero (two_ne_zero' ℝ)), ← div_mul, div_one, mul_two]
[GOAL]
z : ℂ
n✝ n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
have L : IntervalIntegrable _ volume 0 (π / 2) := (continuous_sin.pow n).intervalIntegrable _ _
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
have R : IntervalIntegrable _ volume (π / 2) π := (continuous_sin.pow n).intervalIntegrable _ _
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n
[PROOFSTEP]
rw [← integral_add_adjacent_intervals L R]
  -- Porting note: was `congr 1` but it timeouts
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n =
    (∫ (x : ℝ) in 0 ..π / 2, sin x ^ n) + ∫ (x : ℝ) in π / 2 ..π, sin x ^ n
[PROOFSTEP]
refine congr_arg₂ _ ?_ ?_
[GOAL]
case refine_1
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π / 2, sin x ^ n
[PROOFSTEP]
nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ 0 = π / 2 - π / 2
[PROOFSTEP]
ring
[GOAL]
case refine_1
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in π / 2 - π / 2 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π / 2, sin x ^ n
[PROOFSTEP]
nth_rw 3 [(by ring : π / 2 = π / 2 - 0)]
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π / 2 = π / 2 - 0
[PROOFSTEP]
ring
[GOAL]
case refine_1
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in π / 2 - π / 2 ..π / 2 - 0, cos x ^ n = ∫ (x : ℝ) in 0 ..π / 2, sin x ^ n
[PROOFSTEP]
rw [← integral_comp_sub_left]
[GOAL]
case refine_1
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos (π / 2 - x) ^ n = ∫ (x : ℝ) in 0 ..π / 2, sin x ^ n
[PROOFSTEP]
refine' integral_congr fun x _ => _
[GOAL]
case refine_1
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ cos (π / 2 - x) ^ n = sin x ^ n
[PROOFSTEP]
rw [cos_pi_div_two_sub]
[GOAL]
case refine_2
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in π / 2 ..π, sin x ^ n
[PROOFSTEP]
nth_rw 3 [(by ring : π = π / 2 + π / 2)]
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π = π / 2 + π / 2
[PROOFSTEP]
ring
[GOAL]
case refine_2
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in π / 2 ..π / 2 + π / 2, sin x ^ n
[PROOFSTEP]
nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]
[GOAL]
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π / 2 = 0 + π / 2
[PROOFSTEP]
ring
[GOAL]
case refine_2
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 + π / 2 ..π / 2 + π / 2, sin x ^ n
[PROOFSTEP]
rw [← integral_comp_add_right]
[GOAL]
case refine_2
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π / 2, sin (x + π / 2) ^ n
[PROOFSTEP]
refine' integral_congr fun x _ => _
[GOAL]
case refine_2
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ cos x ^ n = sin (x + π / 2) ^ n
[PROOFSTEP]
rw [sin_add_pi_div_two]
[GOAL]
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))
[PROOFSTEP]
rcases eq_or_ne z 0 with (rfl | hz)
[GOAL]
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))
[PROOFSTEP]
simp
[GOAL]
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))
[PROOFSTEP]
induction' n with n hn
[GOAL]
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))
[PROOFSTEP]
simp_rw [Nat.zero_eq, mul_zero, pow_zero, mul_one, Finset.prod_range_zero, mul_one, integral_one, sub_zero]
[GOAL]
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = (↑π * z * ∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x)) / ↑(π / 2)
[PROOFSTEP]
rw [integral_cos_mul_complex (mul_ne_zero two_ne_zero hz), Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div,
  sub_zero, (by push_cast ; field_simp; ring : 2 * z * ↑(π / 2) = π * z)]
[GOAL]
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑(π / 2) = ↑π * z
[PROOFSTEP]
push_cast
[GOAL]
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * (↑π / 2) = ↑π * z
[PROOFSTEP]
field_simp
[GOAL]
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ 2 * z * ↑π = ↑π * z * 2
[PROOFSTEP]
ring
[GOAL]
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) = ↑π * z * (Complex.sin (↑π * z) / (2 * z)) / ↑(π / 2)
[PROOFSTEP]
field_simp [Complex.ofReal_ne_zero.mpr pi_pos.ne']
[GOAL]
case inr.zero
z✝ : ℂ
n : ℕ
z : ℂ
hz : z ≠ 0
⊢ Complex.sin (↑π * z) * (2 * z * ↑π) = ↑π * z * Complex.sin (↑π * z) * 2
[PROOFSTEP]
ring
[GOAL]
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))
[PROOFSTEP]
rw [hn, Finset.prod_range_succ]
[GOAL]
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))
[PROOFSTEP]
set A := ∏ j in Finset.range n, ((1 : ℂ) - z ^ 2 / ((j : ℂ) + 1) ^ 2)
[GOAL]
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))
[PROOFSTEP]
set B := ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (2 * n)
[GOAL]
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))
[PROOFSTEP]
set C := ∫ x in (0 : ℝ)..π / 2, cos x ^ (2 * n)
[GOAL]
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))
[PROOFSTEP]
have aux' : 2 * n.succ = 2 * n + 2 := by rw [Nat.succ_eq_add_one, mul_add, mul_one]
[GOAL]
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
[PROOFSTEP]
rw [Nat.succ_eq_add_one, mul_add, mul_one]
[GOAL]
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))
[PROOFSTEP]
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, zero_mul, zero_mul, zero_mul, sub_zero,
    zero_div, zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_eq_ofNat]
[GOAL]
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
[PROOFSTEP]
rw [integral_cos_pow_eq]
[GOAL]
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
[PROOFSTEP]
dsimp only
[GOAL]
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)
[PROOFSTEP]
rw [integral_cos_pow_eq, aux', integral_sin_pow, sin_zero, sin_pi, pow_succ, zero_mul, zero_mul, zero_mul, sub_zero,
  zero_div, zero_add, ← mul_assoc, ← mul_assoc, mul_comm (1 / 2 : ℝ) _, Nat.cast_mul, Nat.cast_eq_ofNat]
[GOAL]
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))
[PROOFSTEP]
rw [this]
[GOAL]
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)
[PROOFSTEP]
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 : ℝ)
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
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))
[PROOFSTEP]
nth_rw 2 [Nat.succ_eq_add_one]
[GOAL]
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))
[PROOFSTEP]
rw [Nat.cast_add_one]
[GOAL]
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))
[PROOFSTEP]
ring
[GOAL]
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)
[PROOFSTEP]
rw [this]
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
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)
[PROOFSTEP]
rw [this, Complex.ofReal_mul, Complex.ofReal_div]
[GOAL]
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)
[PROOFSTEP]
have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
[GOAL]
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)
[PROOFSTEP]
have : 2 * (n : ℂ) + 1 ≠ 0 :=
  by
  convert (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
  simp
[GOAL]
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
[PROOFSTEP]
convert (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
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
[GOAL]
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
[PROOFSTEP]
convert (Nat.cast_add_one_ne_zero (2 * n + 1) : (↑(2 * n + 1) + 1 : ℂ) ≠ 0) using 1
[GOAL]
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
[PROOFSTEP]
push_cast
[GOAL]
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
[PROOFSTEP]
ring
[GOAL]
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)
[PROOFSTEP]
field_simp
[GOAL]
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))
[PROOFSTEP]
ring
[GOAL]
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
[PROOFSTEP]
convert integral_cos_mul_cos_pow_even n hz
[GOAL]
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
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
⊢ Tendsto (fun n => (∫ (x : ℝ) in 0 ..π / 2, ↑(cos x) ^ n * f x) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)) atTop (𝓝 (f 0))
[PROOFSTEP]
simp_rw [div_eq_inv_mul (α := ℂ), ← Complex.ofReal_inv, integral_of_le pi_div_two_pos.le, ←
  MeasureTheory.integral_Icc_eq_integral_Ioc, ← Complex.ofReal_pow, ← Complex.real_smul]
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
⊢ Tendsto (fun n => (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x) atTop
    (𝓝 (f 0))
[PROOFSTEP]
have c_lt : ∀ y : ℝ, y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0 := fun y hy hy' =>
  cos_lt_cos_of_nonneg_of_le_pi_div_two (le_refl 0) hy.2 (lt_of_le_of_ne hy.1 hy'.symm)
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
⊢ Tendsto (fun n => (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x) atTop
    (𝓝 (f 0))
[PROOFSTEP]
have c_nonneg : ∀ x : ℝ, x ∈ Icc 0 (π / 2) → 0 ≤ cos x := fun x hx =>
  cos_nonneg_of_mem_Icc ((Icc_subset_Icc_left (neg_nonpos_of_nonneg pi_div_two_pos.le)) hx)
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
⊢ Tendsto (fun n => (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x) atTop
    (𝓝 (f 0))
[PROOFSTEP]
have c_zero_pos : 0 < cos 0 := by rw [cos_zero]; exact zero_lt_one
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
⊢ 0 < cos 0
[PROOFSTEP]
rw [cos_zero]
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ Tendsto (fun n => (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x) atTop
    (𝓝 (f 0))
[PROOFSTEP]
have zero_mem : (0 : ℝ) ∈ closure (interior (Icc 0 (π / 2))) :=
  by
  rw [interior_Icc, closure_Ioo pi_div_two_pos.ne, left_mem_Icc]
  exact pi_div_two_pos.le
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ 0 ∈ closure (interior (Icc 0 (π / 2)))
[PROOFSTEP]
rw [interior_Icc, closure_Ioo pi_div_two_pos.ne, left_mem_Icc]
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ 0 ≤ π / 2
[PROOFSTEP]
exact pi_div_two_pos.le
[GOAL]
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ (y : ℝ), y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0
c_nonneg : ∀ (x : ℝ), x ∈ Icc 0 (π / 2) → 0 ≤ cos x
c_zero_pos : 0 < cos 0
zero_mem : 0 ∈ closure (interior (Icc 0 (π / 2)))
⊢ Tendsto (fun n => (∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n)⁻¹ • ∫ (x : ℝ) in Icc 0 (π / 2), cos x ^ n • f x) atTop
    (𝓝 (f 0))
[PROOFSTEP]
exact
  tendsto_set_integral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn isCompact_Icc continuousOn_cos c_lt
    c_nonneg c_zero_pos zero_mem hf
[GOAL]
z : ℂ
⊢ Tendsto (fun n => ↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
[PROOFSTEP]
have A :
  Tendsto
    (fun 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) : ℝ))
    atTop (𝓝 <| _) :=
  Tendsto.congr (fun n => sin_pi_mul_eq z n) tendsto_const_nhds
[GOAL]
z : ℂ
A :
  Tendsto
    (fun 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)))
    atTop (𝓝 (Complex.sin (↑π * z)))
⊢ Tendsto (fun n => ↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
[PROOFSTEP]
have : 𝓝 (Complex.sin (π * z)) = 𝓝 (Complex.sin (π * z) * 1) := by rw [mul_one]
[GOAL]
z : ℂ
A :
  Tendsto
    (fun 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)))
    atTop (𝓝 (Complex.sin (↑π * z)))
⊢ 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
[PROOFSTEP]
rw [mul_one]
[GOAL]
z : ℂ
A :
  Tendsto
    (fun 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)))
    atTop (𝓝 (Complex.sin (↑π * z)))
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
⊢ Tendsto (fun n => ↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
[PROOFSTEP]
simp_rw [this, mul_div_assoc] at A
[GOAL]
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto (fun n => ↑π * z * ∏ j in Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (Complex.sin (↑π * z)))
[PROOFSTEP]
convert (tendsto_mul_iff_of_ne_zero _ one_ne_zero).mp A
[GOAL]
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
        ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))
    atTop (𝓝 1)
[PROOFSTEP]
suffices :
  Tendsto
    (fun n : ℕ =>
      (∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) / (∫ x in (0 : ℝ)..π / 2, cos x ^ n : ℝ))
    atTop (𝓝 1)
[GOAL]
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this :
  Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
        ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ (2 * n)))
    atTop (𝓝 1)
case this
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)
[PROOFSTEP]
exact this.comp (tendsto_id.const_mul_atTop' zero_lt_two)
[GOAL]
case this
z : ℂ
this : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
⊢ Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)
[PROOFSTEP]
have : ContinuousOn (fun x : ℝ => Complex.cos (2 * z * x)) (Icc 0 (π / 2)) :=
  (Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).continuousOn
[GOAL]
case this
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ Tendsto
    (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n))
    atTop (𝓝 1)
[PROOFSTEP]
convert tendsto_integral_cos_pow_mul_div this using 1
[GOAL]
case h.e'_3
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ (fun n => (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)) =
    fun n => (∫ (x : ℝ) in 0 ..π / 2, ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) =
    (∫ (x : ℝ) in 0 ..π / 2, ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)) / ↑(∫ (x : ℝ) in 0 ..π / 2, cos x ^ n)
[PROOFSTEP]
congr 2 with x : 1
[GOAL]
case h.e'_3.h.e_a.e_f.h
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
n : ℕ
x : ℝ
⊢ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case h.e'_5
z : ℂ
this✝ : 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)
A :
  Tendsto
    (fun 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))))
    atTop (𝓝 (Complex.sin (↑π * z) * 1))
this : ContinuousOn (fun x => Complex.cos (2 * z * ↑x)) (Icc 0 (π / 2))
⊢ 𝓝 1 = 𝓝 (Complex.cos (2 * z * ↑0))
[PROOFSTEP]
rw [Complex.ofReal_zero, mul_zero, Complex.cos_zero]
[GOAL]
x : ℝ
⊢ Tendsto (fun n => π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (π * x)))
[PROOFSTEP]
convert (Complex.continuous_re.tendsto _).comp (Complex.tendsto_euler_sin_prod x) using 1
[GOAL]
case h.e'_3
x : ℝ
⊢ (fun n => π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2)) =
    Complex.re ∘ fun n => ↑π * ↑x * ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)
[PROOFSTEP]
ext1 n
[GOAL]
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    (Complex.re ∘ fun n => ↑π * ↑x * ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)) n
[PROOFSTEP]
rw [Function.comp_apply, ← Complex.ofReal_mul, Complex.ofReal_mul_re]
[GOAL]
case h.e'_3.h
x : ℝ
n : ℕ
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
[PROOFSTEP]
suffices
  (∏ j : ℕ in Finset.range n, ((1 : ℂ) - (x : ℂ) ^ 2 / ((j : ℂ) + 1) ^ 2)) =
    (∏ j : ℕ in Finset.range n, ((1 : ℝ) - x ^ 2 / ((j : ℝ) + 1) ^ 2) : ℝ)
  by rw [this, Complex.ofReal_re]
[GOAL]
x : ℝ
n : ℕ
this : ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
⊢ π * x * ∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
[PROOFSTEP]
rw [this, Complex.ofReal_re]
[GOAL]
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ↑(∏ j in Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2))
[PROOFSTEP]
rw [Complex.ofReal_prod]
[GOAL]
case h.e'_3.h
x : ℝ
n : ℕ
⊢ ∏ j in Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2) = ∏ i in Finset.range n, ↑(1 - x ^ 2 / (↑i + 1) ^ 2)
[PROOFSTEP]
refine' Finset.prod_congr (by rfl) fun n _ => _
[GOAL]
x : ℝ
n : ℕ
⊢ Finset.range n = Finset.range n
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h
x : ℝ
n✝ n : ℕ
x✝ : n ∈ Finset.range n✝
⊢ 1 - ↑x ^ 2 / (↑n + 1) ^ 2 = ↑(1 - x ^ 2 / (↑n + 1) ^ 2)
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_5
x : ℝ
⊢ 𝓝 (sin (π * x)) = 𝓝 (Complex.sin (↑π * ↑x)).re
[PROOFSTEP]
rw [← Complex.ofReal_mul, ← Complex.ofReal_sin, Complex.ofReal_re]


[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
⊢ ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
⊢ ConformalAt f x → IsConformalMap (fderiv ℝ f x)
[PROOFSTEP]
rintro ⟨f', hf, hf'⟩
[GOAL]
case mp.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
f' : X →L[ℝ] Y
hf : HasFDerivAt f f' x
hf' : IsConformalMap f'
⊢ IsConformalMap (fderiv ℝ f x)
[PROOFSTEP]
rwa [hf.fderiv]
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
⊢ IsConformalMap (fderiv ℝ f x) → ConformalAt f x
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
⊢ ConformalAt f x
[PROOFSTEP]
by_cases h : DifferentiableAt ℝ f x
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : DifferentiableAt ℝ f x
⊢ ConformalAt f x
[PROOFSTEP]
exact ⟨fderiv ℝ f x, h.hasFDerivAt, H⟩
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
⊢ ConformalAt f x
[PROOFSTEP]
nontriviality X
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
✝ : Nontrivial X
⊢ ConformalAt f x
[PROOFSTEP]
exact absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
hf : ConformalAt f x
⊢ ConformalAt (g ∘ f) x
[PROOFSTEP]
rcases hf with ⟨f', hf₁, cf⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
⊢ ConformalAt (g ∘ f) x
[PROOFSTEP]
rcases hg with ⟨g', hg₁, cg⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
g' : Y →L[ℝ] Z
hg₁ : HasFDerivAt g g' (f x)
cg : IsConformalMap g'
⊢ ConformalAt (g ∘ f) x
[PROOFSTEP]
exact ⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩


[GOAL]
E : Type u_1
X : Type u_2
c : E
f : ContDiffBump c
⊢ 1 < f.rOut / f.rIn
[PROOFSTEP]
rw [one_lt_div f.rIn_pos]
[GOAL]
E : Type u_1
X : Type u_2
c : E
f : ContDiffBump c
⊢ f.rIn < f.rOut
[PROOFSTEP]
exact f.rIn_lt_rOut
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
x : E
⊢ ↑f (c - x) = ↑f (c + x)
[PROOFSTEP]
simp [f.apply, ContDiffBumpBase.symmetric]
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f✝ : ContDiffBump c
x✝ : E
n : ℕ∞
f : ContDiffBump 0
x : E
⊢ ↑f (-x) = ↑f x
[PROOFSTEP]
simp_rw [← zero_sub, f.sub, zero_add]
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ closedBall c f.rIn
⊢ ↑f x = 1
[PROOFSTEP]
apply ContDiffBumpBase.eq_one _ _ f.one_lt_rOut_div_rIn
[GOAL]
case a
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ closedBall c f.rIn
⊢ ‖(fun x => f.rIn⁻¹ • (x - c)) x‖ ≤ 1
[PROOFSTEP]
simpa only [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_nonneg f.rIn_pos.le, ← div_eq_inv_mul,
  div_le_one f.rIn_pos] using mem_closedBall_iff_norm.1 hx
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
⊢ support ↑f = ball c f.rOut
[PROOFSTEP]
simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
⊢ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) = ball c f.rOut
[PROOFSTEP]
ext x
[GOAL]
case h
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x✝ : E
n : ℕ∞
x : E
⊢ x ∈ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) ↔ x ∈ ball c f.rOut
[PROOFSTEP]
simp only [mem_ball_iff_norm, sub_zero, norm_smul, mem_preimage, Real.norm_eq_abs, abs_inv, abs_of_pos f.rIn_pos, ←
  div_eq_inv_mul, div_lt_div_right f.rIn_pos]
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
⊢ tsupport ↑f = closedBall c f.rOut
[PROOFSTEP]
simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : x ∈ ball c f.rOut
⊢ ↑f x ≠ 0
[PROOFSTEP]
rwa [← support_eq, mem_support] at hx
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
hx : f.rOut ≤ dist x c
⊢ ↑f x = 0
[PROOFSTEP]
rwa [← nmem_support, support_eq, mem_ball, not_lt]
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup X
inst✝² : NormedSpace ℝ X
inst✝¹ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝ : FiniteDimensional ℝ E
⊢ HasCompactSupport ↑f
[PROOFSTEP]
simp_rw [HasCompactSupport, f.tsupport_eq, isCompact_closedBall]
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x✝ : E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ n c s x
hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ n g s x
⊢ ContDiffWithinAt ℝ n (fun x => ↑(f x) (g x)) s x
[PROOFSTEP]
change
  ContDiffWithinAt ℝ n
    (uncurry (someContDiffBumpBase E).toFun ∘ fun x : X => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x✝ : E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ n c s x
hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ n g s x
⊢ ContDiffWithinAt ℝ n
    (uncurry (someContDiffBumpBase E).toFun ∘ fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
[PROOFSTEP]
refine (((someContDiffBumpBase E).smooth.contDiffAt ?_).of_le le_top).comp_contDiffWithinAt x ?_
[GOAL]
case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x✝ : E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ n c s x
hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ n g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))
[PROOFSTEP]
exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem
[GOAL]
case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x✝ : E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ n c s x
hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x
hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x
hg : ContDiffWithinAt ℝ n g s x
⊢ ContDiffWithinAt ℝ n (fun x => ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
[PROOFSTEP]
exact (hR.div hr (f x).rIn_pos.ne').prod ((hr.inv (f x).rIn_pos.ne').smul (hg.sub hc))
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x : E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ContDiff ℝ n c
hr : ContDiff ℝ n fun x => (f x).rIn
hR : ContDiff ℝ n fun x => (f x).rOut
hg : ContDiff ℝ n g
⊢ ContDiff ℝ n fun x => ↑(f x) (g x)
[PROOFSTEP]
rw [contDiff_iff_contDiffAt] at *
[GOAL]
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
c✝ : E
f✝ : ContDiffBump c✝
x : E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ n c x
hr : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ n g x
⊢ ∀ (x : X), ContDiffAt ℝ n (fun x => ↑(f x) (g x)) x
[PROOFSTEP]
exact fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)


[GOAL]
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
by_cases h : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
[GOAL]
case pos
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
exact exists_hasDerivAt_eq_zero' hab hfa hfb fun x hx => (h x hx).hasDerivAt
[GOAL]
case neg
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ¬∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
obtain ⟨c, hc, hcdiff⟩ : ∃ x ∈ Ioo a b, ¬DifferentiableAt ℝ f x
[GOAL]
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ¬∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x
[PROOFSTEP]
push_neg at h
[GOAL]
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x
⊢ ∃ x, x ∈ Ioo a b ∧ ¬DifferentiableAt ℝ f x
[PROOFSTEP]
exact h
[GOAL]
case neg.intro.intro
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : ¬∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
c : ℝ
hc : c ∈ Ioo a b
hcdiff : ¬DifferentiableAt ℝ f c
⊢ ∃ c, c ∈ Ioo a b ∧ deriv f c = 0
[PROOFSTEP]
exact ⟨c, hc, deriv_zero_of_not_differentiableAt hcdiff⟩