-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ Eq (α := Aₚ →ₗ[R] Bₚ)
    ((↑R :
        {S : Type u_8} →
          {M : Type u_9} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module R M] →
                        [inst_26 : Module R M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₚ)
      (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
              (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
            (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
        f.toLinearMap))
    ((↑R :
        {S : Type u_8} →
          {M : Type u_9} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module R M] →
                        [inst_26 : Module R M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)))
have h : Eq (α := A →ₗ[R] Bₚ)
  ((↑R :
        {S : Type u_8} →
          {M : Type u_9} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module R M] →
                        [inst_26 : Module R M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₚ)
      (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
              (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
            (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
        f.toLinearMap) ∘ₗ
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
  ((↑R :
        {S : Type u_8} →
          {M : Type u_9} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module R M] →
                        [inst_26 : Module R M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)) ∘ₗ
    AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
Tactic: apply IsLocalizedModule.linearMap_ext M
    (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
    ((IsScalarTower.toAlgHom R B Bₚ).toLinearMap)