-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
Goal:
R : Type u
inst_1 : CommRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u, u'} R (Rₚ P)
inst_7 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u, u'} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u, v'} R (Mₚ P)
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u', v'} (Rₚ P) (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u, u', v'} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u, u, v, v'} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
inst_12 : Small.{v, u} R
inst_13 : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective.{u', v'} (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
r : Rₚ P
m : Mₚ P
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
          Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
      (r • m) =
    HSMul.hSMul (α := Localization.AtPrime P)
      ((((↑(AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)) :
                    RingEquiv.{u', u} (Rₚ P) (Localization.AtPrime P)) :
                RingHom.{u', u} (Rₚ P) (Localization.AtPrime P)) :
              RingHom.{u', u} (Rₚ P) (Localization.AtPrime P)) :
            (a : Rₚ P) → Localization.AtPrime P)
          r :
        Localization.AtPrime P)
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        m)
have H₁ : ∀ (r : R) (s : ↥P.primeCompl),
  AddHom.toFun
      (LinearMap.toAddHom
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
          Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
      (HSMul.hSMul.{u', v', v'} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m) =
    HSMul.hSMul (α := Localization.AtPrime P)
      ((((↑(AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)) :
                  RingEquiv.{u', u} (Rₚ P) (Localization.AtPrime P)) :
              RingHom.{u', u} (Rₚ P) (Localization.AtPrime P)) :
            RingHom.{u', u} (Rₚ P) (Localization.AtPrime P)) :
          (a : Rₚ P) → Localization.AtPrime P)
        (IsLocalization.mk' (Rₚ P) r s))
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        m)
Tactic: obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl r
Cleared hypotheses: r