-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing M
inst_4 : LieAlgebra R M
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
y : M
z : E.L
x : M
hx :
  ((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x =
    Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
        ((E.proj : (a : E.L) → L) z) -
      z
rw :
  Eq.{u_4 + 1} (α := M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M)
        (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z),
            (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
          ↥E.proj.ker) :
      M)
    ((E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) : M)
rw₁ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z),
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
rw₂ :
  HSub.hSub (α := ↥E.proj.ker) (β := ↥E.proj.ker)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z),
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
        ↥E.proj.ker)
      (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker) =
    0
rw₃ :
  Eq (α := ↥E.proj.ker)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      ↥E.proj.ker)
    (0 : ↥E.proj.ker)
rw₄ :
  Eq.{u_5 + 1} (α := E.L)
    (↑⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
              ((E.proj : (a : E.L) → L) z) -
            z,
          (E.toKer : (a : M) → ↥E.proj.ker) y⁆ :
      E.L)
    (↑0 : E.L)
rw₅ :
  Eq (α := E.L)
    ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
          ((E.proj : (a : E.L) → L) z) -
        z,
      (↑((E.toKer : (a : M) → ↥E.proj.ker) y) : E.L)⁆
    (↑0 : E.L)
rw₆ :
  Eq (α := E.L)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.incl : (a : M) → E.L) y⁆ :
      E.L)
    ((↑0 : E.L) : E.L)
rw₇ :
  Eq (α := E.L)
    (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) ⋯
            ((E.proj : (a : E.L) → L) z) -
          z,
        (E.incl : (a : M) → E.L) y⁆ :
      E.L)
    (0 : E.L)
⊢ Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) z : L) y =
    (E.toKer.symm : (a : ↥E.proj.ker) → M) (⁅z, (E.toKer : (a : M) → ↥E.proj.ker) y⁆ : ↥E.proj.ker)
have rw₈ : Eq.{u_5 + 1} (α := E.L)
  (Bracket.bracket (L := E.L) (((↑E.incl : M →ₗ[R] E.L) : (a : M) → E.L) x : E.L) ((E.incl : (a : M) → E.L) y) : E.L)
  (0 : E.L)
Tactic: rw [ringModuleOf_bracket, EmbeddingLike.apply_eq_iff_eq, ← sub_eq_zero, ← sub_lie,
    Subtype.ext_iff, LieSubmodule.coe_bracket, lie_toKer_apply, ZeroMemClass.coe_zero, ← hx,
    LieHom.coe_toLinearMap, ← LieHom.map_lie, trivial_lie_zero M M x y, map_zero]