-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y_1 z : L
m n_1 : M
x y : L
f : M →ₗ[R] N
n : M
h :
  HSub.hSub (α := N) (β := N) (⁅x, ⁅y, (f : (a : M) → N) n⁆⁆ : N) (⁅x, (f : (a : M) → N) ⁅y, n⁆⁆ : N) -
      HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) ⁅x, n⁆⁆ : N) ((f : (a : M) → N) ⁅y, ⁅x, n⁆⁆ : N) =
    HSub.hSub (α := N) (β := N) (⁅x, ⁅y, (f : (a : M) → N) n⁆⁆ : N) (⁅y, ⁅x, (f : (a : M) → N) n⁆⁆ : N) -
        HSub.hSub (α := N) (β := N) ((f : (a : M) → N) ⁅x, ⁅y, n⁆⁆ : N) ((f : (a : M) → N) ⁅y, ⁅x, n⁆⁆ : N) +
      (HSub.hSub (α := N) (β := N) (⁅y, ⁅x, (f : (a : M) → N) n⁆⁆ : N) (⁅y, (f : (a : M) → N) ⁅x, n⁆⁆ : N) -
        HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) ⁅y, n⁆⁆ : N) ((f : (a : M) → N) ⁅x, ⁅y, n⁆⁆ : N))
⊢ Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N)
                (⁅x,
                    ({
                          toFun := fun (m : M) ↦
                            HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
                          map_add' := ⋯, map_smul' := ⋯ } :
                        (a : M) → N)
                      m⁆ :
                  N)
                (({
                        toFun := fun (m : M) ↦
                          HSub.hSub (α := N) (β := N) (⁅y, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅y, m⁆ : N),
                        map_add' := ⋯, map_smul' := ⋯ } :
                      (a : M) → N)
                    ⁅x, m⁆ :
                  N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅⁅x, y⁆, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅⁅x, y⁆, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N)
                  (⁅y,
                      ({
                            toFun := fun (m : M) ↦
                              HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
                            map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
                          (a : M) → N)
                        m⁆ :
                    N)
                  (({
                          toFun := fun (m : M) ↦
                            HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
                          map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
                        (a : M) → N)
                      ⁅y, m⁆ :
                    N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)

Tactic:
simp only [lie_lie, coe_mk, AddHom.coe_mk, map_sub, add_apply, lie_sub]

Premises used: LinearMap.coe_mk, map_sub, LinearMap.add_apply, lie_sub, AddHom.coe_mk, lie_lie