-- Module: Mathlib.Algebra.Lie.Weights.Basic
Goal:
R : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst_3 : AddCommGroup M₁
inst_4 : Module R M₁
inst_5 : LieRingModule L M₁
inst_6 : LieModule R L M₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
inst_11 : AddCommGroup M₃
inst_12 : Module R M₃
inst_13 : LieRingModule L M₃
inst_14 : LieModule R L M₃
g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃
χ₁ χ₂ : R
x : L
t : TensorProduct.{u_2, u_5, u_6} R ↥𝕎(M₁, χ₁, x) ↥𝕎(M₂, χ₂, x)
F : Module.End R M₃ :=
  HSub.hSub (α := Module.End R M₃)
    (((toEnd R L M₃ : LieHom.{u_2, u_3, u_7} R L (Module.End R M₃)) : (a : L) → Module.End R M₃) x : Module.End R M₃)
    (HSMul.hSMul (β := Module.End R M₃) (χ₁ + χ₂) 1)
m₁_1 : M₁
hm₁ : Membership.mem (γ := Submodule R M₁) 𝕎(M₁, χ₁, x) m₁_1
m₂_1 : M₂
hm₂ : Membership.mem (γ := Submodule R M₂) 𝕎(M₂, χ₂, x) m₂_1
f₁ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.rTensor M₂
    (HSub.hSub (α := Module.End R M₁)
      (((toEnd R L M₁ : LieHom.{u_2, u_3, u_5} R L (Module.End R M₁)) : (a : L) → Module.End R M₁) x : Module.End R M₁)
      (HSMul.hSMul (β := Module.End R M₁) χ₁ 1))
f₂ : Module.End R (M₁ ⊗[R] M₂) :=
  LinearMap.lTensor M₁
    (HSub.hSub (α := Module.End R M₂)
      (((toEnd R L M₂ : LieHom.{u_2, u_3, u_6} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
      (HSMul.hSMul (β := Module.End R M₂) χ₂ 1))
m₁ : M₁
m₂ : M₂
a :
  HAdd.hAdd (α := M₃) (β := M₃) ((g : (a : M₁ ⊗[R] M₂) → M₃) (⁅x, m₁⁆ ⊗ₜ[R] m₂) : M₃)
        ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] ⁅x, m₂⁆) : M₃) -
      (HSMul.hSMul (β := M₃) χ₁ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃) +
        HSMul.hSMul (β := M₃) χ₂ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃)) =
    HSub.hSub (α := M₃) ((g : (a : M₁ ⊗[R] M₂) → M₃) (⁅x, m₁⁆ ⊗ₜ[R] m₂) : M₃)
        (HSMul.hSMul (β := M₃) χ₁ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃)) +
      HSub.hSub (α := M₃) ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] ⁅x, m₂⁆) : M₃)
        (HSMul.hSMul (β := M₃) χ₂ ((g : (a : M₁ ⊗[R] M₂) → M₃) (m₁ ⊗ₜ[R] m₂) : M₃))
⊢ Eq.{u_7 + 1} (α := M₃)
    (((((AlgebraTensorModule.curry (F ∘ₗ (↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃)) : M₁ →ₗ[R] M₂ →ₗ[R] M₃) : (a : M₁) → M₂ →ₗ[R] M₃)
              m₁ :
            M₂ →ₗ[R] M₃) :
          (a : M₂) → M₃)
        m₂ :
      M₃)
    (((((AlgebraTensorModule.curry ((↑g : M₁ ⊗[R] M₂ →ₗ[R] M₃) ∘ₗ (f₁ + f₂)) : M₁ →ₗ[R] M₂ →ₗ[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₃)
              m₁ :
            M₂ →ₗ[R] M₃) :
          (a : M₂) → M₃)
        m₂ :
      M₃)

Tactic:
simp only [f₁, f₂, F, ← g.map_lie x (m₁ ⊗ₜ m₂), add_smul, sub_tmul, tmul_sub, smul_tmul,
      lie_tmul_right, tmul_smul, toEnd_apply_apply, map_smul, Module.End.one_apply,
      LieModuleHom.coe_toLinearMap, LinearMap.smul_apply, Function.comp_apply, LinearMap.coe_comp,
      LinearMap.rTensor_tmul, map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply,
      LinearMap.lTensor_tmul, AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
      LinearMap.coe_restrictScalars]

Premises used: TensorProduct.smul_tmul, map_sub, LinearMap.smul_apply, LinearMap.rTensor_tmul, LinearMap.add_apply, TensorProduct.tmul_sub, LieModuleHom.coe_toLinearMap, LinearMap.coe_restrictScalars, TensorProduct.tmul_smul, map_add, TensorProduct.AlgebraTensorModule.curry_apply, Module.End.one_apply, TensorProduct.LieModule.lie_tmul_right, TensorProduct.sub_tmul, LieModule.toEnd_apply_apply, add_smul, LinearMap.coe_comp, TensorProduct.curry_apply, LinearMap.sub_apply, Function.comp_apply, TensorProduct.tmul, LieModuleHom.map_lie, LinearMap.lTensor_tmul, map_smul