-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f f' : ℝ → E
a b : ℝ
hle : a ≤ b
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f (Set.Icc a b)
Hd : ∀ x ∈ Set.Ioo a b \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
e : ℝ ≃L[ℝ] Fin 1 → ℝ := ContinuousLinearEquiv.symm (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ)
F' : ℝ → ℝ →L[ℝ] E := fun (x : ℝ) ↦ smulRight (S := ℝ) 1 (f' x)
x :
  Eq.{u + 1} (α := E) (∫ (x : ℝ) in a..b, f' x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
x₁ :
  Eq.{u + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Icc a b)) fun (x : ℝ) ↦ f' x)
    (∑ i : Fin 1,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f ((e.symm : (a : Fin 1 → ℝ) → ℝ) (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f
            ((e.symm : (a : Fin 1 → ℝ) → ℝ)
              (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) a i) x))))
x₂ :
  ∑ i : Fin 1,
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f ((e.symm : (a : Fin 1 → ℝ) → ℝ) (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((e : (a : ℝ) → Fin 1 → ℝ) a ∘ i.succAbove) ((e : (a : ℝ) → Fin 1 → ℝ) b ∘ i.succAbove)))
          fun (x : Fin 0 → ℝ) ↦
          f
            ((e.symm : (a : Fin 1 → ℝ) → ℝ)
              (i.insertNth (α := fun (a : Fin 1) ↦ ℝ) ((e : (a : ℝ) → Fin 1 → ℝ) a i) x))) =
    f b - f a
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
calc
    ∫ x in a..b, f' x = ∫ x in Icc a b, f' x := by
      rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]
    _ = ∑ i : Fin 1,
          ((∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
              f (e.symm <| i.insertNth (e b i) x)) -
            ∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),
              f (e.symm <| i.insertNth (e a i) x)) := by
      simp only [← interior_Icc] at Hd
      refine
        integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f)
          (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_
      · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le
      · exact (volume_preserving_funUnique (Fin 1) ℝ).symm _
      · simp [F', e]
      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
        exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm
    _ = f b - f a := by
      simp [e, Subsingleton.elim (const (Fin 0) _) isEmptyElim, volume_pi,
        Measure.pi_of_empty fun _ : Fin 0 ↦ _]

Premises used: Set.Icc, OfNat.ofNat, Fin