-- Lean 4 proof step from Mathlib.Algebra.Lie.Submodule (goal)
Goal:
R : Type u
L : Type v
L' : Type w₂
M : Type w
M' : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieRing L'
inst_3 : LieAlgebra R L'
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : AddCommGroup M'
inst_8 : Module R M'
inst_9 : LieRingModule L M'
f : M →ₗ⁅R,L⁆ M'
N N₂ : LieSubmodule R L M
N' : LieSubmodule R L M'
hf : Function.Injective.{w + 1, w₁ + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : L
m : M
hm : m ∈ N
⊢ Eq (α := ↥(map f N))
    (AddHom.toFun
        (LinearMap.toAddHom
            ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                  ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
              LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
          AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
        ⁅x, Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm⁆ :
      ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
    (⁅x,
        AddHom.toFun
          (LinearMap.toAddHom
              ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                  LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                    ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                  ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
            AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
          (Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm)⁆ :
      ↥(map f N))
have a : (↑(AddHom.toFun
          (LinearMap.toAddHom
              ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                  LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                    ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                  ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
            AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
          ⁅x, Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm⁆ :
        ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
    M') =
  (↑(⁅x,
          AddHom.toFun
            (LinearMap.toAddHom
                ((↑(Submodule.equivMapOfInjective (↑f : M →ₗ[R] M') hf (↑N : Submodule R M)) :
                    LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                      ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
                  LinearMap.{u, u, w, w₁} (RingHom.id R) ↥(↑N : Submodule R M)
                    ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M))) :
              AddHom.{w, w₁} ↥(↑N : Submodule R M) ↥(Submodule.map (↑f : M →ₗ[R] M') (↑N : Submodule R M)))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ N) m hm)⁆ :
        ↥(map f N)) :
    M')
Tactic: ext