∀ (R : Type u_1) (A : Type u_2) (L : Type u_4) (M : Type u_3) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] [inst_5 : AddCommGroup M] [inst_6 : Module R M]
  [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] (a₁ : A) (l₁ : L) (a₂ : A) (l₂ : L)
  (x_1 y_1 : TensorProduct R A M),
  ((LieAlgebra.ExtendScalars.bracket'✝ R A L M) (a₁ ⊗ₜ[R] l₁))
        (((LieAlgebra.ExtendScalars.bracket'✝¹ R A L M) (a₂ ⊗ₜ[R] l₂)) x_1) =
      ((LieAlgebra.ExtendScalars.bracket'✝² R A L M)
            (((LieAlgebra.ExtendScalars.bracket'✝³ R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
          x_1 +
        ((LieAlgebra.ExtendScalars.bracket'✝⁴ R A L M) (a₂ ⊗ₜ[R] l₂))
          (((LieAlgebra.ExtendScalars.bracket'✝⁵ R A L M) (a₁ ⊗ₜ[R] l₁)) x_1) →
    ((LieAlgebra.ExtendScalars.bracket'✝⁶ R A L M) (a₁ ⊗ₜ[R] l₁))
          (((LieAlgebra.ExtendScalars.bracket'✝⁷ R A L M) (a₂ ⊗ₜ[R] l₂)) y_1) =
        ((LieAlgebra.ExtendScalars.bracket'✝⁸ R A L M)
              (((LieAlgebra.ExtendScalars.bracket'✝⁹ R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
            y_1 +
          ((LieAlgebra.ExtendScalars.bracket'✝¹⁰ R A L M) (a₂ ⊗ₜ[R] l₂))
            (((LieAlgebra.ExtendScalars.bracket'✝¹¹ R A L M) (a₁ ⊗ₜ[R] l₁)) y_1) →
      ((LieAlgebra.ExtendScalars.bracket'✝¹² R A L M) (a₁ ⊗ₜ[R] l₁))
          (((LieAlgebra.ExtendScalars.bracket'✝¹³ R A L M) (a₂ ⊗ₜ[R] l₂)) (x_1 + y_1)) =
        ((LieAlgebra.ExtendScalars.bracket'✝¹⁴ R A L M)
              (((LieAlgebra.ExtendScalars.bracket'✝¹⁵ R A L L) (a₁ ⊗ₜ[R] l₁)) (a₂ ⊗ₜ[R] l₂)))
            (x_1 + y_1) +
          ((LieAlgebra.ExtendScalars.bracket'✝¹⁶ R A L M) (a₂ ⊗ₜ[R] l₂))
            (((LieAlgebra.ExtendScalars.bracket'✝¹⁷ R A L M) (a₁ ⊗ₜ[R] l₁)) (x_1 + y_1))