-- Mathlib/RingTheory/Norm/Transitivity.lean
theorem LinearMap.det_restrictScalars [AddCommGroup A] [Module R A] [Module S A]
    [IsScalarTower R S A] [Module.Free S A] {f : A →ₗ[S] A} :
    (f.restrictScalars R).det = Algebra.norm R f.det

Proof state:
case inr.inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

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

Result:
no goals

Proof state:
case inr.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
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))]

Result:
no goals

Proof state:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
cases fintypeOrInfinite ιS

Result:
case inr.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Fintype ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

case inr.inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝ : Infinite ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Proof state:
case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Subsingleton A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
simp_rw [det_eq_one_of_subsingleton, _root_.map_one]

Result:
no goals

Proof state:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
let ⟨ιA, bA⟩ := Module.Free.exists_basis (R := S) (M := A)

Result:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Proof state:
case inr.inl.inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝¹ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this✝ : Nonempty ιS
this : Nonempty ιA
val✝¹ : Fintype ιS
val✝ : Fintype ιA
⊢ ((Matrix.comp ιA ιA ιS ιS R) (((toMatrix bA bA) f).map ⇑(Algebra.leftMulMatrix bS))).det =
    ((Matrix.comp ιA ιA ιS ιS R) (((toMatrix bA bA) f).map ⇑↑(Algebra.leftMulMatrix bS))).det

Tactic:
rfl

Result:
no goals

Proof state:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
have := bS.index_nonempty

Result:
case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
this✝ : Nontrivial S
ιS : Type u_2
bS : Basis ιS R S
ιA : Type u_3
bA : Basis ιA S A
this : Nonempty ιS
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
cases subsingleton_or_nontrivial A

Result:
case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Subsingleton A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Free R S
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : Module S A
inst✝¹ : IsScalarTower R S A
inst✝ : Module.Free S A
f : A →ₗ[S] A
a✝ : Nontrivial R
h✝ : Nontrivial A
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)