-- 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
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⁆)
⊢ HSub.hSub (β := M)
      (HSub.hSub (α := M) (β := M)
        (⁅x,
            (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)
        (⁅y,
            (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)
have a : 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)) sorry)) :
        M)
      (⁅y,
          (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)) sorry)⁆ :
        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)) sorry) :
      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))
          sorry) :
      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))
          sorry) :
      M)
Tactic: nth_rw 1 [← hs x]