rw [← map_sum, Basis.sum_repr b 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 =
    ∑ x_1 : ι, (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ((b.repr x) x_1 • b x_1)
no goals