awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 : LE.le (α := Submodule R S) ⊤ (span R s)
⊢ Eq (α := Submodule R S) (span R s) ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 ⊤
mp₃ : Ideal R
⊢ LE.le (α := Submodule R S) ⊤ (span R s)

Tactic:
apply le_of_le_smul_of_le_jacobson_bot

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
    ⊤
⊢ FG.{u_1, u_2} (R := R) (M := S) ⊤

Tactic:
Module.finite_def.mp ‹_›

Premises used: Module.finite_def, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
    ⊤
⊢ FG.{u_1, u_2} (R := R) (M := S) ⊤

Tactic:
exact Module.finite_def.mp ‹_›

Premises used: Module.finite_def, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 (α := Ideal R) p (Ideal.jacobson ⊥)

Tactic:
(jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge

Premises used: Eq.ge, Set.Mem, setOf, Bot.bot, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 (α := Ideal R) p (Ideal.jacobson ⊥)

Tactic:
exact (jacobson_eq_maximalIdeal ⊥ bot_ne_top).ge

Premises used: Eq.ge, Bot.bot, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 : LE.le (α := Submodule R S) ⊤ (span R s ⊔ Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ ⊤ ≤ span R s ⊔ HSMul.hSMul (α := Ideal R) (β := Submodule R S) p ⊤

Tactic:
rw [Ideal.smul_top_eq_map]

Premises used: Ideal.smul_top_eq_map
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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
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
⊢ 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:
ext
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 x_1 : 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_1 ↔
    Membership.mem (γ := Submodule R S) (Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p)) x_1

Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))

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]
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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))
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))
⊢ Membership.mem (γ := Submodule R S)
    (span R s ⊔ Submodule.restrictScalars R (Ideal.map (F := R →+* S) (algebraMap R S) p)) x

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

Premises used: Submodule.restrictScalars_top, Submodule.mem_comap, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 (α := 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:
mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.LocalRing.Quotient
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 (α := 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:
exact mem_top

Premises used: Submodule.mem_top