a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, x ^ 1) = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)
⊢ (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
have := @integral_pow a b 1
a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
⊢ (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, x ^ 1) = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)
⊢ (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
norm_num at this
no goals
a b : ℝ
n : ℕ
this : (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
⊢ (∫ (x : ℝ) in a..b, x) = (b ^ 2 - a ^ 2) / 2
exact this