-- Module: Mathlib.Algebra.Lie.Extension
Goal:
R : Type u_1
N : Type u_2
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
E : Extension.{u_1, u_4, u_3, u_5} R M L
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)
x y : L
h :
  ∀ (x_1 : L),
    Eq.{u_5 + 1} (α := E.L)
      (↑(({
                toFun := fun (y_1 : L) ↦
                  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 + y) : E.L) ((s : (a : L) → E.L) y_1) : E.L)
                      ((s : (a : L) → E.L) ⁅x + y, y_1⁆ : E.L))
                    ⋯,
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : L) → ↥E.proj.ker)
            x_1) :
        E.L)
      (↑((HAdd.hAdd (α := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
                {
                  toFun := fun (y : L) ↦
                    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))
                      ⋯,
                  map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }
                {
                  toFun := fun (y_1 : L) ↦
                    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) y : E.L) ((s : (a : L) → E.L) y_1) : E.L)
                        ((s : (a : L) → E.L) ⁅y, y_1⁆ : E.L))
                      ⋯,
                  map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker } :
              (a : L) → ↥E.proj.ker)
            x_1) :
        E.L)
⊢ {
      toFun := fun (y_1 : L) ↦
        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 + y) : E.L) ((s : (a : L) → E.L) y_1) : E.L)
            ((s : (a : L) → E.L) ⁅x + y, y_1⁆ : E.L))
          ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker)
      {
        toFun := fun (y : L) ↦
          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))
            ⋯,
        map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }
      {
        toFun := fun (y_1 : L) ↦
          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) y : E.L) ((s : (a : L) → E.L) y_1) : E.L)
              ((s : (a : L) → E.L) ⁅y, y_1⁆ : E.L))
            ⋯,
        map_add' := ⋯, map_smul' := ⋯ : LinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) L ↥E.proj.ker }

Tactic:
ext