awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective (α := R ⧸ P') (β := R[X] ⧸ P) (⇑φ : (a : R ⧸ P') → R[X] ⧸ P) := ⋯
Rₘ : Type u_5 := Localization.Away x
Sₘ : Type u_5 := Localization (Submonoid.map φ (Submonoid.powers x))
neg : RingHom.IsIntegral.{u_5, u_5} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥

Tactic:
refine jacobson_bot_of_integral_localization (S := R[X] ⧸ P) (R := R ⧸ P') Rₘ Sₘ _ hφ _ hx ?_

Premises used: Polynomial.jacobson_bot_of_integral_localization
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective (α := R ⧸ P') (β := R[X] ⧸ P) (⇑φ : (a : R ⧸ P') → R[X] ⧸ P) := ⋯
Rₘ : Type u_5 := Localization.Away x
Sₘ : Type u_5 := Localization (Submonoid.map φ (Submonoid.powers x))
⊢ RingHom.IsIntegral.{u_5, u_5} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)

Tactic:
isIntegral_isLocalization_polynomial_quotient P p pP

Premises used: Polynomial.isIntegral_isLocalization_polynomial_quotient
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective (α := R ⧸ P') (β := R[X] ⧸ P) (⇑φ : (a : R ⧸ P') → R[X] ⧸ P) := ⋯
Rₘ : Type u_5 := Localization.Away x
Sₘ : Type u_5 := Localization (Submonoid.map φ (Submonoid.powers x))
⊢ RingHom.IsIntegral.{u_5, u_5} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)

Tactic:
exact isIntegral_isLocalization_polynomial_quotient P p pP

Premises used: Polynomial.isIntegral_isLocalization_polynomial_quotient
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
rw : ∀ (P : Ideal R[X]), P.IsPrime → P.jacobson = P
⊢ IsJacobsonRing.{u_1} R[X]

Tactic:
rw [isJacobsonRing_iff_prime_eq]

Premises used: isJacobsonRing_iff_prime_eq
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
⊢ Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')

Tactic:
have hi : Function.Surjective ↑i := ((Ideal.Quotient.mk I).comp C).rangeRestrict_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f
apply : ∀ (n : ℕ), Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)
⊢ f ∈ I

Tactic:
apply polynomial_mem_ideal_of_coeff_mem_ideal I f

Premises used: Ideal.polynomial_mem_ideal_of_coeff_mem_ideal
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
hf : Membership.mem (γ := Submodule R[X] R[X]) (RingHom.ker (mapRingHom i)) f
n : ℕ
⊢ Eq.{u_1 + 1} (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
    ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n)
      ((mapRingHom i : (a : R[X]) → (↥R')[X]) f))
    ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n) 0)

Tactic:
replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
    ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n)
      ((mapRingHom i : (a : R[X]) → (↥R')[X]) f))
    ((fun (g : (↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))[X]) ↦ g.coeff n) 0)
⊢ Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
    (coeff (map (RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)) f) n) 0

Tactic:
change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf

Premises used: Polynomial.C, Ideal.Quotient.mk, RingHom.rangeRestrict, Polynomial.coeff, RingHom.comp, Polynomial.map
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq (α := ↥(RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)))
    (coeff (map (RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)) f) n) 0
⊢ Eq.{u_1 + 1} (α := R[X] ⧸ I)
    (↑((RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C) : (a : R) → ↥((Ideal.Quotient.mk I).comp C).range)
          (f.coeff n)) :
      R[X] ⧸ I)
    (↑0 : R[X] ⧸ I)

Tactic:
rw [coeff_map, Subtype.ext_iff] at hf

Premises used: Polynomial.coeff_map, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
f : R[X]
n : ℕ
hf :
  Eq.{u_1 + 1} (α := R[X] ⧸ I)
    (↑((RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C) : (a : R) → ↥((Ideal.Quotient.mk I).comp C).range)
          (f.coeff n)) :
      R[X] ⧸ I)
    (↑0 : R[X] ⧸ I)
