-- Mathlib/RingTheory/LocalRing/Quotient.lean
theorem quotient_span_eq_top_iff_span_eq_top (s : Set S) :
    span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s) = ⊤ ↔ span R s = ⊤

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s

Tactic:
apply le_of_le_smul_of_le_jacobson_bot

Result:
case mp.hN'
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤.FG

case mp.hIJ
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ?mp.I ≤ ⊥.jacobson

case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤ ≤ span R s ⊔ ?mp.I • ⊤

case mp.I
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ Ideal R

Proof state:
case mp.hIJ
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ?mp.I ≤ ⊥.jacobson

Tactic:
exact (jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge

Result:
no goals

Proof state:
case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
this : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) = restrictScalars R pS
⊢ x ∈ span R s ⊔ restrictScalars R pS

Tactic:
rw [← this, ← comap_map_eq, mem_comap, ← H, hs, restrictScalars_top]

Result:
case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
this : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) = restrictScalars R pS
⊢ (IsScalarTower.toAlgHom R S (S ⧸ pS)) x ∈ ⊤

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
⊢ restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)

Tactic:
rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
  IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]

Result:
no goals

Proof state:
case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
⊢ x ∈ span R s ⊔ restrictScalars R pS

Tactic:
have : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) =
    restrictScalars R pS := by
  ext; simp [Ideal.Quotient.eq_zero_iff_mem]

Result:
case mp.hNN
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x : S
this : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) = restrictScalars R pS
⊢ x ∈ span R s ⊔ restrictScalars R pS

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    LinearMap.range (IsScalarTower.toAlgHom R S (S ⧸ pS))
hs : span R s = ⊤
⊢ Function.Surjective ⇑(Ideal.Quotient.mk pS)

Tactic:
exact Ideal.Quotient.mk_surjective

Result:
no goals

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
x x✝ : S
⊢ x✝ ∈ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) ↔ x✝ ∈ restrictScalars R pS

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem]

Result:
no goals

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    LinearMap.range (IsScalarTower.toAlgHom R S (S ⧸ pS))
hs : span R s = ⊤
⊢ Function.Surjective ⇑(IsScalarTower.toAlgHom R S (S ⧸ pS))

Tactic:
rw [IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]

Result:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    LinearMap.range (IsScalarTower.toAlgHom R S (S ⧸ pS))
hs : span R s = ⊤
⊢ Function.Surjective ⇑(Ideal.Quotient.mk pS)

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
⊢ span R s = ⊤ → span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

Tactic:
intro hs

Result:
case mpr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
hs : span R s = ⊤
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