awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p_1 : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p_1 ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p'
p : R[X]
hy : p = (C : (a : R) → R[X]) (p.coeff 0)
refine_1 :
  HSub.hSub (α := Sₘ) (β := Sₘ)
      ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) :
        Sₘ)
      ((φ' : (a : Rₘ) → Sₘ)
          ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ)
              ((Ideal.Quotient.mk P' : (a : R) → R ⧸ P') (p.coeff 0) : R ⧸ P') :
            Rₘ) :
        Sₘ) =
    0
⊢ eval₂ φ'
      ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X]))
      (HSub.hSub (α := Rₘ[X]) (β := Rₘ[X]) X
        ((C : (a : Rₘ) → Rₘ[X])
            ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ)
              ((Ideal.Quotient.mk P' : (a : R) → R ⧸ P') (p.coeff 0) : R ⧸ P')) :
          Rₘ[X])) =
    0

Tactic:
simp only [eval₂_sub, eval₂_X, eval₂_C]

Premises used: Polynomial.eval₂_sub, Polynomial.eval₂_X, Polynomial.eval₂_C
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p_1 : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p_1 ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p'
p : R[X]
hy : p = (C : (a : R) → R[X]) (p.coeff 0)
refine_1 :
  Eq.{u_4 + 1} (α := Sₘ)
    ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) :
      Sₘ)
    ((φ'.comp (algebraMap (R ⧸ P') Rₘ) : (a : R ⧸ P') → Sₘ)
        ((Ideal.Quotient.mk P' : (a : R) → R ⧸ P') (p.coeff 0) : R ⧸ P') :
      Sₘ)
⊢ HSub.hSub (α := Sₘ) (β := Sₘ)
      ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) :
        Sₘ)
      ((φ' : (a : Rₘ) → Sₘ)
          ((algebraMap (R ⧸ P') Rₘ : (a : R ⧸ P') → Rₘ)
              ((Ideal.Quotient.mk P' : (a : R) → R ⧸ P') (p.coeff 0) : R ⧸ P') :
            Rₘ) :
        Sₘ) =
    0

Tactic:
rw [sub_eq_zero, ← φ'.comp_apply]

Premises used: sub_eq_zero, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p_1 : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p_1 ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p'
p : R[X]
hy : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ Eq.{u_4 + 1} (α := Sₘ)
    ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ)
        ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) :
      Sₘ)
    ((φ'.comp (algebraMap (R ⧸ P') Rₘ) : (a : R ⧸ P') → Sₘ)
        ((Ideal.Quotient.mk P' : (a : R) → R ⧸ P') (p.coeff 0) : R ⧸ P') :
      Sₘ)

Tactic:
simp [φ', IsLocalization.map_comp _, P', φ]

Premises used: IsLocalization.map_comp
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p : Sₘ
p' q : R[X] ⧸ P
hq : q ∈ M'
hp :
  HMul.hMul (β := Sₘ) p ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p'
refine_2 :
  ∀ (p_1 : R[X])
    (hp :
      HMul.hMul (β := Sₘ) p ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
        (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ)
          ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) p_1 : R[X] ⧸ P)),
    Membership.mem.{u_4, u_4} (α := Sₘ) (γ := Subring Sₘ)
      (Subring.closure
        (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
          (insert X {p : R[X] | p.degree ≤ 0})))
      ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) p_1 : R[X] ⧸ P) :
        Sₘ)
⊢ Membership.mem.{u_4, u_4} (α := Sₘ) (γ := Subring Sₘ)
    (Subring.closure
      (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
        (insert X {p : R[X] | p.degree ≤ 0})))
    ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p' : Sₘ)

Tactic:
obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective p'

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p_1 : Sₘ
q : R[X] ⧸ P
hq : q ∈ M'
p : R[X]
hp :
  HMul.hMul (β := Sₘ) p_1 ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) p : R[X] ⧸ P)
refine_2 :
  Membership.mem.{u_4, u_4} (α := Sₘ) (γ := Subring Sₘ)
    (Subring.closure
      (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
        (insert X {p : R[X] | p.degree ≤ 0})))
    ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p : Sₘ)
