-- Lean 4 proof step from Mathlib.Algebra.Lie.SemiDirect (goal)
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
⊢ ⁅x, ⁅x_1, x_2⁆⁆ = ⁅⁅x, x_1⁆, x_2⁆ + ⁅x_1, ⁅x, x_2⁆⁆
have 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))
Tactic: simp