case inl
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)

case inr
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)
cases' le_or_lt a b with hab hab
no goals
case inl
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)
calc
  (∫ x in Ι a b, |x - a| ^ n) = ∫ x in a..b, |x - a| ^ n := by
    rw [uIoc_of_le hab, ← integral_of_le hab]
  _ = ∫ x in (0)..(b - a), x ^ n := by
    simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
    refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| _) rfl
    rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
    exact hx.1
  _ = |b - a| ^ (n + 1) / (n + 1) := by simp [abs_of_nonneg (sub_nonneg.2 hab)]
no goals
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = ∫ (x : ℝ) in a..b, abs (x - a) ^ n
rw [uIoc_of_le hab, ← integral_of_le hab]
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in 0 ..b - a, abs x ^ n) = ∫ (x : ℝ) in 0 ..b - a, x ^ n
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in a..b, abs (x - a) ^ n) = ∫ (x : ℝ) in 0 ..b - a, x ^ n
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in 0 ..b - a, abs x ^ n) = ∫ (x : ℝ) in 0 ..b - a, x ^ n
refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| _) rfl
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x
rw [uIcc_of_le (sub_nonneg.2 hab)] at hx
no goals
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x
exact hx.1
no goals
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ (∫ (x : ℝ) in 0 ..b - a, x ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)
simp [abs_of_nonneg (sub_nonneg.2 hab)]
no goals
case inr
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)
calc
  (∫ x in Ι a b, |x - a| ^ n) = ∫ x in b..a, |x - a| ^ n := by
    rw [uIoc_of_lt hab, ← integral_of_le hab.le]
  _ = ∫ x in b - a..0, (-x) ^ n := by
    simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
    refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| _) rfl
    rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
    exact hx.2
  _ = |b - a| ^ (n + 1) / (n + 1) := by
    simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]
no goals
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in Ι a b, abs (x - a) ^ n) = ∫ (x : ℝ) in b..a, abs (x - a) ^ n
rw [uIoc_of_lt hab, ← integral_of_le hab.le]
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in b - a..0, abs x ^ n) = ∫ (x : ℝ) in b - a..0, (-x) ^ n
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in b..a, abs (x - a) ^ n) = ∫ (x : ℝ) in b - a..0, (-x) ^ n
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in b - a..0, abs x ^ n) = ∫ (x : ℝ) in b - a..0, (-x) ^ n
refine' integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| _) rfl
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0
rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx
no goals
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0
exact hx.2
no goals
a b : ℝ
n : ℕ
hab : b < a
⊢ (∫ (x : ℝ) in b - a..0, (-x) ^ n) = abs (b - a) ^ (n + 1) / (↑n + 1)
simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]