-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DivergenceTheorem (goal)
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) → ℝ))
refine_1 :
  ∀ (i : Fin (n + 1)),
    ContinuousOn.{0, u} (X := Fin (n + 1) → ℝ) (Y := E)
      ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦ f i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x)) i :
        (x : Fin (n + 1) → ℝ) → E)
      (Set.Icc ((eL : (a : F) → Fin (n + 1) → ℝ) a) ((eL : (a : F) → Fin (n + 1) → ℝ) 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))))
have refine_2 : ∀ (x : (i : Fin (n + 1)) → ℝ),
  Membership.mem (γ := Set ((i : Fin (n + 1)) → ℝ))
      ((Set.pi (α := fun (i : Fin (n + 1)) ↦ ℝ) Set.univ fun (i : Fin (n + 1)) ↦
          Set.Ioo ((eL : (a : F) → Fin (n + 1) → ℝ) a i) ((eL : (a : F) → Fin (n + 1) → ℝ) b i)) \
        (⇑eL.symm : (a : Fin (n + 1) → ℝ) → F) ⁻¹' s)
      x →
    ∀ (i : Fin (n + 1)),
      HasFDerivAt.{0, 0, u} (𝕜 := ℝ) (F := E)
        ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦ f i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x)) i)
        ((fun (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ) ↦
            f' i ((eL.symm : (a : Fin (n + 1) → ℝ) → F) x) ∘SL (↑eL.symm : (Fin (n + 1) → ℝ) →L[ℝ] F))
          i x)
        x
Tactic: refine 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) ?_ ?_ ?_