awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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'
⊢ φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
have refine_1 : ∀ (x : Sₘ),
  Membership.mem (γ := Set Sₘ)
      (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}))
      x →
    φ'.IsIntegralElem x
Tactic: refine @IsIntegral.of_mem_closure'' Rₘ _ Sₘ _ φ'
    ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_
    ((algebraMap (R[X] ⧸ P) Sₘ) p') ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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_1 :
  ∀ (x : Sₘ),
    Membership.mem (γ := Set Sₘ)
        (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}))
        x →
      φ'.IsIntegralElem x
⊢ φ'.IsIntegralElem ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p')
have 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})))
  ((algebraMap (R[X] ⧸ P) Sₘ : (a : R[X] ⧸ P) → Sₘ) p' : Sₘ)
Tactic: refine @IsIntegral.of_mem_closure'' Rₘ _ Sₘ _ φ'
    ((algebraMap (R[X] ⧸ P) Sₘ).comp (Ideal.Quotient.mk P) '' insert X { p | p.degree ≤ 0 }) ?_
    ((algebraMap (R[X] ⧸ P) Sₘ) p') ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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_1 :
  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]
hp : Membership.mem (γ := Set R[X]) (insert X {p : R[X] | p.degree ≤ 0}) p
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
have hp₁ : p = X ∨ p.degree ≤ 0
Tactic: push _ ∈ _ at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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_1 :
  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]
hp : p = X ∨ p.degree ≤ 0
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
have refine_1 : ∀ (hy : p = X), φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
Tactic: rcases hp with hy | hy
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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_1 :
  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]
hp : p = X ∨ p.degree ≤ 0
refine_1 :
  ∀ (hy : p = X),
    φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
have refine_1₁ : ∀ (hy : p.degree ≤ 0),
  φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
Tactic: rcases hp with hy | hy
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
have refine_1 : φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) X)
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) X)
have refine_1 : eval₂ φ ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) (map (Ideal.Quotient.mk P') pX) = 0
Tactic: refine φ.isIntegralElem_localization_at_leadingCoeff ((Ideal.Quotient.mk P) X)
        (pX.map (Ideal.Quotient.mk P')) ?_ M ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
refine_1 : eval₂ φ ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) (map (Ideal.Quotient.mk P') pX) = 0
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) X)
have refine_1₁ : (map (Ideal.Quotient.mk P') pX).leadingCoeff ∈ M
Tactic: refine φ.isIntegralElem_localization_at_leadingCoeff ((Ideal.Quotient.mk P) X)
        (pX.map (Ideal.Quotient.mk P')) ?_ M ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
⊢ eval₂ φ ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) (map (Ideal.Quotient.mk P') pX) = 0
have refine_1 : eval₂ (φ.comp (Ideal.Quotient.mk P')) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
Tactic: rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
refine_1 : eval₂ (φ.comp (Ideal.Quotient.mk P')) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
⊢ eval₂ φ ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) (map (Ideal.Quotient.mk P') pX) = 0
have refine_1₁ : eval₂ (RingHom.comp (Ideal.Quotient.mk P) C) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
Tactic: rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
refine_1 : eval₂ (φ.comp (Ideal.Quotient.mk P')) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
refine_1₁ : eval₂ (RingHom.comp (Ideal.Quotient.mk P) C) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
⊢ eval₂ φ ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) (map (Ideal.Quotient.mk P') pX) = 0
have refine_1₂ : Eq (α := R[X] ⧸ P) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) (eval₂ C X pX) : R[X] ⧸ P) (0 : R[X] ⧸ P)
Tactic: rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 = X
refine_1 : eval₂ (φ.comp (Ideal.Quotient.mk P')) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
refine_1₁ : eval₂ (RingHom.comp (Ideal.Quotient.mk P) C) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) pX = 0
refine_1₂ : Eq (α := R[X] ⧸ P) ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) (eval₂ C X pX) : R[X] ⧸ P) (0 : R[X] ⧸ P)
⊢ eval₂ φ ((Ideal.Quotient.mk P : (a : R[X]) → R[X] ⧸ P) X) (map (Ideal.Quotient.mk P') pX) = 0
have refine_1₃ : eval₂ C X pX ∈ P
Tactic: rwa [eval₂_map, hφ', ← hom_eval₂, Quotient.eq_zero_iff_mem, eval₂_C_X]