⊢ Membership.mem.{u_4, u_4} (α := Sₘ) (γ := Subring Sₘ)
    (Subring.closure
      (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
        (insert X {p : R[X] | p.degree ≤ 0})))
    ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) p : R[X] ⧸ P) : Sₘ)

Tactic:
rw [← RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p_1 : Sₘ
q : R[X] ⧸ P
hq : q ∈ M'
p : R[X]
hp :
  HMul.hMul (β := Sₘ) p_1 ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) p : R[X] ⧸ P)
refine_2 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {p : R[X] | p.degree ≤ 0})) p
⊢ Membership.mem.{u_4, u_4} (α := Sₘ) (γ := Subring Sₘ)
    (Subring.closure
      (Set.image (α := R[X]) (⇑(RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P)) : (a : R[X]) → Sₘ)
        (insert X {p : R[X] | p.degree ≤ 0})))
    ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p : Sₘ)

Tactic:
apply Subring.mem_closure_image_of

Premises used: Subring.mem_closure_image_of
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
Rₘ : Type u_3
Sₘ : Type u_4
inst_1 : CommRing Rₘ
inst_2 : CommRing Sₘ
P : Ideal R[X]
pX : R[X]
hpX : pX ∈ P
inst_3 : Algebra.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P)) Rₘ
inst_4 :
  IsLocalization.Away (R := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))
    (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) Rₘ
inst_5 : Algebra.{u_1, u_4} (R[X] ⧸ P) Sₘ
inst_6 :
  IsLocalization
    (Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
      (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))))
    Sₘ
P' : Ideal R := comap (F := R →+* R[X]) C P
M : Submonoid (R ⧸ P') := Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX))
M' : Submonoid (R[X] ⧸ P) :=
  Submonoid.map (F := HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P) →+* R[X] ⧸ P)
    (quotientMap P C ⋯) (Submonoid.powers (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)))
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
hφ' : φ.comp (Ideal.Quotient.mk P') = RingHom.comp (Ideal.Quotient.mk P) C
p_1 : Sₘ
q : R[X] ⧸ P
hq : q ∈ M'
p : R[X]
hp :
  HMul.hMul (β := Sₘ) p_1 ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) q : Sₘ) =
    (algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) p : R[X] ⧸ P)
⊢ Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {p : R[X] | p.degree ≤ 0})) p

Tactic:
apply Polynomial.mem_closure_X_union_C

Premises used: Polynomial.mem_closure_X_union_C
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
⊢ LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)

Tactic:
have hM : ((Submonoid.powers x).map φ : Submonoid S) ≤ nonZeroDivisors S :=
    map_le_nonZeroDivisors_of_injective φ hφ (powers_le_nonZeroDivisors_of_noZeroDivisors hx)
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
rw : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := Sₘ) (⇑(algebraMap S Sₘ) : (a : S) → Sₘ)
⊢ Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥

Tactic:
rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]

Premises used: RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
⊢ Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := Sₘ) (⇑(algebraMap S Sₘ) : (a : S) → Sₘ)

Tactic:
IsLocalization.injective Sₘ hM

Premises used: IsLocalization.injective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
⊢ Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := Sₘ) (⇑(algebraMap S Sₘ) : (a : S) → Sₘ)

Tactic:
exact IsLocalization.injective Sₘ hM

Premises used: IsLocalization.injective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
⊢ Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥

Tactic:
have hϕ' : comap (algebraMap S Sₘ) (⊥ : Ideal Sₘ) = (⊥ : Ideal S) := by
      rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
      exact IsLocalization.injective Sₘ hM
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
⊢ IsJacobsonRing Rₘ

Tactic:
have hRₘ : IsJacobsonRing Rₘ := isJacobsonRing_localization x
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
hRₘ : IsJacobsonRing Rₘ
⊢ IsJacobsonRing Sₘ

Tactic:
have hSₘ : IsJacobsonRing Sₘ := isJacobsonRing_of_isIntegral' φ' hφ'