-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_of_isIntegral [Algebra R S] [Algebra.IsIntegral R S] [IsJacobsonRing R] :
    IsJacobsonRing S

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this✝ : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ ∃ x, x.IsMaximal ∧ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) x = J

Tactic:
exact exists_ideal_over_maximal_of_isIntegral J
  (comap_bot_le_of_injective _ algebraMap_quotient_injective)

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ sInf (comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}) ≤ ⊥.jacobson

Tactic:
refine sInf_le_sInf fun J hJ => ?_

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ J ∈ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : comap (algebraMap R S) P = ⊤
⊢ P.jacobson = P

Tactic:
simp [comap_eq_top_iff.1 hP_top]

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ ∃ x, x.IsMaximal ∧ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) x = J

Tactic:
have : J.IsMaximal := by simpa using hJ

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this✝ : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ ∃ x, x.IsMaximal ∧ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) x = J

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P

Tactic:
intro P hP

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
⊢ P.jacobson = P

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_prime_eq]

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
⊢ ∀ (P : Ideal S), P.IsPrime → P.jacobson = P

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ J.IsMaximal

Tactic:
simpa using hJ

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) ⊥.jacobson = ⊥

Tactic:
rw [eq_bot_iff, ← jacobson_eq_iff_jacobson_quotient_eq_bot.1
  ((isJacobsonRing_iff_prime_eq.1 ‹_›) (comap (algebraMap R S) P) (comap_isPrime _ _)),
  comap_jacobson]

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ sInf (comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}) ≤ ⊥.jacobson

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
⊢ P.jacobson = P

Tactic:
by_cases hP_top : comap (algebraMap R S) P = ⊤

Result:
case pos
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : comap (algebraMap R S) P = ⊤
⊢ P.jacobson = P

case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
⊢ P.jacobson = P

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ J ∈ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) '' {J | ⊥ ≤ J ∧ J.IsMaximal}

Tactic:
simp only [true_and, Set.mem_image, bot_le, Set.mem_setOf_eq]

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
J : Ideal (R ⧸ comap (algebraMap R S) P)
hJ : J ∈ {J | ⊥ ≤ J ∧ J.IsMaximal}
⊢ ∃ x, x.IsMaximal ∧ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) x = J

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
⊢ P.jacobson = P

Tactic:
haveI : Nontrivial (R ⧸ comap (algebraMap R S) P) := Quotient.nontrivial hP_top

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ P.jacobson = P