-- 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
calc :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) (TangentSpace I x) (V x))
    (∑ i ∈ s, f i x • cov i (g • σ) 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))))
calc₁ :
  ∑ 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))
⊢ ∑ i ∈ s, f i x • cov i (g • σ) 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) +
      ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)
have calc₂ : 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)) =
  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) +
    ContinuousLinearMap.smulRight (S := 𝕜) (d% g x) (σ x)
Tactic: calc ∑ i ∈ s, f i x • cov i (g • σ) x
      _ = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)) := by
          congr! 1 with i hi
          rw [(h i).leibniz hσ hg]
          simp [mvfderiv]
          module
      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) := by
          rw [Finset.sum_add_distrib, Finset.smul_sum, Finset.sum_apply, Finset.sum_smul]
      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x) := by rw [hf]; simp