-- Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
n : ℕ
F : Type u_1
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : Preorder F
inst_5 : MeasureSpace F
inst_6 : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord :
  ∀ (x y : F),
    LE.le (α := Fin (n + 1) → ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) x : Fin (n + 1) → ℝ)
        ((eL : (a : F) → Fin (n + 1) → ℝ) y : Fin (n + 1) → ℝ) ↔
      x ≤ y
he_vol : MeasurePreserving (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ) volume volume
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : s.Countable
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF :
  ∀ (x : F),
    DF x =
      ∑ i : Fin (n + 1),
        (f' i x : (a : F) → E)
          ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F)
Hi : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding (α := F) (β := Fin (n + 1) → ℝ) (⇑eL : (a : F) → Fin (n + 1) → ℝ)
hIcc :
  Set.preimage (β := Fin (n + 1) → ℝ) ((⇑eL : (a : F) → Fin (n + 1) → ℝ) : (a : F) → Fin (n + 1) → ℝ)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ)) =
    Set.Icc a b
hIcc' :
  Eq (α := Set (Fin (n + 1) → ℝ))
    (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b) : Set (Fin (n + 1) → ℝ))
    ((⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' Set.Icc a b : Set (Fin (n + 1) → ℝ))
⊢ Eq.{u + 1} (α := E)
    (@integral (Fin (n + 1) → ℝ) _ _ _ (MeasureSpace.toMeasurableSpace : MeasurableSpace (Fin (n + 1) → ℝ))
      (Measure.restrict volume (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) b)) :
        Measure (Fin (n + 1) → ℝ))
      fun (x : Fin (n + 1) → ℝ) ↦
      (∑ i : Fin (n + 1),
          (f' i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x) : (a : F) → E)
            ((eL.symm : (a : Fin (n + 1) → ℝ) → F) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) i 1) : F) :
        E))
    (∑ i : Fin (n + 1),
      HSub.hSub (α := E)
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a ∘ i.succAbove)
              ((eL : (a : F) → Fin (n + 1) → ℝ) b ∘ i.succAbove)))
          fun (x : Fin n → ℝ) ↦
          f i
            ((eL.symm : (a : Fin (n + 1) → ℝ) → F)
              (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) b i) x)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
          (Measure.restrict volume
            (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a ∘ i.succAbove)
              ((eL : (a : F) → Fin (n + 1) → ℝ) b ∘ i.succAbove)))
          fun (x : Fin n → ℝ) ↦
          f i
            ((eL.symm : (a : Fin (n + 1) → ℝ) → F)
              (i.insertNth (α := fun (a : Fin (n + 1)) ↦ ℝ) ((eL : (a : F) → Fin (n + 1) → ℝ) a i) x))))

Tactic:
integral_divergence_of_hasFDerivAt_off_countable' (eL a) (eL b)
        ((he_ord _ _).2 hle) (fun i x => f i (eL.symm x))
        (fun i x => f' i (eL.symm x) ∘L (eL.symm : ℝⁿ⁺¹ →L[ℝ] F)) (eL.symm ⁻¹' s)
        (hs.preimage eL.symm.injective) ?_ ?_ ?_

Premises used: ContinuousLinearMap.comp, Iff.mpr, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.injective, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', Set.preimage, Set.Countable.preimage, DFunLike.coe, ContinuousLinearEquiv.toContinuousLinearMap