-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this_1 : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this_2 : Nonempty ιS
this : Nonempty ιA
val : Fintype ιS
val_1 : Fintype ιA
inl :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    (det.{u_1, u_2} (n := ιS)
        ((Algebra.leftMulMatrix bS : (a : S) → Matrix ιS ιS R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f)) :
      R)
inl₁ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    (det.{u_1, u_2} (n := ιS)
        (((↑(Algebra.leftMulMatrix bS) : S →+* Matrix ιS ιS R) : (a : S) → Matrix ιS ιS R)
          ((LinearMap.det : (a : A →ₗ[S] A) → S) f)) :
      R)
inl₂ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    (det.{u_1, u_2} (n := ιS)
        (((↑(Algebra.leftMulMatrix bS) : S →+* Matrix ιS ιS R) : (a : S) → Matrix ιS ιS R)
          (det.{u_2, u_3} (n := ιA) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f))) :
      R)
inl₃ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    (det (n := ιA × ιS)
        ((Matrix.comp ιA ιA ιS ιS R : (a : Matrix ιA ιA (Matrix ιS ιS R)) → Matrix (ιA × ιS) (ιA × ιS) R)
          (Matrix.map (α := S) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f)
            (⇑(↑(Algebra.leftMulMatrix bS) : S →+* Matrix ιS ιS R) : (a : S) → Matrix ιS ιS R))) :
      R)
inl₄ :
  Eq.{u_1 + 1} (α := R)
    (det (n := ιA × ιS)
      ((toMatrix (bS.smulTower' bA) (bS.smulTower' bA) : (a : A →ₗ[R] A) → Matrix (ιA × ιS) (ιA × ιS) R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f)))
    (det (n := ιA × ιS)
      ((Matrix.comp ιA ιA ιS ιS R : (a : Matrix ιA ιA (Matrix ιS ιS R)) → Matrix (ιA × ιS) (ιA × ιS) R)
        (Matrix.map (α := S) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f)
          (⇑(↑(Algebra.leftMulMatrix bS) : S →+* Matrix ιS ιS R) : (a : S) → Matrix ιS ιS R))))
inl₅ :
  Eq.{u_1 + 1} (α := R)
    (det (n := ιA × ιS)
      ((Matrix.comp ιA ιA ιS ιS R : (a : Matrix ιA ιA (Matrix ιS ιS R)) → Matrix (ιA × ιS) (ιA × ιS) R)
        (Matrix.map (α := S) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f)
          (⇑(Algebra.leftMulMatrix bS) : (a : S) → Matrix ιS ιS R))))
    (det (n := ιA × ιS)
      ((Matrix.comp ιA ιA ιS ιS R : (a : Matrix ιA ιA (Matrix ιS ιS R)) → Matrix (ιA × ιS) (ιA × ιS) R)
        (Matrix.map (α := S) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f)
          (⇑(↑(Algebra.leftMulMatrix bS) : S →+* Matrix ιS ιS R) : (a : S) → Matrix ιS ιS R))))
inl₆ inl₇ :
  Eq.{u_1 + 1} (α := R)
    (det (n := ιA × ιS)
      ((Matrix.comp ιA ιA ιS ιS R : (a : Matrix ιA ιA (Matrix ιS ιS R)) → Matrix (ιA × ιS) (ιA × ιS) R)
        (Matrix.map (α := S) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f)
          (⇑(Algebra.leftMulMatrix bS) : (a : S) → Matrix ιS ιS R))))
    (det (n := ιA × ιS)
      ((Matrix.comp ιA ιA ιS ιS R : (a : Matrix ιA ιA (Matrix ιS ιS R)) → Matrix (ιA × ιS) (ιA × ιS) R)
        (Matrix.map (α := S) ((toMatrix bA bA : (a : A →ₗ[S] A) → Matrix ιA ιA S) f)
          (⇑(Algebra.leftMulMatrix bS) : (a : S) → Matrix ιS ιS R))))
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
rw [Algebra.norm_eq_matrix_det bS, ← AlgHom.coe_toRingHom, ← det_toMatrix bA, det_det,
    ← det_toMatrix (bS.smulTower' bA), restrictScalars_toMatrix, RingHom.coe_coe]

Premises used: LinearMap.restrictScalars_toMatrix, AlgHom.coe_toRingHom, Matrix.det_det, Algebra.norm_eq_matrix_det, Module.Basis.smulTower', RingHom.coe_coe, LinearMap.det_toMatrix