-- Mathlib/RingTheory/Localization/NormTrace.lean
theorem Algebra.traceMatrix_localizationLocalization (b : Basis ι R S) :
    Algebra.traceMatrix Rₘ (b.localizationLocalization Rₘ M Sₘ) =
      (algebraMap R Rₘ).mapMatrix (Algebra.traceMatrix R b)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this : Module.Finite R S
⊢ traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

Tactic:
have : Module.Free R S := Module.Free.of_basis b

Result:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
⊢ traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

Tactic:
have : Module.Finite R S := Module.Finite.of_basis b

Result:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this : Module.Finite R S
⊢ traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
⊢ traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

Tactic:
ext i j : 2

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
i j : ι
⊢ traceMatrix Rₘ (⇑(Basis.localizationLocalization Rₘ M Sₘ b)) i j = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b) i j

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
i j : ι
⊢ traceMatrix Rₘ (⇑(Basis.localizationLocalization Rₘ M Sₘ b)) i j = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b) i j

Tactic:
simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, traceMatrix_apply, traceForm_apply,
  Basis.localizationLocalization_apply, ← map_mul]

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
i j : ι
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) (b i * b j)) = (algebraMap R Rₘ) ((trace R S) (b i * b j))

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
this✝ : Module.Finite R S
this : Module.Free R S
i j : ι
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) (b i * b j)) = (algebraMap R Rₘ) ((trace R S) (b i * b j))

Tactic:
exact Algebra.trace_localization R M _

Result:
no goals