-- Lean 4 proof step from Mathlib.Algebra.Lie.Extension (goal)
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
⊢ {
      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 }
have 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))
                  sorry,
              map_add' := sorry, map_smul' := sorry } :
            (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))
                    sorry,
                map_add' := sorry, map_smul' := sorry : 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))
                    sorry,
                map_add' := sorry, map_smul' := sorry : 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)
Tactic: ext