-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
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
x y : A ⊗[R] L
z : A ⊗[R] M
a₁ : A
l₁ : L
⊢ ∀ (x y : A ⊗[R] L),
    (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
            (a : A ⊗[R] M) → A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) x : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            z) =
        HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                    ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                          A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                        (a : A ⊗[R] L) → A ⊗[R] L)
                      x) :
                  A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              z :
            A ⊗[R] M)
          ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) x : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                z) :
            A ⊗[R] M) →
      (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              z) =
          HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                            A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                          (a : A ⊗[R] L) → A ⊗[R] L)
                        y) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                z :
              A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) y : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                    (a : A ⊗[R] M) → A ⊗[R] M)
                  z) :
              A ⊗[R] M) →
        (((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (x + y) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              z) =
          HAdd.hAdd (α := A ⊗[R] M) (β := A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M)
                      ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (a₁ ⊗ₜ[R] l₁) :
                            A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                          (a : A ⊗[R] L) → A ⊗[R] L)
                        (x + y)) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                z :
              A ⊗[R] M)
            ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (x + y) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                ((((bracket' R A L M : (a : A ⊗[R] L) → A ⊗[R] M →ₗ[A] A ⊗[R] M) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                    (a : A ⊗[R] M) → A ⊗[R] M)
                  z) :
              A ⊗[R] M)

Tactic:
grind [LinearMap.add_apply]

Premises used: LinearMap.add_apply