-- 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.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
h :
  Eq (α := (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)) :
      (a : (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))) :
      (a : Rₚ p) → Sₚ p)
⊢ Function.Surjective.{u_3 + 1, u_4 + 1} (α := (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)) :
      (a : (fun (P : Ideal R) (x : P.IsMaximal) ↦ Rₚ P) p hp) → (fun (P : Ideal R) (x : P.IsMaximal) ↦ Sₚ P) p hp)
have convert_to : Function.Surjective.{u_3 + 1, u_4 + 1} (α := Rₚ p) (β := Sₚ p)
  (⇑((↑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))) :
    (a : Rₚ p) → Sₚ p)
Tactic: convert_to Function.Surjective ((Algebra.linearMap (Rₚ p) (Sₚ p)).restrictScalars R)