∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Free R S]
  [Module.Finite R S] [inst_5 : IsLocalRing R] (x : S),
  (Algebra.trace (R ⧸ IsLocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)))
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) x) =
    (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) ((Algebra.trace R S) x)