-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Exactness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst_3 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst_4 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst_5 : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst_6 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_2, u_4} S (Sₚ p)
inst_7 : (p : Ideal R) → [inst : p.IsMaximal] → Algebra.{u_3, u_4} (Rₚ p) (Sₚ p)
inst_8 : (p : Ideal R) → [inst_13 : p.IsMaximal] → Algebra.{u_1, u_4} R (Sₚ p)
inst_9 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ p) (Sₚ p)
inst_10 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsScalarTower.{u_1, u_2, u_4} R S (Sₚ p)
inst_11 : ∀ (p : Ideal R) [inst_13 : p.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ p) p
inst_12 :
  ∀ (p : Ideal R) [inst_13 : p.IsMaximal],
    IsLocalizedModule.AtPrime.{u_1, u_2, u_4} (M := S) (M' := Sₚ p) p
      (↑(IsScalarTower.toAlgHom R S (Sₚ p)) :
        [inst_14 : FunLike (S →ₐ[R] Sₚ p) S (Sₚ p)] →
          [SemilinearMapClass (S →ₐ[R] Sₚ p) (RingHom.id R) S (Sₚ p)] → S →ₗ[R] Sₚ p)
H :
  ∀ (p : Ideal R) [inst : p.IsMaximal],
    Function.Injective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have apply : ∀ (P : Ideal R) [inst_13 : P.IsMaximal],
  Function.Injective.{u_3 + 1, u_4 + 1} (α := (fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) P inst_13) (β :=
    (fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) P inst_13)
    (⇑((IsLocalizedModule.map P.primeCompl
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    (Algebra.linearMap R ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) P x) :
                      LinearMap.{u_1, u_1, u_1, u_3} (RingHom.id R) R
                        ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) P x)))
                  P inst_13)
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    ((↑(IsScalarTower.toAlgHom R S (Sₚ P)) :
                        [inst_14 : FunLike (S →ₐ[R] Sₚ P) S (Sₚ P)] →
                          [SemilinearMapClass (S →ₐ[R] Sₚ P) (RingHom.id R) S (Sₚ P)] → S →ₗ[R] Sₚ P) :
                      LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) S (Sₚ P)))
                  P inst_13) :
              (a : R →ₗ[R] S) →
                (fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) P inst_13 →ₗ[R]
                  (fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) P inst_13)
            (Algebra.linearMap R S) :
          LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) P inst_13)
            ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) P inst_13)) :
      (a : (fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) P inst_13) →
        (fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) P inst_13)
Tactic: apply injective_of_isLocalized_maximal (fun P _ ↦ Rₚ P) (fun P _ ↦ Algebra.linearMap _ _)
    (fun P _ ↦ Sₚ P) (fun P _ ↦ IsScalarTower.toAlgHom R S (Sₚ P)) (Algebra.linearMap R S) _