-- 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 :
  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)
⊢ Eq.{u_4 + 1} (α := M)
    (((((↑((d₁₂ R L M : (a : oneCochain R L M) → ↥(twoCochain R L M)) (E.oneCochainOfTwoSplitting hs₁ hs₂)) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)
    (((((↑((↑(E.twoCocycleOf hs₁) : ↥(twoCochain R L M)) - (↑(E.twoCocycleOf hs₂) : ↥(twoCochain R L M))) :
                  L →ₗ[R] L →ₗ[R] M) :
                (a : L) → L →ₗ[R] M)
              x :
            L →ₗ[R] M) :
          (a : L) → M)
        y :
      M)

Tactic:
simp only [d₁₂_apply_coe_apply_apply, oneCochainOfTwoSplitting_apply, AddSubgroupClass.coe_sub,
    twoCocycleOf_coe_coe, LinearMap.sub_apply, LinearMap.compr₂_apply, LinearMap.coe_mk,
    AddHom.coe_mk, LinearEquiv.coe_coe, LieEquiv.coe_toLinearEquiv]

Premises used: AddSubgroupClass.coe_sub, LinearMap.coe_mk, LinearMap.compr₂_apply, LieModule.Cohomology.d₁₂_apply_coe_apply_apply, LinearMap.sub_apply, AddHom.coe_mk, LieAlgebra.Extension.twoCocycleOf_coe_coe, LinearEquiv.coe_coe, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieEquiv.coe_toLinearEquiv