rwa : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (f.coeff n) : R[X])
rwa₁ :
  Eq (α := R[X] ⧸ I) ((Ideal.Quotient.mk I : (a : R[X]) → R[X] ⧸ I) ((C : (a : R) → R[X]) (f.coeff n)) : R[X] ⧸ I)
    (0 : R[X] ⧸ I)
rwa₂ rwa₃ rwa₄ rwa₅ :
  Eq (α := R[X] ⧸ I) ((RingHom.comp (Ideal.Quotient.mk I) C : (a : R) → R[X] ⧸ I) (f.coeff n) : R[X] ⧸ I) (0 : R[X] ⧸ I)
⊢ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C I) (f.coeff n)

Tactic:
rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]

Premises used: Ideal.Quotient.eq_zero_iff_mem, RingHom.comp_apply, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
have hi' : RingHom.ker (mapRingHom i) ≤ I := by
    intro f hf
    apply polynomial_mem_ideal_of_coeff_mem_ideal I f
    intro n
    replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf
    change (Polynomial.map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0 at hf
    rw [coeff_map, Subtype.ext_iff] at hf
    rwa [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ IsJacobsonRing.{u_1} ↥R'

Tactic:
have R'_jacob : IsJacobsonRing R' := isJacobsonRing_of_surjective ⟨i, hi⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
⊢ Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])

Tactic:
have h_surj : Function.Surjective (mapRingHom i) := Polynomial.map_surjective i hi
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
⊢ J.IsPrime

Tactic:
have : IsPrime J := map_isPrime_of_surjective h_surj hi'
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : J.jacobson = J
⊢ Eq (α := Ideal R[X]) (comap (mapRingHom i) J.jacobson) (comap (mapRingHom i) J)

Tactic:
replace h := congrArg (comap (Polynomial.mapRingHom i)) h
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : Eq (α := Ideal R[X]) (comap (mapRingHom i) J.jacobson) (comap (mapRingHom i) J)
⊢ I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥

Tactic:
rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
      comap_map_of_surjective _ h_surj] at h

Premises used: Ideal.comap_map_of_surjective, Ideal.map_jacobson_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson = I

Tactic:
le_antisymm ?_ le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
refine : I.jacobson ≤ I
⊢ I.jacobson = I

Tactic:
refine le_antisymm ?_ le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson ≤ I

Tactic:
le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))

Premises used: le_rfl, le_sup_of_le_left, sup_le, le_of_eq, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson ≤ I

Tactic:
exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))

Premises used: le_rfl, le_sup_of_le_left, sup_le, le_of_eq, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
suffices : J.jacobson = J
⊢ I.jacobson = I

