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_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
⊢ (map (Ideal.Quotient.mk P') pX).leadingCoeff ∈ M
have h : (fun (x : ℕ) ↦ HPow.hPow (α := R ⧸ P') (leadingCoeff (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX)) x) 1 =
  (map (Ideal.Quotient.mk P') pX).leadingCoeff
Tactic: use 1
-- 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 :
  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.degree ≤ 0
⊢ φ'.IsIntegralElem ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p)
have hy₁ : p = (C : (a : R) → R[X]) (p.coeff 0)
Tactic: rw [degree_le_zero_iff] at hy
Cleared hypotheses: 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 = (C : (a : R) → R[X]) (p.coeff 0)
⊢ φ'.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ₘ)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[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 = (C : (a : R) → R[X]) (p.coeff 0)
⊢ φ'.IsIntegralElem
    ((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]))
have refine_1 : 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: refine ⟨X - C (algebraMap _ _ ((Ideal.Quotient.mk P') (p.coeff 0))), monic_X_sub_C _, ?_⟩
-- 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 = (C : (a : R) → R[X]) (p.coeff 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
have 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
Tactic: simp only [eval₂_sub, eval₂_X, eval₂_C]
-- 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 = (C : (a : R) → R[X]) (p.coeff 0)
⊢ 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
have 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ₘ)
Tactic: rw [sub_eq_zero, ← φ'.comp_apply]
-- 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'
⊢ 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ₘ)
have 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ₘ)
Tactic: obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective p'
Cleared hypotheses: p', 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ₘ
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.{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ₘ)
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})))
  ((RingHom.comp (algebraMap (R[X] ⧸ P) Sₘ) (Ideal.Quotient.mk P) : (a : R[X]) → Sₘ) p : Sₘ)
Tactic: rw [← RingHom.comp_apply]
-- 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ₘ
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.{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ₘ)
have refine_2 : Membership.mem (γ := Subring R[X]) (Subring.closure (insert X {p : R[X] | p.degree ≤ 0})) p
Tactic: apply Subring.mem_closure_image_of
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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ₘ φ ⋯)
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥
have hM : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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ₘ) ⊥) ⊥
have rw : Function.Injective.{u_2 + 1, u_7 + 1} (α := S) (β := Sₘ) (⇑(algebraMap S Sₘ) : (a : S) → Sₘ)
Tactic: rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥
have hϕ' : 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
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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ₘ) ⊥) ⊥
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥
have hRₘ : IsJacobsonRing Rₘ
Tactic: have hRₘ : IsJacobsonRing Rₘ := isJacobsonRing_localization x