-- Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
Goal:
R : Type u_6
inst : CommRing R
S : Type u_7
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_8
inst_3 : AddCommGroup M
inst_4 : Module R M
P : Type u_9
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Module S P
inst_8 : IsScalarTower R S P
inst_9 : Free R M
inst_10 : Module.Finite R M
α : M →ₗ[R] P
j : IsBaseChange S α
f : M →ₗ[R] M
hR : Nontrivial R
b : Basis (Fin (finrank R M)) R M := finBasis R M
inr :
  Eq.{u_7 + 1} (α := S)
    ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₁ :
  Eq.{u_7 + 1} (α := S)
    (Matrix.det (n := Fin (finrank R M))
        ((toMatrix (basis b j) (basis b j) : (a : P →ₗ[S] P) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) S)
          ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₂ :
  Eq.{u_7 + 1} (α := S)
    (Matrix.det (n := Fin (finrank R M))
        (Matrix.map.{u_6, u_7, 0, 0} (α := R)
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)
          (⇑(algebraMap R S) : (a : R) → S)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₃ :
  Eq.{u_7 + 1} (α := S)
    (Matrix.det (n := Fin (finrank R M))
        (((RingHom.mapMatrix (algebraMap R S) :
              RingHom.{u_6, u_7} (Matrix (Fin (finrank R M)) (Fin (finrank R M)) R)
                (Matrix (Fin (finrank R M)) (Fin (finrank R M)) S)) :
            (a : Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) S)
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
inr₄ inr₅ :
  Eq.{u_7 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
    ((algebraMap R S : (a : R) → S)
        (Matrix.det (n := Fin (finrank R M))
          ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin (finrank R M)) (Fin (finrank R M)) R) f)) :
      S)
⊢ Eq.{u_7 + 1} (α := S)
    ((LinearMap.det : (a : P →ₗ[S] P) → S) ((j.endHom : (a : M →ₗ[R] M) → P →ₗ[S] P) f : P →ₗ[S] P) : S)
    ((algebraMap R S : (a : R) → S) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : S)

Tactic:
rw [← f.det_toMatrix b, ← (j.endHom f).det_toMatrix (j.basis b),
    endHom_toMatrix, ← RingHom.mapMatrix_apply, ← RingHom.map_det]

Premises used: RingHom.mapMatrix_apply, IsBaseChange.endHom_toMatrix, RingHom.map_det, DFunLike.coe, LinearMap.det_toMatrix, IsBaseChange.endHom, IsBaseChange.basis