Tactic:
suffices h : J.jacobson = J by
    replace h := congrArg (comap (Polynomial.mapRingHom i)) h
    rw [← map_jacobson_of_surjective h_surj hi', comap_map_of_surjective _ h_surj,
      comap_map_of_surjective _ h_surj] at h
    refine le_antisymm ?_ le_jacobson
    exact le_trans (le_sup_of_le_left le_rfl) (le_trans (le_of_eq h) (sup_le le_rfl hi'))
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
apply : ∀ (x : ↥R'), Membership.mem (α := (↥R')[X]) J ((C : (a : ↥R') → (↥R')[X]) x : (↥R')[X]) → x = 0
⊢ J.jacobson = J

Tactic:
apply isJacobsonRing_polynomial_of_domain R' J

Premises used: _private.0.Polynomial.isJacobsonRing_polynomial_of_domain, Membership.mem, Subtype
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
⊢ ∀ (x : ↥R'), Membership.mem (α := (↥R')[X]) J ((C : (a : ↥R') → (↥R')[X]) x : (↥R')[X]) → x = 0

Tactic:
eq_zero_of_polynomial_mem_map_range I

Premises used: Set.Mem, setOf, Ideal.eq_zero_of_polynomial_mem_map_range
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := RingHom.range (R := R) (RingHom.comp (Ideal.Quotient.mk I) C)
i : R →+* ↥R' := RingHom.rangeRestrict (RingHom.comp (Ideal.Quotient.mk I) C)
hi : Function.Surjective (α := R) (β := ↥R') (⇑i : (a : R) → ↥R')
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing.{u_1} ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective (α := R[X]) (β := (↥R')[X]) (⇑(mapRingHom i) : (a : R[X]) → (↥R')[X])
this : J.IsPrime
⊢ ∀ (x : ↥R'), Membership.mem (α := (↥R')[X]) J ((C : (a : ↥R') → (↥R')[X]) x : (↥R')[X]) → x = 0

Tactic:
exact eq_zero_of_polynomial_mem_map_range I

Premises used: Ideal.eq_zero_of_polynomial_mem_map_range
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing.{u_1} R[X] ↔ IsJacobsonRing R

Tactic:
⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩

Premises used: Iff.intro, Polynomial.isJacobsonRing_polynomial_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
refine : IsJacobsonRing.{u_1} R[X] → IsJacobsonRing R
⊢ IsJacobsonRing.{u_1} R[X] ↔ IsJacobsonRing R

Tactic:
refine ⟨?_, isJacobsonRing_polynomial_of_isJacobsonRing⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
H : IsJacobsonRing.{u_1} R[X]
x : R
⊢ (eval₂RingHom (RingHom.id R) 1 : (a : R[X]) → R) ((C : (a : R) → R[X]) x : R[X]) = x

Tactic:
simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]

Premises used: RingHom.id_apply, Polynomial.eval₂_C, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
H : IsJacobsonRing.{u_1} R[X]
⊢ IsJacobsonRing R

Tactic:
exact isJacobsonRing_of_surjective ⟨eval₂RingHom (RingHom.id _) 1, fun x =>
    ⟨C x, by simp only [coe_eval₂RingHom, RingHom.id_apply, eval₂_C]⟩⟩

Premises used: Polynomial.C, isJacobsonRing_of_surjective, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain S
Rₘ : Type u_3
Sₘ : Type u_4
inst_3 : CommRing Rₘ
inst_4 : CommRing Sₘ
inst_5 : IsJacobsonRing R
⊢ IsJacobsonRing.{u_1} R[X]

Tactic:
isJacobsonRing_polynomial_iff_isJacobsonRing.mpr ‹IsJacobsonRing R›

Premises used: Iff.mpr, Polynomial.isJacobsonRing_polynomial_iff_isJacobsonRing
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)

Tactic:
(isIntegral_quotientMap_iff _).mp ?_

Premises used: Iff.mp, isIntegral_quotientMap_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
refine : RingHom.IsIntegral (quotientMap P C ⋯)
⊢ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) C)

Tactic:
refine (isIntegral_quotientMap_iff _).mp ?_

Premises used: Iff.mp, isIntegral_quotientMap_iff
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
P' : Ideal R := comap (F := R →+* R[X]) C P
pX : R[X]
hpX : pX ∈ P
hp0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX) 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
⊢ P'.IsPrime

Tactic:
have hP'_prime : P'.IsPrime := comap_isPrime C P
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_1
inst : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst_1 : Nontrivial R
hR : IsJacobsonRing R
hP' : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
P' : Ideal R := comap (F := R →+* R[X]) C P
pX : R[X]
hpX : pX ∈ P
hp0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) pX) 0
a : R ⧸ P' := (map (Ideal.Quotient.mk P') pX).leadingCoeff
M : Submonoid (R ⧸ P') := Submonoid.powers a
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hP'_prime : P'.IsPrime
⊢ 0 ∉ M

Tactic:
have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ =>
    hp0 <| leadingCoeff_eq_zero.mp (eq_zero_of_pow_eq_zero hn)