-- 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
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)

Tactic:
swap

Result:
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)

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)

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)

case inr.inl.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✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
swap

Result:
case inr.inl.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✝¹ : Fintype ιS
val✝ : Infinite ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

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)

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
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)

Tactic:
have := bA.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
this : Nonempty ιA
⊢ LinearMap.det (↑R f) = (Algebra.norm R) (LinearMap.det f)