-- 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 : M
x y : L
f : M →ₗ[R] N
h :
  ∀ (n : M),
    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)
⊢ {
      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' := ⋯ } =
    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 }

Tactic:
ext n