-- 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
x : A
⊢ Eq.{u_10 + 1} (α := 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ₚ) :
          (a : A) → Bₚ)
        x :
      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₂)
              (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)) ∘ₗ
            AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ) :
          (a : A) → Bₚ)
        x :
      Bₚ)
have h : Eq.{u_10 + 1} (α := Bₚ)
  ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ) : (a : B) → Bₚ) ((f.toLinearMap : (a : A) → B) x : B) : 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₂)
            (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)) ∘ₗ
          AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ) :
        (a : A) → Bₚ)
      x :
    Bₚ)
Tactic: rw [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
    IsLocalizedModule.mapExtendScalars_apply_apply, IsLocalizedModule.map_apply]