-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : ∀ (x : M), IsTopologicalAddGroup.{u_6} (V x)
inst_13 : ∀ (x : M), ContinuousSMul.{u_1, u_6} 𝕜 (V x)
inst_14 : FiberBundle F V
ι : Type u_7
s : Finset ι
u : Set M
cov : ι → ((x : M) → V x) → (x : M) → ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)
h : ∀ (i : ι), IsCovariantDerivativeOn F (V := V) (cov i) u
f : ι → M → 𝕜
hf : Eq (α := M → 𝕜) (∑ i ∈ s, f i) 1
σ : (x : M) → V x
g : M → 𝕜
x : M
hσ : MDiffAt (T% σ) x
hg : MDiffAt g x
hx : x ∈ u
rw :
  HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
      (∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x)
      (∑ x_1 ∈ s,
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f x_1 x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
        (∑ i ∈ s, f i x • cov i σ x) +
      HSMul.hSMul (α := 𝕜) (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
        ((∑ i ∈ s, f i) x) (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
rw₁ :
  HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
      (∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x)
      (∑ x_1 ∈ s,
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f x_1 x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))) =
    ∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x +
      HSMul.hSMul (α := 𝕜) (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
        ((∑ i ∈ s, f i) x) (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
rw₂ :
  HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
      (∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x)
      (∑ x_1 ∈ s,
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f x_1 x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))) =
    ∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x +
      HSMul.hSMul (α := 𝕜) (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
        (∑ c ∈ s, f c x) (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
⊢ ∑ i ∈ s,
      (g x • f i x • cov i σ x +
        HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
          (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))) =
    HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (g x)
        (∑ i ∈ s, f i x • cov i σ x) +
      HSMul.hSMul (α := 𝕜) (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
        ((∑ i ∈ s, f i) x) (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))
have rw₃ : HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x)
    (∑ x_1 ∈ s,
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f x_1 x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x))) =
  HAdd.hAdd (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ x_1 ∈ s, g x • f x_1 x • cov x_1 σ x)
    (∑ i ∈ s,
      HSMul.hSMul (β := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x)) (f i x)
        (ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)))
Tactic: rw [Finset.sum_add_distrib, Finset.smul_sum, Finset.sum_apply, Finset.sum_smul]