-- 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:
rw [← top_le_iff]

Result:
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

Proof state:
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

Tactic:
exact Module.finite_def.mp ‹_›

Result:
no goals

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
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ ↔ span R s = ⊤

Tactic:
have H : (span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
    (span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS)) := by
  rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
    IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]

Result:
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 ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ ↔ span R s = ⊤

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
H :
  restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) = map (IsScalarTower.toAlgHom R S (S ⧸ pS)) (span R s)
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ ↔ span R s = ⊤

Tactic:
constructor

Result:
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)
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤ → span R s = ⊤

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) = ⊤

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) = ⊤
⊢ ⊤ ≤ span R s ⊔ restrictScalars R pS

Tactic:
rintro x -

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
⊢ x ∈ span R s ⊔ restrictScalars R pS

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
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
⊢ LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS)) = restrictScalars R pS

Tactic:
ext

Result:
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

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)
hs : span R s = ⊤
⊢ span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤

Tactic:
rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr,
  restrictScalars_eq_top_iff] at H

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 ⇑(IsScalarTower.toAlgHom R S (S ⧸ pS))

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
⊢ (IsScalarTower.toAlgHom R S (S ⧸ pS)) x ∈ ⊤

Tactic:
exact mem_top

Result:
no goals