-- 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
inst_5 : IsLieAbelian M
E : Extension.{u_1, u_4, u_3, u_5} R M L
x y : L
m : M
h : HasRightInverse.{u_5 + 1, u_3 + 1} (α := E.L) (β := L) (⇑E.proj : (a : E.L) → L) := ⋯
aux :
  ∀ (z : ↥E.proj.ker),
    Eq (α := ↥E.proj.ker)
      (⁅⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
            Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y⁆,
          z⁆ :
        ↥E.proj.ker)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h ⁅x, y⁆, z⁆ :
        ↥E.proj.ker)
⊢ (E.toKer.symm : (a : ↥E.proj.ker) → M)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
          (E.toKer : (a : M) → ↥E.proj.ker)
            ((E.toKer.symm : (a : ↥E.proj.ker) → M)
              (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y,
                  (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                ↥E.proj.ker))⁆ :
        ↥E.proj.ker) =
    HAdd.hAdd (α := M) (β := M)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h ⁅x, y⁆,
              (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
            ↥E.proj.ker) :
        M)
      ((E.toKer.symm : (a : ↥E.proj.ker) → M)
          (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y,
              (E.toKer : (a : M) → ↥E.proj.ker)
                ((E.toKer.symm : (a : ↥E.proj.ker) → M)
                  (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
                      (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                    ↥E.proj.ker))⁆ :
            ↥E.proj.ker) :
        M)
have rw : Eq.{u_4 + 1} (α := M)
  ((E.toKer.symm : (a : ↥E.proj.ker) → M)
      (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
          (E.toKer : (a : M) → ↥E.proj.ker)
            ((E.toKer.symm : (a : ↥E.proj.ker) → M)
              (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y,
                  (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                ↥E.proj.ker))⁆ :
        ↥E.proj.ker) :
    M)
  ((E.toKer.symm : (a : ↥E.proj.ker) → M)
      (HAdd.hAdd (α := ↥E.proj.ker)
        ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h ⁅x, y⁆,
          (E.toKer : (a : M) → ↥E.proj.ker) m⁆
        ⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h y,
          (E.toKer : (a : M) → ↥E.proj.ker)
            ((E.toKer.symm : (a : ↥E.proj.ker) → M)
              (⁅Exists.choose (p := fun (finv : L → E.L) ↦ RightInverse finv (⇑E.proj : (a : E.L) → L)) h x,
                  (E.toKer : (a : M) → ↥E.proj.ker) m⁆ :
                ↥E.proj.ker))⁆) :
    M)
Tactic: rw [← map_add, EquivLike.apply_eq_iff_eq, LieEquiv.apply_symm_apply, LieEquiv.apply_symm_apply,
      leibniz_lie, aux]