Module: Mathlib.Geometry.Manifold.GroupLieAlgebra

Goal state before:
pp: case e'_5
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : 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, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun g ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I fun p ↦ 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₁) := ContMDiff.comp (ContMDiff.comp S₃ S₂) S₁
g : G
e_4✝ : g = (((F₃ ∘ F₂) ∘ F₁) g).proj
⊢ mulInvariantVectorField v g =
    ((mfderiv% fun p ↦ p.1 * p.2) ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj)
      ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).snd

Tactic:
rw [mfderiv_prod_eq_add_apply ((contMDiff_mul I (minSmoothness 𝕜 3)).mdifferentiableAt M)]

Goal state after:
case e'_5
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Group G
inst✝ : 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, 0⟩
sfg : ContMDiff I I.tangent (minSmoothness 𝕜 2) fg
fv : G → TangentBundle I G := fun x ↦ ⟨1, v⟩
sfv : ContMDiff I I.tangent (minSmoothness 𝕜 2) fv
F₁ : G → TangentBundle I G × TangentBundle I G := fun g ↦ (fg g, fv g)
S₁ : ContMDiff I (I.tangent.prod I.tangent) (minSmoothness 𝕜 2) F₁
F₂ : TangentBundle I G × TangentBundle I G → TangentBundle (I.prod I) (G × G) := ⇑(equivTangentBundleProd I G I G).symm
S₂ : ContMDiff (I.tangent.prod I.tangent) (I.prod I).tangent (minSmoothness 𝕜 2) F₂
F₃ : TangentBundle (I.prod I) (G × G) → TangentBundle I G := tangentMap (I.prod I) I fun p ↦ 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₁) := ContMDiff.comp (ContMDiff.comp S₃ S₂) S₁
g : G
e_4✝ : g = (((F₃ ∘ F₂) ∘ F₁) g).proj
⊢ mulInvariantVectorField v g =
    ((mfderiv% fun z ↦
            (z, ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.2).1 *
              (z, ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.2).2)
          ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.1)
        ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).snd.1 +
      ((mfderiv% fun z ↦
            (((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.1, z).1 *
              (((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.1, z).2)
          ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).proj.2)
        ((equivTangentBundleProd I G I G).symm (⟨g, 0⟩, ⟨1, v⟩)).snd.2