-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem integral_cos_pow_eq (n : ℕ) :
    (∫ x in (0 : ℝ)..π / 2, cos x ^ n) = 1 / 2 * ∫ x in (0 : ℝ)..π, sin x ^ n

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

Tactic:
nth_rw 3 [(by ring : π = π / 2 + π / 2)]

Result:
case e_a
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

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

Tactic:
refine integral_congr fun x _ => ?_

Result:
case e_a
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

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

Tactic:
rw [cos_pi_div_two_sub]

Result:
no goals

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

Tactic:
rw [← integral_comp_add_right]

Result:
case e_a
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

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

Tactic:
rw [← integral_add_adjacent_intervals L R]

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

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

Tactic:
nth_rw 3 [(by ring : π / 2 = π / 2 - 0)]

Result:
case e_a
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

Proof state:
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ n

Tactic:
rw [mul_comm (1 / 2 : ℝ), ← div_eq_iff (one_div_ne_zero (two_ne_zero' ℝ)), ← div_mul, div_one,
  mul_two]

Result:
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n

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

Tactic:
rw [← integral_comp_sub_left]

Result:
case e_a
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

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

Tactic:
nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]

Result:
case e_a
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

Proof state:
n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ 0 = π / 2 - π / 2

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π / 2 = 0 + π / 2

Tactic:
ring

Result:
no goals

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

Tactic:
refine integral_congr fun x _ => ?_

Result:
case e_a
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

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

Tactic:
congr 1

Result:
case e_a
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

case e_a
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

Proof state:
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 ..π, sin x ^ n

Tactic:
have L : IntervalIntegrable _ volume 0 (π / 2) := (continuous_sin.pow n).intervalIntegrable _ _

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

Proof state:
n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π / 2 = π / 2 - 0

Tactic:
ring

Result:
no goals

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

Tactic:
rw [sin_add_pi_div_two]

Result:
no goals

Proof state:
n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π = π / 2 + π / 2

Tactic:
ring

Result:
no goals

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

Tactic:
nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]

Result:
case e_a
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