-- 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
a₂ : A
l₂ : L
⊢ ∀ (x y : 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) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
              (a : A ⊗[R] M) → A ⊗[R] M)
            x) =
        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)
                      (a₂ ⊗ₜ[R] l₂)) :
                  A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              x :
            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) (a₁ ⊗ₜ[R] l₁) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                x) :
            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) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              y) =
          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)
                        (a₂ ⊗ₜ[R] l₂)) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                y :
              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) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                    (a : A ⊗[R] M) → A ⊗[R] M)
                  y) :
              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) (a₂ ⊗ₜ[R] l₂) : A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                (a : A ⊗[R] M) → A ⊗[R] M)
              (x + y)) =
          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)
                        (a₂ ⊗ₜ[R] l₂)) :
                    A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                  (a : A ⊗[R] M) → A ⊗[R] M)
                (x + y) :
              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) (a₁ ⊗ₜ[R] l₁) :
                      A ⊗[R] M →ₗ[A] A ⊗[R] M) :
                    (a : A ⊗[R] M) → A ⊗[R] M)
                  (x + y)) :
              A ⊗[R] M)

Tactic:
grind