-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x : ↥(map f p)
rw :
  Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) :
                  (a : ↥p) → ↥(map f p))
                (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                    (a : ↥(map f p)) → ↥p)
                  x))) :
          M) :
      M₂)
    ((↑(((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
            (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              x)) :
        M₂) :
      M₂)
rw₁ :
  Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) :
                  (a : ↥p) → ↥(map f p))
                (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                    (a : ↥(map f p)) → ↥p)
                  x))) :
          M) :
      M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              x) :
          M) :
      M₂)
rw₂ :
  Eq.{u_5 + 1} (α := M)
    (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
            (a : ↥(map f p)) → ↥p)
          (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
            (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              x))) :
      M)
    (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
            (a : ↥(map f p)) → ↥p)
          x) :
      M)
⊢ (f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x) :
        M) =
    (↑x : M₂)
have rw₃ : Eq.{u_5 + 1} (α := M)
  (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
          (a : ↥(map f p)) → ↥p)
        x) :
    M)
  (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
          (a : ↥(map f p)) → ↥p)
        x) :
    M)
Tactic: rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
    i.eq_iff, LinearEquiv.apply_symm_apply]