a b : ℝ
n : ℕ
H : ∀ (x : ℝ), x ∈ Set.Icc 0 π → sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)
no goals
a b : ℝ
n : ℕ
H : ∀ (x : ℝ), x ∈ Set.Icc 0 π → sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ (∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1)) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
refine' integral_mono_on pi_pos.le _ _ H <;> exact (continuous_sin.pow _).intervalIntegrable 0 π