rw [Finsupp.total_eq_fintype_total_apply _ (R ⧸ p), Fintype.total_apply]
case a.a
R : Type u_3
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : LocalRing R
inst✝⁴ : Module.Free R S
inst✝³ : Module.Finite R S
p : Ideal R
inst✝² : p.IsMaximal
inst✝¹ : LocalRing R
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    (Finsupp.total ι (S ⧸ Ideal.map (algebraMap R S) p) (R ⧸ p) ⇑(basisQuotientOfLocalRing b))
      ((Finsupp.linearEquivFunOnFinite (R ⧸ p) (R ⧸ p) ι).symm (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)))
case a.a
R : Type u_3
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : LocalRing R
inst✝⁴ : Module.Free R S
inst✝³ : Module.Finite R S
p : Ideal R
inst✝² : p.IsMaximal
inst✝¹ : LocalRing R
ι : Type u_1
inst✝ : Fintype ι
b : Basis ι R S
x : S
i : ι
⊢ (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x =
    ∑ i : ι, (⇑(Ideal.Quotient.mk p) ∘ ⇑(b.repr x)) i • (basisQuotientOfLocalRing b) i