z : ℂ
n✝ n : ℕ
⊢ ((∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) = ∫ (x : ℝ) in 0 ..π, sin x ^ n
z : ℂ
n✝ n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) = 1 / 2 * ∫ (x : ℝ) in 0 ..π, sin x ^ n
rw [mul_comm (1 / 2 : ℝ), ← div_eq_iff (one_div_ne_zero (two_ne_zero' ℝ)), ← div_mul, div_one,
  mul_two]
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
z : ℂ
n✝ n : ℕ
⊢ ((∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) + ∫ (x : ℝ) in 0 ..π / 2, cos x ^ n) = ∫ (x : ℝ) in 0 ..π, sin x ^ n
have L : IntervalIntegrable _ volume 0 (π / 2) := (continuous_sin.pow n).intervalIntegrable _ _
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
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
have R : IntervalIntegrable _ volume (π / 2) π := (continuous_sin.pow n).intervalIntegrable _ _
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
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
rw [← integral_add_adjacent_intervals L R]
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

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
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
refine congr_arg₂ _ ?_ ?_
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
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
nth_rw 1 [(by ring : 0 = π / 2 - π / 2)]
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
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
nth_rw 3 [(by ring : π / 2 = π / 2 - 0)]
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
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
rw [← integral_comp_sub_left]
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
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
refine' integral_congr fun x _ => _
no goals
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
rw [cos_pi_div_two_sub]
no goals
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
ring
no goals
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
ring
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
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
nth_rw 3 [(by ring : π = π / 2 + π / 2)]
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
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
nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]
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
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
rw [← integral_comp_add_right]
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
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
refine' integral_congr fun x _ => _
no goals
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
rw [sin_add_pi_div_two]
no goals
z : ℂ
n✝ n : ℕ
L : IntervalIntegrable (fun b => sin b ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun b => sin b ^ n) volume (π / 2) π
⊢ π = π / 2 + π / 2
ring
no goals
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
ring