ext
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)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x : S
⊢ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) =
    Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)
case h
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)) =
    Submodule.map (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) (Submodule.span R s)
hs : Submodule.span (R ⧸ p) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) '' s) = ⊤
x x✝ : S
⊢ x✝ ∈ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ Ideal.map (algebraMap R S) p)) ↔
    x✝ ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R S) p)