change _ = LinearMap.range (Ideal.Quotient.mkₐ _ _) at H
case mpr
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
s : Set S
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    LinearMap.range (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p))
hs : Submodule.span R s = ⊤
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
case mpr
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
s : Set S
hs : Submodule.span R s = ⊤
H :
  Submodule.restrictScalars R (Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s)) =
    LinearMap.range (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) p))
⊢ Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