a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2)) = arctan b - arctan a
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹) = arctan b - arctan a
simp only [← one_div]
case refine'_1
a b : ℝ
n : ℕ
⊢ deriv arctan = fun x => 1 / (1 + x ^ 2)

case refine'_2
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ arctan x

case refine'_3
a b : ℝ
n : ℕ
⊢ Continuous fun x => 1 + x ^ 2

case refine'_4
a b : ℝ
n : ℕ
x : ℝ
⊢ 1 + x ^ 2 ≠ 0
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2)) = arctan b - arctan a
refine' integral_deriv_eq_sub' _ _ _ (continuous_const.div _ fun x => _).continuousOn
no goals
case refine'_1
a b : ℝ
n : ℕ
⊢ deriv arctan = fun x => 1 / (1 + x ^ 2)
norm_num
no goals
case refine'_2
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ arctan x
exact fun _ _ => differentiableAt_arctan _
no goals
case refine'_3
a b : ℝ
n : ℕ
⊢ Continuous fun x => 1 + x ^ 2
continuity
no goals
case refine'_4
a b : ℝ
n : ℕ
x : ℝ
⊢ 1 + x ^ 2 ≠ 0
nlinarith