-- Mathlib/RingTheory/Trace/Quotient.lean
lemma Algebra.trace_quotient_mk [IsLocalRing R] (x : S) :
    Algebra.trace (R ⧸ p) (S ⧸ pS) (Ideal.Quotient.mk pS x) =
      Ideal.Quotient.mk p (Algebra.trace R S x)

Proof state:
case e_A.a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
i j : ι
⊢ (leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x) i j =
    (↑(Ideal.Quotient.mk p)).mapMatrix ((leftMulMatrix b) x) i j

Tactic:
simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
  basisQuotient_apply, LinearMap.mul_apply', RingHom.toAddMonoidHom_eq_coe,
  AddMonoidHom.mapMatrix_apply, AddMonoidHom.coe_coe, Matrix.map_apply, ← map_mul,
  basisQuotient_repr]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Tactic:
let ι := Module.Free.ChooseBasisIndex R S

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Tactic:
let b : Basis ι R S := Module.Free.chooseBasis R S

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Tactic:
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x)).trace =
    ((↑(Ideal.Quotient.mk p)).mapMatrix ((leftMulMatrix b) x)).trace

Proof state:
case e_A
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x) =
    (↑(Ideal.Quotient.mk p)).mapMatrix ((leftMulMatrix b) x)

Tactic:
ext i j

Result:
case e_A.a
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
i j : ι
⊢ (leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x) i j =
    (↑(Ideal.Quotient.mk p)).mapMatrix ((leftMulMatrix b) x) i j

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((trace R S) x)

Tactic:
classical
let ι := Module.Free.ChooseBasisIndex R S
let b : Basis ι R S := Module.Free.chooseBasis R S
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]
congr 1
ext i j
simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply,
  basisQuotient_apply, LinearMap.mul_apply', RingHom.toAddMonoidHom_eq_coe,
  AddMonoidHom.mapMatrix_apply, AddMonoidHom.coe_coe, Matrix.map_apply, ← map_mul,
  basisQuotient_repr]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ ((leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x)).trace =
    ((↑(Ideal.Quotient.mk p)).mapMatrix ((leftMulMatrix b) x)).trace

Tactic:
congr 1

Result:
case e_A
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Free R S
inst✝¹ : Module.Finite R S
inst✝ : IsLocalRing R
x : S
ι : Type u_2 := Module.Free.ChooseBasisIndex R S
b : Basis ι R S := Module.Free.chooseBasis R S
⊢ (leftMulMatrix (basisQuotient b)) ((Ideal.Quotient.mk pS) x) =
    (↑(Ideal.Quotient.mk p)).mapMatrix ((leftMulMatrix b) x)