-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_pow_abs_sub_uIoc : ∫ x in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (n + 1)

Proof state:
case inr
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
calc
  ∫ x in Ι a b, |x - a| ^ n = ∫ x in b..a, |x - a| ^ n := by
    rw [uIoc_of_ge hab.le, ← 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)]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x

Tactic:
rw [uIcc_of_le (sub_nonneg.2 hab)] at hx

Result:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x

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

Tactic:
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)]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in a..b, |x - a| ^ n

Tactic:
rw [uIoc_of_le hab, ← integral_of_le hab]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0

Tactic:
rw [uIcc_of_le (sub_nonpos.2 hab.le)] at hx

Result:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0

Proof state:
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b..a, |x - a| ^ n = ∫ (x : ℝ) in b - a..0, (-x) ^ n

Tactic:
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]

Result:
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, |x| ^ n = ∫ (x : ℝ) in b - a..0, (-x) ^ n

Proof state:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, |x - a| ^ n = ∫ (x : ℝ) in 0 ..b - a, x ^ n

Tactic:
simp only [integral_comp_sub_right fun x => |x| ^ n, sub_self]

Result:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0 ..b - a, |x| ^ n = ∫ (x : ℝ) in 0 ..b - a, x ^ n

Proof state:
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = ∫ (x : ℝ) in b..a, |x - a| ^ n

Tactic:
rw [uIoc_of_ge hab.le, ← integral_of_le hab.le]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ Set.Icc (b - a) 0
⊢ x ≤ 0

Tactic:
exact hx.2

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, (-x) ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
simp [integral_comp_neg fun x => x ^ n, abs_of_neg (sub_neg.2 hab)]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in b - a..0, |x| ^ n = ∫ (x : ℝ) in b - a..0, (-x) ^ n

Tactic:
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonpos <| ?_) rfl

Result:
a b : ℝ
n : ℕ
hab : b < a
x : ℝ
hx : x ∈ [[b - a, 0]]
⊢ x ≤ 0

Proof state:
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
rcases le_or_lt a b with hab | hab

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

case inr
a b : ℝ
n : ℕ
hab : b < a
⊢ ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Proof state:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0 ..b - a, x ^ n = |b - a| ^ (n + 1) / (↑n + 1)

Tactic:
simp [abs_of_nonneg (sub_nonneg.2 hab)]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
hab : a ≤ b
⊢ ∫ (x : ℝ) in 0 ..b - a, |x| ^ n = ∫ (x : ℝ) in 0 ..b - a, x ^ n

Tactic:
refine integral_congr fun x hx => congr_arg₂ Pow.pow (abs_of_nonneg <| ?_) rfl

Result:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ [[0, b - a]]
⊢ 0 ≤ x

Proof state:
a b : ℝ
n : ℕ
hab : a ≤ b
x : ℝ
hx : x ∈ Set.Icc 0 (b - a)
⊢ 0 ≤ x

Tactic:
exact hx.1

Result:
no goals