-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Deriv (goal)
Goal:
E : Type u_5
F₁ : Type u_9
F₂ : Type u_10
F₃ : Type u_11
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace ℝ F₁
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace ℝ F₂
inst_7 : NormedAddCommGroup F₃
inst_8 : NormedSpace ℝ F₃
inst_9 : MeasurableSpace E
μ : Measure E
inst_10 : BorelSpace E
inst_11 : μ.IsAddHaarMeasure
f : 𝓢(E, F₁)
g : 𝓢(E, F₂)
L : F₁ →L[ℝ] F₂ →L[ℝ] F₃
rw :
  Eq.{u_11 + 1} (α := F₃)
    (∑ i : Fin (Module.finrank ℝ E),
      ∫ (a : E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) a) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
                (a : E) → F₂)
              a :
            F₂) ∂μ)
    (∑ i : Fin (Module.finrank ℝ E),
      ∫ (a : E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
                    (a : E) → F₁)
                  a) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) a : F₂) ∂μ)
hf :
  ∀ (i : Fin (Module.finrank ℝ E)),
    Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
      Integrable.{u_11, u_5} (ε := F₃)
        (fun (x : E) ↦
          (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                  ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                        (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                          f) :
                      (a : E) → F₁)
                    x) :
                F₂ →L[ℝ] F₃) :
              (a : F₂) → F₃)
            ((g : (a : E) → F₂) x : F₂))
        μ
⊢ Eq.{u_11 + 1} (α := F₃)
    (∫ (x : E),
      ∑ x_1 : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) x_1 : E) g) :
                (a : E) → F₂)
              x :
            F₂) ∂μ)
    (∫ (x : E),
      ∑ c : Fin (Module.finrank ℝ E),
        (((L : (a : F₁) → F₂ →L[ℝ] F₃)
                ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E)
                      (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) c : E) f) :
                    (a : E) → F₁)
                  x) :
              F₂ →L[ℝ] F₃) :
            (a : F₂) → F₃)
          ((g : (a : E) → F₂) x : F₂) ∂μ)
have hf₁ : ∀ (i : Fin (Module.finrank ℝ E)),
  Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i →
    Integrable.{u_11, u_5} (ε := F₃)
      (fun (x : E) ↦
        (((L : (a : F₁) → F₂ →L[ℝ] F₃) ((f : (a : E) → F₁) x) : F₂ →L[ℝ] F₃) : (a : F₂) → F₃)
          ((lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E)
                  (lineDerivOp (V := E) ((stdOrthonormalBasis ℝ E : (a : Fin (Module.finrank ℝ E)) → E) i : E) g) :
                (a : E) → F₂)
              x :
            F₂))
      μ
Tactic: rw [MeasureTheory.integral_finsetSum, MeasureTheory.integral_finsetSum]