-- Mathlib/RingTheory/Jacobson/Polynomial.lean
theorem jacobson_bot_polynomial_le_sInf_map_maximal :
    jacobson (⊥ : Ideal R[X]) ≤ sInf (map (C : R →+* R[X]) '' { J : Ideal R | J.IsMaximal })

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
r1 : X ≠ 0
⊢ f ∈ ⊥

Tactic:
simpa [r1] using eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit ((mem_jacobson_bot.1 hf) X))

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
⊢ ⊥.jacobson ≤ J

Tactic:
haveI : j.IsMaximal := hj.1

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ ⊥.jacobson ≤ J

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ J.jacobson = J

Tactic:
suffices t : (⊥ : Ideal (Polynomial (R ⧸ j))).jacobson = ⊥ by
  rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]
  replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t
  rwa [map_jacobson_of_bijective _, map_bot] at t
  exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ ⊥.jacobson = ⊥

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ ⊥.jacobson ≤ sInf (map C '' {J | J.IsMaximal})

Tactic:
refine le_sInf fun J => exists_imp.2 fun j hj => ?_

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
⊢ ⊥.jacobson ≤ J

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
⊢ (fun x => x.coeff 1) X ≠ (fun x => x.coeff 1) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ J.jacobson = J

Tactic:
rw [← hj.2, jacobson_eq_iff_jacobson_quotient_eq_bot]

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ ⊥.jacobson = ⊥

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t :
  map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥.jacobson =
    map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥
⊢ ⊥.jacobson = ⊥

Tactic:
rwa [map_jacobson_of_bijective _, map_bot] at t

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t :
  map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥.jacobson =
    map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥
⊢ Function.Bijective ⇑j.polynomialQuotientEquivQuotientPolynomial.toRingHom

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t :
  map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥.jacobson =
    map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥
⊢ Function.Bijective ⇑j.polynomialQuotientEquivQuotientPolynomial.toRingHom

Tactic:
exact RingEquiv.bijective (polynomialQuotientEquivQuotientPolynomial j)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ ⊥.jacobson ≤ J

Tactic:
refine Trans.trans (jacobson_mono bot_le) (le_of_eq ?_ : J.jacobson ≤ J)

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ J.jacobson = J

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
⊢ ⊥.jacobson = ⊥

Tactic:
refine eq_bot_iff.2 fun f hf => ?_

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
f : (R ⧸ j)[X]
hf : f ∈ ⊥.jacobson
⊢ f ∈ ⊥

Proof state:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t : ⊥.jacobson = ⊥
⊢ ⊥.jacobson = ⊥

Tactic:
replace t := congr_arg (map (polynomialQuotientEquivQuotientPolynomial j).toRingHom) t

Result:
R : Type u_1
inst✝ : CommRing R
J : Ideal R[X]
j : Ideal R
hj : j ∈ {J | J.IsMaximal} ∧ map C j = J
this : j.IsMaximal
t :
  map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥.jacobson =
    map j.polynomialQuotientEquivQuotientPolynomial.toRingHom ⊥
⊢ ⊥.jacobson = ⊥