-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_of_surjective [H : IsJacobsonRing R] :
    (∃ f : R →+* S, Function.Surjective ↑f) → IsJacobsonRing S

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ (∀ J ∈ Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal}, J.IsMaximal ∨ J = ⊤) ∧
    p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm

Result:
case right
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Proof state:
case right
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
this : p = Ideal.map f (comap f p).jacobson
⊢ p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
exact this.trans (map_sInf hf fun J ⟨hJ, _⟩ => le_trans (Ideal.ker_le_comap f) hJ)

Result:
no goals

Proof state:
case right
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Tactic:
have : p = map f (comap f p).jacobson :=
  (IsJacobsonRing.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm

Result:
case right
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
this : p = Ideal.map f (comap f p).jacobson
⊢ p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ p = sInf M

Tactic:
use map f '' { J : Ideal R | comap f p ≤ J ∧ J.IsMaximal }

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ (∀ J ∈ Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal}, J.IsMaximal ∨ J = ⊤) ∧
    p = sInf (Ideal.map f '' {J | comap f p ≤ J ∧ J.IsMaximal})

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ IsJacobsonRing S

Tactic:
rw [isJacobsonRing_iff_sInf_maximal]

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ {I : Ideal S}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
⊢ (∃ f, Function.Surjective ⇑f) → IsJacobsonRing S

Tactic:
rintro ⟨f, hf⟩

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ IsJacobsonRing S

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ {I : Ideal S}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Tactic:
intro p hp

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective ⇑f
p : Ideal S
hp : p.IsPrime
⊢ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ p = sInf M