-- Module: Mathlib.RingTheory.LocalProperties.Exactness
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.Surjective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p) (⇑(algebraMap (Rₚ p) (Sₚ p)) : (a : Rₚ p) → Sₚ p)
p : Ideal R
hp : p.IsMaximal
⊢ Eq (α :=
    LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) p hp)
      ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) p hp))
    ((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 hp)
            ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                ((↑(IsScalarTower.toAlgHom R S (Sₚ P)) :
                    [inst_13 : 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 hp) :
          (a : R →ₗ[R] S) →
            (fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) p hp →ₗ[R] (fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) p hp)
        (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 hp)
        ((fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) p hp))
    ((↑R :
          {S M : Type u_3} →
            {M₂ : Type u_4} →
              [inst : Semiring R] →
                [inst_13 : Semiring S] →
                  [inst_14 : AddCommMonoid M] →
                    [inst_15 : AddCommMonoid M₂] →
                      [inst_16 : Module R M] →
                        [inst_17 : Module R M₂] →
                          [inst_18 : Module S M] →
                            [inst_19 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap (Rₚ p) (Sₚ p)) :
      LinearMap.{u_1, u_1, u_3, u_4} (RingHom.id R) (Rₚ p) (Sₚ p))

Tactic:
apply IsLocalizedModule.map_linearMap_of_isLocalization

Premises used: IsLocalizedModule.map_linearMap_of_isLocalization