-- Module: Mathlib.Algebra.Lie.BaseChange
Goal:
R_1 : Type u_1
A_1 : Type u_2
L_1 : Type u_3
M : Type u_4
inst : CommRing R_1
inst_1 : CommRing A_1
inst_2 : Algebra R_1 A_1
inst_3 : LieRing L_1
inst_4 : LieAlgebra R_1 L_1
inst_5 : AddCommGroup M
inst_6 : Module R_1 M
inst_7 : LieRingModule L_1 M
inst_8 : LieModule R_1 L_1 M
R : Type u_5
A : Type u_6
B : Type u_7
L : Type u_8
L' : Type u_9
inst_9 : CommRing R
inst_10 : CommRing A
inst_11 : Algebra R A
inst_12 : CommRing B
inst_13 : Algebra R B
inst_14 : LieRing L
inst_15 : LieAlgebra R L
inst_16 : LieRing L'
inst_17 : LieAlgebra R L'
f : A →ₐ[R] B
g : L →ₗ⁅R⁆ L'
x y x_1 y_1 : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    (Eq (α := B ⊗[R] L')
          ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
              ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                  (a : A ⊗[R] L) → A ⊗[R] L)
                x) :
            B ⊗[R] L')
          ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                    ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x_1) :
                  B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                (a : B ⊗[R] L') → B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x) :
            B ⊗[R] L') →
        Eq (α := B ⊗[R] L')
            ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  x) :
              B ⊗[R] L')
            ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                      ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y_1) :
                    B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                  (a : B ⊗[R] L') → B ⊗[R] L')
                ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x) :
              B ⊗[R] L') →
          Eq (α := B ⊗[R] L')
            ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x_1 + y_1) :
                      A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  x) :
              B ⊗[R] L')
            ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                      ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x_1 + y_1)) :
                    B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                  (a : B ⊗[R] L') → B ⊗[R] L')
                ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x) :
              B ⊗[R] L')) →
      (Eq (α := B ⊗[R] L')
            ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  y) :
              B ⊗[R] L')
            ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                      ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x_1) :
                    B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                  (a : B ⊗[R] L') → B ⊗[R] L')
                ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
              B ⊗[R] L') →
          Eq (α := B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                  ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                      (a : A ⊗[R] L) → A ⊗[R] L)
                    y) :
                B ⊗[R] L')
              ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y_1) :
                      B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                    (a : B ⊗[R] L') → B ⊗[R] L')
                  ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
                B ⊗[R] L') →
            Eq (α := B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                  ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x_1 + y_1) :
                        A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                      (a : A ⊗[R] L) → A ⊗[R] L)
                    y) :
                B ⊗[R] L')
              ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x_1 + y_1)) :
                      B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                    (a : B ⊗[R] L') → B ⊗[R] L')
                  ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y) :
                B ⊗[R] L')) →
        Eq (α := B ⊗[R] L')
            ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) x_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                    (a : A ⊗[R] L) → A ⊗[R] L)
                  (x + y)) :
              B ⊗[R] L')
            ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                      ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') x_1) :
                    B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                  (a : B ⊗[R] L') → B ⊗[R] L')
                ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x + y)) :
              B ⊗[R] L') →
          Eq (α := B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                  ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) y_1 : A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                      (a : A ⊗[R] L) → A ⊗[R] L)
                    (x + y)) :
                B ⊗[R] L')
              ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') y_1) :
                      B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                    (a : B ⊗[R] L') → B ⊗[R] L')
                  ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x + y)) :
                B ⊗[R] L') →
            Eq (α := B ⊗[R] L')
              ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L')
                  ((((bracket' R A L L : (a : A ⊗[R] L) → A ⊗[R] L →ₗ[A] A ⊗[R] L) (x_1 + y_1) :
                        A ⊗[R] L →ₗ[A] A ⊗[R] L) :
                      (a : A ⊗[R] L) → A ⊗[R] L)
                    (x + y)) :
                B ⊗[R] L')
              ((((bracket' R B L' L' : (a : B ⊗[R] L') → B ⊗[R] L' →ₗ[B] B ⊗[R] L')
                        ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x_1 + y_1)) :
                      B ⊗[R] L' →ₗ[B] B ⊗[R] L') :
                    (a : B ⊗[R] L') → B ⊗[R] L')
                  ((TensorProduct.map f.toLinearMap (↑g : L →ₗ[R] L') : (a : A ⊗[R] L) → B ⊗[R] L') (x + y)) :
                B ⊗[R] L')

Tactic:
simp_all