-- 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)
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)
rw₁ :
  ⁅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))⁆ =
    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))⁆
rw₂ :
  ⁅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,
        (E.toKer : (a : M) → ↥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))⁆
⊢ (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₃ : ⁅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,
      (E.toKer : (a : M) → ↥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,
      ⁅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⁆⁆
Tactic: rw [← map_add, EquivLike.apply_eq_iff_eq, LieEquiv.apply_symm_apply, LieEquiv.apply_symm_apply,
      leibniz_lie, aux]