-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_polynomial_of_isJacobsonRing (hR : IsJacobsonRing R) :
    IsJacobsonRing R[X]

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
⊢ I.jacobson = 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]

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ I.jacobson = I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ f.coeff n ∈ comap C I

Tactic:
replace hf := congrArg (fun g : Polynomial ((Ideal.Quotient.mk I).comp C).range => g.coeff n) hf

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : (fun g => g.coeff n) ((mapRingHom i) f) = (fun g => g.coeff n) 0
⊢ f.coeff n ∈ comap C I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : (fun g => g.coeff n) ((mapRingHom i) f) = (fun g => g.coeff n) 0
⊢ f.coeff n ∈ comap C I

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

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
n : ℕ
hf : (map ((Ideal.Quotient.mk I).comp C).rangeRestrict f).coeff n = 0
⊢ f.coeff n ∈ comap C I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
⊢ ∀ (x : ↥R'), C x ∈ J → x = 0

Tactic:
exact eq_zero_of_polynomial_mem_map_range I

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson = I

Tactic:
refine le_antisymm ?_ le_jacobson

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
h : I.jacobson ⊔ comap (mapRingHom i) ⊥ = I ⊔ comap (mapRingHom i) ⊥
⊢ I.jacobson ≤ I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
⊢ 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'))

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
this : J.IsPrime
⊢ J.jacobson = J

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
J : Ideal (↥R')[X] := Ideal.map (mapRingHom i) I
h_surj : Function.Surjective ⇑(mapRingHom i)
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'))

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ I.jacobson = I

Tactic:
have R'_jacob : IsJacobsonRing R' := isJacobsonRing_of_surjective ⟨i, hi⟩

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
hi' : RingHom.ker (mapRingHom i) ≤ I
R'_jacob : IsJacobsonRing ↥R'
⊢ I.jacobson = I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
⊢ I.jacobson = I

Tactic:
let R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
⊢ I.jacobson = I

Proof state:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
⊢ RingHom.ker (mapRingHom i) ≤ I

Tactic:
intro f hf

Result:
R : Type u_1
inst✝ : CommRing R
hR : IsJacobsonRing R
I : Ideal R[X]
hI : I.IsPrime
R' : Subring (R[X] ⧸ I) := ((Ideal.Quotient.mk I).comp C).range
i : R →+* ↥R' := ((Ideal.Quotient.mk I).comp C).rangeRestrict
hi : Function.Surjective ⇑i
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
⊢ f ∈ I