case h
a b : ℝ
n✝ : ℕ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < ↑n ∨ ↑n ≠ -1 ∧ ¬0 ∈ [[a, b]]

a b : ℝ
n✝ : ℕ
n : ℤ
h : -1 < ↑n ∨ ↑n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, x ^ n) = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
a b : ℝ
n✝ : ℕ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, x ^ n) = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]
no goals
a b : ℝ
n✝ : ℕ
n : ℤ
h : -1 < ↑n ∨ ↑n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ (∫ (x : ℝ) in a..b, x ^ n) = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
exact_mod_cast integral_rpow h
no goals
case h
a b : ℝ
n✝ : ℕ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ ¬0 ∈ [[a, b]]
⊢ -1 < ↑n ∨ ↑n ≠ -1 ∧ ¬0 ∈ [[a, b]]
exact_mod_cast h