-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem integral_cos_mul_cos_pow (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)

Proof state:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : ↑n = 0
⊢ n < 2

Tactic:
rw [Nat.cast_eq_zero] at hn

Result:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ n < 2

Proof state:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ 0 < 2

Tactic:
exact zero_lt_two

Result:
no goals

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

Tactic:
convert congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this using 1 <;> field_simp <;> ring

Result:
no goals

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

Tactic:
rw [integral_sin_mul_sin_mul_cos_pow_eq hn hz, sub_eq_neg_add, mul_add, ← sub_eq_iff_eq_add]
  at this

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

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

Tactic:
have nne : (n : ℂ) ≠ 0 := by
  contrapose! hn; rw [Nat.cast_eq_zero] at hn; rw [hn]; exact zero_lt_two

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

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

Tactic:
have := integral_cos_mul_cos_pow_aux hn hz

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

Proof state:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ n < 2

Tactic:
rw [hn]

Result:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : n = 0
⊢ 0 < 2

Proof state:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ↑n ≠ 0

Tactic:
contrapose! hn

Result:
z : ℂ
n : ℕ
hz : z ≠ 0
hn : ↑n = 0
⊢ n < 2