-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
simp :
  HSub.hSub (β := K)
          (HAdd.hAdd (β := K) ⁅x.left, ⁅x_1.left, x_2.left⁆⁆
            (⁅x.left, (((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left⁆ :
              K))
          (⁅x.left, (((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left⁆ :
            K) +
        HSub.hSub (β := K)
          (HAdd.hAdd (β := K)
            (HSub.hSub (α := K) (β := K)
              (⁅x_1.left,
                  (((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left⁆ :
                K)
              (⁅x_2.left,
                  (((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left⁆ :
                K))
            ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K)
                ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) :
              K))
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K)
              ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) :
            K) -
      HSub.hSub (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K)
            ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) :
          K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K)
            ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K) :
          K) =
    ⁅x.left, ⁅x_1.left, x_2.left⁆⁆ - ⁅x_1.left, ⁅x.left, x_2.left⁆⁆ +
              Bracket.bracket (L := K)
                ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)
                x_2.left -
            Bracket.bracket (L := K)
              ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K)
              x_2.left +
          HSub.hSub (α := K) (β := K)
            ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K)
                ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) :
              K)
            ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K)
                ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) :
              K) -
        HSub.hSub (β := K)
          (HAdd.hAdd (β := K)
            (HSub.hSub (α := K) (β := K)
              (⁅x.left,
                  (((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left⁆ :
                K)
              (⁅x_1.left,
                  (((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left⁆ :
                K))
            ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K)
                ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) :
              K))
          ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K)
              ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K) :
            K) +
      (HSub.hSub (β := K)
            (HAdd.hAdd (β := K) ⁅x_1.left, ⁅x.left, x_2.left⁆⁆
              (⁅x_1.left,
                  (((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left⁆ :
                K))
            (⁅x_1.left, (((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left⁆ :
              K) +
          HSub.hSub (β := K)
            (HAdd.hAdd (β := K)
              (HSub.hSub (α := K) (β := K)
                (⁅x.left,
                    (((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left⁆ :
                  K)
                (⁅x_2.left,
                    (((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left⁆ :
                  K))
              ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K)
                  ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) :
                K))
            ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K)
                ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) :
              K) -
        HSub.hSub (α := K) (β := K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K)
              ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) :
            K)
          ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K)
              ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) :
            K))
⊢ ⁅x, ⁅x_1, x_2⁆⁆ = ⁅⁅x, x_1⁆, x_2⁆ + ⁅x_1, ⁅x, x_2⁆⁆

Tactic:
simp