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)

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))

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)

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)
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)
convert
  integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_sin_comp_const_mul hz x) _ _ using 1
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
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
intro x _
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
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
have c := HasDerivAt.comp (x : ℂ) (hasDerivAt_pow (n - 1) _) (Complex.hasDerivAt_cos x)
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

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)
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
convert ((Complex.hasDerivAt_sin x).mul c).comp_ofReal using 1
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
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
ext1 y
no goals
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
simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]
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)
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)
simp only [Complex.ofReal_cos, Complex.ofReal_sin]
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)
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)
rw [mul_neg, mul_neg, ← sub_eq_add_neg, Function.comp_apply]
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)

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)
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)
congr 1
no goals
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)
rw [← pow_succ, Nat.sub_add_cancel (by linarith : 1 ≤ n)]
no goals
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
linarith
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)
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)
have : ((n - 1 : ℕ) : ℂ) = (n : ℂ) - 1 := by
  rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
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)
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)
rw [Nat.sub_sub, this]
no goals
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)
ring
no goals
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
rw [Nat.cast_sub (one_le_two.trans hn), Nat.cast_one]
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)
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)
refine' integral_congr fun x _ => _
no goals
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)
ring_nf
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
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))
rw [sin_zero, cos_pi_div_two, Complex.ofReal_zero, zero_pow, MulZeroClass.zero_mul,
  MulZeroClass.mul_zero, MulZeroClass.zero_mul, MulZeroClass.zero_mul, sub_zero, zero_sub, ←
  integral_neg, ← integral_const_mul, ← integral_const_mul, ← integral_sub]
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

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
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
rotate_left
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)))
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)))
refine' integral_congr fun x _ => _
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)))
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)))
dsimp only
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)
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)))
rw [Complex.ofReal_cos, Complex.ofReal_sin, Complex.sin_sq, ← mul_div_right_comm, ←
  mul_div_right_comm, ← sub_div, mul_div, ← neg_div]
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))
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)
congr 1
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))
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))
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]
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))
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))
rw [this]
no goals
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))
ring
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)
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)
apply Continuous.intervalIntegrable
no goals
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)
exact
  continuous_const.mul
    ((Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).mul
      ((Complex.continuous_ofReal.comp continuous_cos).pow n))
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))
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)
apply Continuous.intervalIntegrable
no goals
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))
exact
  continuous_const.mul
    ((Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)).mul
      ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 2)))
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
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
apply Nat.sub_pos_of_lt
no goals
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
exact one_lt_two.trans_le hn
no goals
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
conv_lhs => rw [← Nat.sub_add_cancel hn, pow_add]
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)
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)
apply Continuous.intervalIntegrable
no goals
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)
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)))
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)
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)
apply Continuous.intervalIntegrable
no goals
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)
exact Complex.continuous_sin.comp (continuous_const.mul Complex.continuous_ofReal)