∀ {R : Type u_2} {L : Type u_4} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) {s : L →ₗ[R] E.L},
  Function.LeftInverse ⇑E.proj ⇑s → ∀ (x y x_1 x_2 : L), ⁅s (x + y), s (x_1 + x_2)⁆ - s ⁅x + y, x_1 + x_2⁆ ∈ E.proj.ker