awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
⊢ Eq (α :=
      Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
      ⊤ ↔
    Eq (α := Submodule R S) (span R s) ⊤
have mp : Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤ →
  Eq (α := Submodule R S) (span R s) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
mp :
  Eq (α :=
      Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
      ⊤ →
    Eq (α := Submodule R S) (span R s) ⊤
⊢ Eq (α :=
      Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
      ⊤ ↔
    Eq (α := Submodule R S) (span R s) ⊤
have mpr : Eq (α := Submodule R S) (span R s) ⊤ →
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
⊢ Eq (α := Submodule R S) (span R s) ⊤
have mp : LE.le (α := Submodule R S) ⊤ (span R s)
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
⊢ LE.le (α := Submodule R S) ⊤ (span R s)
have mp : FG.{u_1, u_2} (R := R) (M := S) ⊤
Tactic: apply le_of_le_smul_of_le_jacobson_bot
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
mp : FG.{u_1, u_2} (R := R) (M := S) ⊤
⊢ LE.le (α := Submodule R S) ⊤ (span R s)
have mp₁ : LE.le (α := Ideal R) p (Ideal.jacobson ⊥)
Tactic: apply le_of_le_smul_of_le_jacobson_bot
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
mp : FG.{u_1, u_2} (R := R) (M := S) ⊤
mp₁ : LE.le (α := Ideal R) p (Ideal.jacobson ⊥)
⊢ LE.le (α := Submodule R S) ⊤ (span R s)
have mp₂ : ⊤ ≤ span R s ⊔ HSMul.hSMul (α := Ideal R) (β := Submodule R S) p ⊤
Tactic: apply le_of_le_smul_of_le_jacobson_bot
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
mp : FG.{u_1, u_2} (R := R) (M := S) ⊤
mp₁ : LE.le (α := Ideal R) p (Ideal.jacobson ⊥)
mp₂ : ⊤ ≤ span R s ⊔ HSMul.hSMul (α := Ideal R) (β := Submodule R S) p ⊤
⊢ LE.le (α := Submodule R S) ⊤ (span R s)
have mp₃ : Ideal R
Tactic: apply le_of_le_smul_of_le_jacobson_bot
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
⊢ ⊤ ≤ span R s ⊔ HSMul.hSMul (α := Ideal R) (β := Submodule R S) p ⊤
have mp : LE.le (α := Submodule R S) ⊤ (span R s ⊔ Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [Ideal.smul_top_eq_map]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
x : S
⊢ Eq (α := Submodule R S)
    (LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
    (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p))
have h : ∀ (x : S),
  Membership.mem (γ := Submodule R S)
      (LinearMap.ker (R₂ := R) (M₂ :=
        HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) (τ₁₂ := RingHom.id R)
        (↑(IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
          [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
            [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
      x ↔
    Membership.mem (γ := Submodule R S) (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
x : S
⊢ Membership.mem (γ := Submodule R S)
    (span R s ⊔ Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p)) x
have this : Eq (α := Submodule R S)
  (LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (τ₁₂ := RingHom.id R)
    (↑(IsScalarTower.toAlgHom R S
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
      [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
        [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
  (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: have : LinearMap.ker (IsScalarTower.toAlgHom R S (S ⧸ pS) : S →ₗ[R] S ⧸ pS) =
          Submodule.restrictScalars R pS := by
        ext; simp [Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs :
  Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
x : S
this :
  Eq (α := Submodule R S)
    (LinearMap.ker (R₂ := R) (M₂ := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
      (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
    (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Membership.mem (γ := Submodule R S)
    (span R s ⊔ Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p)) x
have mp : Membership.mem (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) (γ :=
  Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) ⊤
  (((↑(IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
          [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
            [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
        (a : S) → S ⧸ pS)
      x :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: rw [← this, ← comap_map_eq, mem_comap, ← H, hs, restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
hs : Eq (α := Submodule R S) (span R s) ⊤
⊢ Eq (α :=
    Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
      (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
    ⊤
have mpr : ∀
  (H :
    Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
      (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
        (span (HasQuotient.Quotient R (B := Ideal R) p)
          ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
      (LinearMap.range (M := S) (τ₁₂ := RingHom.id R)
        (↑(IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
          [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
            [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)))
  (hs : Eq (α := Submodule R S) (span R s) ⊤),
  Function.Surjective (α := S) (β :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (⇑(↑(IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
          [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
            [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
      (a : S) → S ⧸ pS)
Tactic: rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr,
      restrictScalars_eq_top_iff] at H
Cleared hypotheses: H, hs
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
s : Set S
H :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (LinearMap.range (M := S) (τ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS))
hs : Eq (α := Submodule R S) (span R s) ⊤
⊢ Function.Surjective (α := S) (β :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (⇑(↑(IsScalarTower.toAlgHom R S
              (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
          [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
            [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
      (a : S) → S ⧸ pS)
have mpr : Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS)
Tactic: rw [LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]