-- 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
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 x_1 : L
rw :
  Eq.{u_4 + 1} (α := 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 + x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x + x_1) : 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 : E.L) ((s₂ : (a : L) → E.L) x : E.L)) ⋯ +
          Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
            (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
      M)
rw₁ :
  Eq.{u_4 + 1} (α := 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 + x_1) : E.L)
            ((s₂ : (a : L) → E.L) (x + x_1) : 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 : E.L) ((s₂ : (a : L) → E.L) x : E.L) +
            HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L))
          ⋯) :
      M)
rw₂ :
  Subtype.mk (p := fun (x : E.L) ↦ x ∈ E.proj.ker)
      (HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x + x_1) : E.L) ((s₂ : (a : L) → E.L) (x + x_1) : E.L))
      ⋯ =
    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) +
        HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L))
      ⋯
rw₃ :
  HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) (x + x_1) : E.L) ((s₂ : (a : L) → E.L) (x + x_1) : E.L) =
    HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L) +
      HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.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) (x + x_1) : E.L) ((s₂ : (a : L) → E.L) (x + x_1) : E.L))
        ⋯) =
    HAdd.hAdd (α := 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) ((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_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)) ⋯) :
        M)
have rw₄ : HSub.hSub (β := E.L) (HAdd.hAdd (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₁ : (a : L) → E.L) x_1 : E.L))
    ((s₂ : (a : L) → E.L) (x + x_1) : E.L) =
  HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x : E.L) ((s₂ : (a : L) → E.L) x : E.L) +
    HSub.hSub (α := E.L) (β := E.L) ((s₁ : (a : L) → E.L) x_1 : E.L) ((s₂ : (a : L) → E.L) x_1 : E.L)
Tactic: rw [← map_add, AddMemClass.mk_add_mk, EquivLike.apply_eq_iff_eq, Subtype.mk_eq_mk, map_add,
      map_add, add_sub_add_comm]