-- Module: Mathlib.Algebra.Lie.Extension
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
s₁ s₂ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L E.L
hs₁ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₁ : (a : L) → E.L)
hs₂ : LeftInverse.{u_3 + 1, u_5 + 1} (α := L) (β := E.L) (⇑E.proj : (a : E.L) → L) (⇑s₂ : (a : L) → E.L)
x y : L
s : (b : L) → E.L
hs : ∀ (b : L), (E.proj : (a : E.L) → L) (s b) = b
this :
  ∀ {s' : L → E.L} (h : LeftInverse (⇑E.proj : (a : E.L) → L) s'),
    ⁅s x, s' y⁆ = ⁅s' x, s' y⁆ + (⁅s x, s y⁆ - ⁅s' x, s y⁆)
a :
  HAdd.hAdd (α := E.L) (Bracket.bracket (L := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₁ : (a : L) → E.L) y) : E.L)
            (HSub.hSub (β := E.L) ⁅s x, s y⁆ (-⁅s y, (s₁ : (a : L) → E.L) x⁆ : E.L)) -
          HAdd.hAdd (α := E.L)
            (Bracket.bracket (L := E.L) ((s₂ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) y) : E.L)
            (HSub.hSub (β := E.L) ⁅s x, s y⁆ (-⁅s y, (s₂ : (a : L) → E.L) x⁆ : E.L)) -
        HSub.hSub (α := E.L) (β := E.L) (⁅s y, (s₁ : (a : L) → E.L) x⁆ : E.L) (⁅s y, (s₂ : (a : L) → E.L) x⁆ : E.L) -
      HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L) =
    HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₁ : (a : L) → E.L) y) : E.L)
        ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L) -
      HSub.hSub (α := E.L) (β := E.L)
        (Bracket.bracket (L := E.L) ((s₂ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) y) : E.L)
        ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L)
⊢ HSub.hSub (β := M)
      (HSub.hSub (α := M) (β := M)
        (Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) (s x) : L)
            ((E.toKer.symm : (a : ↥E.proj.ker) → M)
              (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) y : E.L) ((s₂ : (a : L) → E.L) y : E.L)) ⋯)) :
          M)
        (Bracket.bracket.{u_3, u_4} (L := L) ((E.proj : (a : E.L) → L) (s y) : L)
            ((E.toKer.symm : (a : ↥E.proj.ker) → M)
              (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
                (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L)) ⋯)) :
          M))
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L) ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L))
            ⋯) :
        M) =
    HSub.hSub (α := M) (β := M)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₁ : (a : L) → E.L) y) : E.L)
              ((s₁ : (a : L) → E.L) ⁅x, y⁆ : E.L))
            ⋯) :
        M)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L)
              (Bracket.bracket (L := E.L) ((s₂ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) y) : E.L)
              ((s₂ : (a : L) → E.L) ⁅x, y⁆ : E.L))
            ⋯) :
        M)

Tactic:
simp only [← EmbeddingLike.apply_eq_iff_eq E.toKer, ringModuleOf_bracket_proj,
    LieEquiv.apply_symm_apply, map_sub, Subtype.ext_iff, AddSubgroupClass.coe_sub,
    LieSubmodule.coe_bracket, lie_sub, this hs₁, this hs₂, ← lie_skew (s₁ x) (s y),
    ← lie_skew (s₂ x) (s y)]

Premises used: AddSubgroupClass.coe_sub, map_sub, EmbeddingLike.apply_eq_iff_eq, LieEquiv.apply_symm_apply, lie_skew, Subtype.ext_iff, LieAlgebra.Extension.toKer, LieSubmodule.coe_bracket, lie_sub, LieAlgebra.Extension.ringModuleOf_bracket_proj, DFunLike.coe