-- Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
theorem integral_divergence_of_hasFDerivWithinAt_off_countable_of_equiv {F : Type*}
    [NormedAddCommGroup F] [NormedSpace ℝ F] [PartialOrder F] [MeasureSpace F] [BorelSpace F]
    (eL : F ≃L[ℝ] ℝⁿ⁺¹) (he_ord : ∀ x y, eL x ≤ eL y ↔ x ≤ y)
    (he_vol : MeasurePreserving eL 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, ContinuousOn (f i) (Icc a b))
    (Hd : ∀ x ∈ interior (Icc a b) \ s, ∀ (i), HasFDerivAt (f i) (f' i x) x) (DF : F → E)
    (hDF : ∀ x, DF x = ∑ i, f' i x (eL.symm <| e i)) (Hi : IntegrableOn DF (Icc a b)) :
    ∫ x in Icc a b, DF x =
      ∑ i : Fin (n + 1),
        ((∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),
            f i (eL.symm <| i.insertNth (eL b i) x)) -
          ∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),
            f i (eL.symm <| i.insertNth (eL a i) x)) :=
  have he_emb : MeasurableEmbedding eL := eL.toHomeomorph.measurableEmbedding
  have hIcc : eL ⁻¹' Icc (eL a) (eL b) = Icc a b

Proof state:
case refine_3
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) 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) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ IntegrableOn (fun x => ∑ i : Fin (n + 1), ((fun i x => (f' i (eL.symm x)).comp ↑eL.symm) i x) (e i))
    (Set.Icc (eL a) (eL b)) volume

Tactic:
rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]

Result:
case refine_3
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) 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) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ IntegrableOn ((fun x => ∑ i : Fin (n + 1), ((fun i x => (f' i (eL.symm x)).comp ↑eL.symm) i x) (e i)) ∘ ⇑eL)
    (Set.Icc a b) volume

Proof state:
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) 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) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ ∫ (x : Fin (n + 1) → ℝ) in Set.Icc (eL a) (eL b), ∑ i : Fin (n + 1), (f' i (eL.symm x)) (eL.symm (e i)) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),
          f i (eL.symm (i.insertNth (eL b i) x))) -
        ∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm (i.insertNth (eL a i) x)))

Tactic:
refine integral_divergence_of_hasFDerivWithinAt_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) ?_ ?_ ?_

Result:
case refine_1
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) 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) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ ∀ (i : Fin (n + 1)), ContinuousOn ((fun i x => f i (eL.symm x)) i) (Set.Icc (eL a) (eL b))

case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) 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) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s,
    ∀ (i : Fin (n + 1)),
      HasFDerivAt ((fun i x => f i (eL.symm x)) i) ((fun i x => (f' i (eL.symm x)).comp ↑eL.symm) i x) x

case refine_3
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y
he_vol : MeasurePreserving (⇑eL) 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) (eL.symm (e i))
Hi : IntegrableOn DF (Set.Icc a b) volume
he_emb : MeasurableEmbedding ⇑eL
hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b
hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
⊢ IntegrableOn (fun x => ∑ i : Fin (n + 1), ((fun i x => (f' i (eL.symm x)).comp ↑eL.symm) i x) (e i))
    (Set.Icc (eL a) (eL b)) volume