-- Module: Mathlib.RingTheory.Trace.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Free R S
inst_4 : Module.Finite R S
inst_5 : IsLocalRing R
x : S
let let₁ let₂ let₃ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((trace (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((trace R S : (a : S) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
let₄ :
  let ι := Free.ChooseBasisIndex R S;
  let b : Basis ι R S := Free.chooseBasis R S;
  Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) p)
    (Matrix.trace.{u_2, u_1} (n := ι)
      ((leftMulMatrix (basisQuotient b) : (a : S ⧸ pS) → Matrix ι ι (R ⧸ p))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x)))
    (Matrix.trace.{u_2, u_1} (n := ι)
      (Matrix.map (α := R) ((leftMulMatrix b : (a : S) → Matrix ι ι R) x) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)))
e_A :
  let ι := Free.ChooseBasisIndex R S;
  let b : Basis ι R S := Free.chooseBasis R S;
  Eq (α := Matrix.{u_2, u_2, u_1} ι ι (HasQuotient.Quotient R (B := Ideal R) p))
    ((leftMulMatrix (basisQuotient b) : (a : S ⧸ pS) → Matrix ι ι (R ⧸ p))
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      Matrix.{u_2, u_2, u_1} ι ι (HasQuotient.Quotient R (B := Ideal R) p))
    (Matrix.map (α := R) ((leftMulMatrix b : (a : S) → Matrix ι ι R) x) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p) :
      Matrix.{u_2, u_2, u_1} ι ι (HasQuotient.Quotient R (B := Ideal R) (p : Ideal R)))
e_A₁ :
  let ι := Free.ChooseBasisIndex R S;
  let b : Basis ι R S := Free.chooseBasis R S;
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) p)
      ((leftMulMatrix (basisQuotient b) : (a : S ⧸ pS) → Matrix ι ι (R ⧸ p))
          ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) i j :
        HasQuotient.Quotient R (B := Ideal R) p)
      (Matrix.map (α := R) ((leftMulMatrix b : (a : S) → Matrix ι ι R) x) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p) i
          j :
        HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) p)
    ((trace (HasQuotient.Quotient R (B := Ideal R) p)
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
          (a : S ⧸ pS) → R ⧸ p)
        ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
      HasQuotient.Quotient R (B := Ideal R) p)
    ((Ideal.Quotient.mk p : (a : R) → R ⧸ p) ((trace R S : (a : S) → R) x) :
      HasQuotient.Quotient R (B := Ideal R) (p : Ideal R))

Tactic:
classical
  let ι := Module.Free.ChooseBasisIndex R S
  let b : Module.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', Matrix.map_apply, ← map_mul,
    basisQuotient_repr]

Premises used: AddMonoidHom.map_trace, LinearMap.mul_apply', IsLocalRing.basisQuotient_repr, Matrix.map_apply, map_mul, IsLocalRing.basisQuotient_apply, Algebra.coe_lmul_eq_mul, Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply