awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥

Tactic:
eq_bot_iff.mpr (le_trans ?_ (le_of_eq hϕ'))

Premises used: Iff.mpr, le_of_eq, eq_bot_iff, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
refine : LE.le (α := Ideal S) (jacobson ⊥) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥)
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥

Tactic:
refine eq_bot_iff.mpr (le_trans ?_ (le_of_eq hϕ'))

Premises used: Iff.mpr, le_of_eq, eq_bot_iff, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
rw :
  LE.le (α := Ideal S) (jacobson ⊥)
    (sInf
      (Set.image (α := Ideal Sₘ) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ))
        {J : Ideal Sₘ | ⊥ ≤ J ∧ J.IsMaximal}))
⊢ LE.le (α := Ideal S) (jacobson ⊥) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥)

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

Premises used: IsJacobsonRing.out, Ideal.isRadical_bot_of_noZeroDivisors, Ideal.comap_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ LE.le (α := Ideal S) (jacobson ⊥)
    (sInf
      (Set.image (α := Ideal Sₘ) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ))
        {J : Ideal Sₘ | ⊥ ≤ J ∧ J.IsMaximal}))

Tactic:
sInf_le_sInf fun j hj => ⟨bot_le,
      let ⟨J, hJ⟩ := hj
      hJ.2 ▸ this J hJ.1.2⟩

Premises used: Set.Mem, sInf_le_sInf, Eq.rec, _private.0.Polynomial.jacobson_bot_of_integral_localization.match_1, And.right, And.left, And.intro, Ideal.IsMaximal, bot_le
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
this : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
hϕ' : Eq (α := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥) ⊥
hRₘ : IsJacobsonRing Rₘ
hSₘ : IsJacobsonRing Sₘ
⊢ LE.le (α := Ideal S) (jacobson ⊥)
    (sInf
      (Set.image (α := Ideal Sₘ) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ))
        {J : Ideal Sₘ | ⊥ ≤ J ∧ J.IsMaximal}))

Tactic:
exact sInf_le_sInf fun j hj => ⟨bot_le,
      let ⟨J, hJ⟩ := hj
      hJ.2 ▸ this J hJ.1.2⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
suffices : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥

Tactic:
suffices ∀ I : Ideal Sₘ, I.IsMaximal → (I.comap (algebraMap S Sₘ)).IsMaximal by
    have hϕ' : comap (algebraMap S Sₘ) (⊥ : Ideal Sₘ) = (⊥ : Ideal S) := by
      rw [← RingHom.ker_eq_comap_bot, ← RingHom.injective_iff_ker_eq_bot]
      exact IsLocalization.injective Sₘ hM
    have hRₘ : IsJacobsonRing Rₘ := isJacobsonRing_localization x
    have hSₘ : IsJacobsonRing Sₘ := isJacobsonRing_of_isIntegral' φ' hφ'
    refine eq_bot_iff.mpr (le_trans ?_ (le_of_eq hϕ'))
    rw [← hSₘ.out isRadical_bot_of_noZeroDivisors, comap_jacobson]
    exact sInf_le_sInf fun j hj => ⟨bot_le,
      let ⟨J, hJ⟩ := hj
      hJ.2 ▸ this J hJ.1.2⟩
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
⊢ IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)

Tactic:
have : (I.comap (algebraMap S Sₘ)).IsPrime := comap_isPrime _ I
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
⊢ IsPrime (comap φ' I)

Tactic:
have : (I.comap φ').IsPrime := comap_isPrime φ' I
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this : IsPrime (comap φ' I)
⊢ IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥

Tactic:
have : (⊥ : Ideal (S ⧸ I.comap (algebraMap S Sₘ))).IsPrime := isPrime_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this_3 : IsPrime (comap φ' I)
this : IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
⊢ φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ

Tactic:
have hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ := IsLocalization.map_comp _
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this_3 : IsPrime (comap φ' I)
this : IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
hcomm : φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ
f : RingHom.{u_5, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
  (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) :=
  quotientMap (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I) φ ⋯
g : RingHom.{u_2, u_7} (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ) I))
  (Sₘ ⧸ I) :=
  quotientMap I (algebraMap S Sₘ) ⋯
⊢ IsMaximal (comap φ' I)

Tactic:
have := isMaximal_comap_of_isIntegral_of_isMaximal' φ' hφ' I
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this_3 : IsPrime (comap φ' I)
this_4 : IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
hcomm : φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ
f : RingHom.{u_5, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
  (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) :=
  quotientMap (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I) φ ⋯
g : RingHom.{u_2, u_7} (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ) I))
  (Sₘ ⧸ I) :=
  quotientMap I (algebraMap S Sₘ) ⋯
this : IsMaximal (comap φ' I)
⊢ IsMaximal (under R (comap φ' I))

Tactic:
have := ((IsLocalization.isMaximal_iff_isMaximal_disjoint Rₘ x _).1 this).left
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this_3 : IsPrime (comap φ' I)
this_4 : IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
hcomm : φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ
f : RingHom.{u_5, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
  (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) :=
  quotientMap (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I) φ ⋯
g : RingHom.{u_2, u_7} (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ) I))
  (Sₘ ⧸ I) :=
  quotientMap I (algebraMap S Sₘ) ⋯
this_5 : IsMaximal (comap φ' I)
this : IsMaximal (under R (comap φ' I))
rwa :
  ∀ (this : IsMaximal (comap (F := R →+* Rₘ) (algebraMap R Rₘ) (comap φ' I))),
    IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
rwa₁ :
  ∀ (this : IsMaximal (comap (F := R →+* Sₘ) (φ'.comp (algebraMap R Rₘ)) I)),
    IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
rwa₂ :
  ∀ (this : IsMaximal (comap (F := R →+* Sₘ) (RingHom.comp (algebraMap S Sₘ) φ) I)),
    IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (this : IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))),
    IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
⊢ IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))

Tactic:
rwa [under_def, comap_comap, hcomm, ← comap_comap] at this

Premises used: Ideal.under_def, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this_3 : IsPrime (comap φ' I)
this_4 : IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
hcomm : φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ
f : RingHom.{u_5, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
  (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) :=
  quotientMap (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I) φ ⋯
g : RingHom.{u_2, u_7} (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ) I))
  (Sₘ ⧸ I) :=
  quotientMap I (algebraMap S Sₘ) ⋯
this_5 : IsMaximal (comap φ' I)
this : IsMaximal (under R (comap φ' I))
⊢ IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))

Tactic:
have : ((I.comap (algebraMap S Sₘ)).comap φ).IsMaximal := by
    rwa [under_def, comap_comap, hcomm, ← comap_comap] at this
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDomain S
R : Type u_5
inst_2 : CommRing R
inst_3 : IsDomain R
inst_4 : IsJacobsonRing R
Rₘ : Type u_6
Sₘ : Type u_7
inst_5 : CommRing Rₘ
inst_6 : CommRing Sₘ
φ : R →+* S
hφ : Function.Injective.{u_5 + 1, u_2 + 1} (α := R) (β := S) (⇑φ : (a : R) → S)
x : R
hx : x ≠ 0
inst_7 : Algebra R Rₘ
inst_8 : IsLocalization.Away x Rₘ
inst_9 : Algebra S Sₘ
inst_10 : IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ
hφ' : RingHom.IsIntegral.{u_6, u_7} (R := Rₘ) (A := Sₘ) (IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯)
hM : LE.le (α := Submonoid S) (Submonoid.map φ (Submonoid.powers x) : Submonoid S) (nonZeroDivisors S : Submonoid S)
this_1 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
this_2 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
this_3 : IsPrime (comap φ' I)
this_4 : IsPrime.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
hcomm : φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ
f : RingHom.{u_5, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
  (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) :=
  quotientMap (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I) φ ⋯
g : RingHom.{u_2, u_7} (HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ : S →+* Sₘ) I))
  (Sₘ ⧸ I) :=
  quotientMap I (algebraMap S Sₘ) ⋯
this_5 : IsMaximal (comap φ' I)
this_6 : IsMaximal (under R (comap φ' I))
this : IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
rw :
  ∀
    (this :
      IsMaximal.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
        ⊥),
    IsMaximal.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥
⊢ IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)

Tactic:
rw [← bot_quotient_isMaximal_iff] at this ⊢

Premises used: Ideal.bot_quotient_isMaximal_iff