-- Module: Mathlib.Geometry.Manifold.GroupLieAlgebra
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)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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:
rw [mfderiv_prod_eq_add_apply ((contMDiff_mul I (minSmoothness 𝕜 3)).mdifferentiableAt M)]

Premises used: contMDiff_mul, minSmoothness, OfNat.ofNat, ContMDiff.mdifferentiableAt, mfderiv_prod_eq_add_apply