apply (quotient_span_eq_top_iff_span_eq_top_of_localRing _).mpr b.span_eq
case a
R : Type u_2
S : Type u_1
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
this✝ : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) p)
this : Module.Finite (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p)
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ Submodule.span (R ⧸ p) (⇑(IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) '' Set.range ⇑b) = ⊤
no goals