-- 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
nontriviality :
  Subsingleton 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)
nontriviality₁ :
  Nontrivial 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)
nontriviality₂ :
  Nontrivial R →
    Nontrivial A →
      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)
nontriviality₃ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S),
        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)
nontriviality₄ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S),
        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)
nontriviality₅ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A),
        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)
nontriviality₆ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS),
        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)
nontriviality₇ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA),
        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)
inl :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS),
        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)
inr :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA),
        Infinite ιS →
          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)
inl₁ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS),
        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)
inr₁ inr₂ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA),
        Infinite ιS →
          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)
inl₂ inl₃ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS),
        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)
inl₄ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS) (val : Fintype ιA),
        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)
inl₅ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS),
        Infinite ιA →
          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)
inl₆ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS) (val : Fintype ιA),
        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)
inl₇ inl₈ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS),
        Infinite ιA →
          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)
inl₉ inl₁₀ :
  Nontrivial R →
    Nontrivial A →
      ∀ (this : Nontrivial S) (ιS : Type u_2) (bS : Module.Basis ιS R S) (ιA : Type u_3) (bA : Module.Basis ιA S A)
        (this : Nonempty ιS) (this : Nonempty ιA) (val : Fintype ιS) (val : Fintype ιA),
        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)
⊢ 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:
classical
  nontriviality R
  nontriviality A
  have := Module.nontrivial S A
  let ⟨ιS, bS⟩ := Module.Free.exists_basis (R := R) (M := S)
  let ⟨ιA, bA⟩ := Module.Free.exists_basis (R := S) (M := A)
  have := bS.index_nonempty
  have := bA.index_nonempty
  cases fintypeOrInfinite ιS; swap
  · rw [Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]
  cases fintypeOrInfinite ιA; swap
  · rw [det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bA), map_one,
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]
  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, RingHom.coe_coe, map_one