rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]
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
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) ∘ ⇑b) ⋯ ⋯) i =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) (b i)
no goals