-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem jacobson_bot_of_integral_localization
    {R : Type*} [CommRing R] [IsDomain R] [IsJacobsonRing R]
    (Rₘ Sₘ : Type*) [CommRing Rₘ] [CommRing Sₘ] (φ : R →+* S) (hφ : Function.Injective ↑φ) (x : R)
    (hx : x ≠ 0) [Algebra R Rₘ] [IsLocalization.Away x Rₘ] [Algebra S Sₘ]
    [IsLocalization ((Submonoid.powers x).map φ : Submonoid S) Sₘ]
    (hφ' :
      RingHom.IsIntegral (IsLocalization.map Sₘ φ (Submonoid.powers x).le_comap_map : Rₘ →+* Sₘ)) :
    (⊥ : Ideal S).jacobson = (⊥ : Ideal S)

Proof state:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝⁵ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝⁴ : (comap (algebraMap S Sₘ) I).IsPrime
this✝³ : (comap φ' I).IsPrime
this✝² : ⊥.IsPrime
hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ
f : R ⧸ comap φ (comap (algebraMap S Sₘ) I) →+* S ⧸ comap (algebraMap S Sₘ) I :=
  quotientMap (comap (algebraMap S Sₘ) I) φ ⋯
g : S ⧸ comap (algebraMap S Sₘ) I →+* Sₘ ⧸ I := quotientMap I (algebraMap S Sₘ) ⋯
this✝¹ : (comap φ' I).IsMaximal
this✝ : (comap (algebraMap R Rₘ) (comap φ' I)).IsMaximal
this : ⊥.IsMaximal
⊢ f.IsIntegral

Tactic:
exact RingHom.IsIntegral.tower_bot f g quotientMap_injective
  ((comp_quotientMap_eq_of_comp_eq hcomm I).symm ▸
    (RingHom.isIntegral_of_surjective _
      (IsLocalization.surjective_quotientMap_of_maximal_of_localization (Submonoid.powers x) Rₘ
        (by rwa [comap_comap, hcomm, ← bot_quotient_isMaximal_iff]))).trans _ _ (hφ'.quotient _))

Result:
no goals

Proof state:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ comap (algebraMap S Sₘ) ⊥

Tactic:
rw [← hSₘ.out isRadical_bot_of_noZeroDivisors, comap_jacobson]

Result:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal
hϕ' : comap (algebraMap S Sₘ) ⊥ = ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ ⊥.jacobson ≤ sInf (comap (algebraMap S Sₘ) '' {J | ⊥ ≤ J ∧ J.IsMaximal})

Proof state:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this : (comap (algebraMap S Sₘ) I).IsPrime
⊢ (comap (algebraMap S Sₘ) I).IsMaximal

Tactic:
haveI : (I.comap φ').IsPrime := comap_isPrime φ' I

Result:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this✝¹ : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this✝ : (comap (algebraMap S Sₘ) I).IsPrime
this : (comap φ' I).IsPrime
⊢ (comap (algebraMap S Sₘ) I).IsMaximal

Proof state:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
⊢ ∀ (I : Ideal Sₘ), I.IsMaximal → (comap (algebraMap S Sₘ) I).IsMaximal

Tactic:
intro I hI

Result:
S : Type u_2
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
R : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst✝⁵ : CommRing Rₘ
inst✝⁴ : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective ⇑φ
x : R
hx : x ≠ 0
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization.Away x Rₘ
inst✝¹ : Algebra S Sₘ
inst✝ : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral
hM : Submonoid.map φ (Submonoid.powers x) ≤ nonZeroDivisors S
this : IsDomain Sₘ := IsLocalization.isDomain_of_le_nonZeroDivisors S hM
φ' : Rₘ →+* Sₘ := IsLocalization.map Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
⊢ (comap (algebraMap S Sₘ) I).IsMaximal