-- Lean 4 proof step from Mathlib.Geometry.Manifold.GroupLieAlgebra (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
H : Type u_2
inst_1 : TopologicalSpace H
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst_4 : TopologicalSpace G
inst_5 : ChartedSpace H G
inst_6 : Group G
inst_7 : LieGroup I (minSmoothness 𝕜 3) G
v : GroupLieAlgebra I G
M : minSmoothness 𝕜 3 ≠ 0
A : minSmoothness 𝕜 2 + 1 = minSmoothness 𝕜 3
fg : G → TangentBundle I G := fun (g : G) ↦ ⟨g, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun (x : G) ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun (g : G) ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) :=
  (⇑(Equiv.symm (equivTangentBundleProd I G I G)) :
    (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle.{u_1, u_3, u_2, u_4} (I.prod I) (G × G) → TangentBundle I G :=
  tangentMap (I.prod I) I fun (p : G × G) ↦ p.1 * p.2
S₃ : ContMDiff (I.prod I).tangent I.tangent (minSmoothness 𝕜 2) F₃
S : ContMDiff I I.tangent (minSmoothness 𝕜 2) ((F₃ ∘ F₂) ∘ F₁) := ⋯
g : G
e_4 : g = (((F₃ ∘ F₂) ∘ F₁) g).proj (E := TangentSpace I)
⊢ mulInvariantVectorField v g = (((F₃ ∘ F₂) ∘ F₁) g).snd (E := TangentSpace I)
have h : mulInvariantVectorField v g =
  (((mfderiv% fun (p : G × G) ↦ p.1 * p.2)
          (TotalSpace.proj (F := E × E) (E := TangentSpace (I.prod I))
            ((Equiv.symm (equivTangentBundleProd I G I G) :
                (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
              (⟨g, 0⟩, ⟨1, v⟩))) :
        TangentSpace.{u_3, u_1, u_2, u_4} (I.prod I) (M := G × G)
            (TotalSpace.proj (F := E × E) (E := TangentSpace (I.prod I))
              ((Equiv.symm (equivTangentBundleProd I G I G) :
                  (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
                (⟨g, 0⟩, ⟨1, v⟩))) →L[𝕜]
          TangentSpace I
            (HMul.hMul (α := G)
              (TotalSpace.proj (F := E × E) (E := TangentSpace (I.prod I))
                  ((Equiv.symm (equivTangentBundleProd I G I G) :
                      (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
                    (⟨g, 0⟩, ⟨1, v⟩))).1
              (TotalSpace.proj (F := E × E) (E := TangentSpace (I.prod I))
                  ((Equiv.symm (equivTangentBundleProd I G I G) :
                      (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
                    (⟨g, 0⟩, ⟨1, v⟩))).2)) :
      (a :
          TangentSpace (I.prod I)
            (((equivTangentBundleProd I G I G).symm :
                  (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
                (⟨g, 0⟩, ⟨1, v⟩)).proj) →
        TangentSpace I
          ((((equivTangentBundleProd I G I G).symm :
                    (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
                  (⟨g, 0⟩, ⟨1, v⟩)).proj.1 *
            (((equivTangentBundleProd I G I G).symm :
                    (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
                  (⟨g, 0⟩, ⟨1, v⟩)).proj.2))
    (TotalSpace.snd (E := TangentSpace (I.prod I))
      ((Equiv.symm (equivTangentBundleProd I G I G) :
          (a : TangentBundle I G × TangentBundle I G) → TangentBundle (I.prod I) (G × G))
        (⟨g, 0⟩, ⟨1, v⟩)))
Tactic: simp only [comp_apply, tangentMap, F₃, F₂, F₁, fg, fv]