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ₘ φ ⋯
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.{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)) ⊥

Tactic:
isMaximal_of_isIntegral_of_isMaximal_comap' f ?_ ⊥
    ((eq_bot_iff.2 (comap_bot_le_of_injective f quotientMap_injective)).symm ▸ this)

Premises used: Iff.mpr, Ideal.comap_bot_le_of_injective, Ideal.isMaximal_of_isIntegral_of_isMaximal_comap', Eq.rec, Bot.bot, Ideal.quotientMap_injective, eq_bot_iff, Eq.symm
-- 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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
refine : f.IsIntegral
⊢ IsMaximal.{u_2} (α := HasQuotient.Quotient S (B := Ideal S) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)) ⊥

Tactic:
refine isMaximal_of_isIntegral_of_isMaximal_comap' f ?_ ⊥
    ((eq_bot_iff.2 (comap_bot_le_of_injective f quotientMap_injective)).symm ▸ this)

Premises used: Iff.mpr, Ideal.comap_bot_le_of_injective, Ideal.isMaximal_of_isIntegral_of_isMaximal_comap', Eq.rec, Bot.bot, Ideal.quotientMap_injective, eq_bot_iff, Eq.symm
-- 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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
apply : (g.comp f).IsIntegral
⊢ f.IsIntegral

Tactic:
apply RingHom.IsIntegral.tower_bot f g quotientMap_injective

Premises used: RingHom.IsIntegral.tower_bot, Ideal.quotientMap_injective
-- 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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
rw :
  RingHom.IsIntegral (R := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I φ' ⋯)
      (quotientMap (comap φ' I) (algebraMap R Rₘ) ⋯))
⊢ (g.comp f).IsIntegral

Tactic:
rw [comp_quotientMap_eq_of_comp_eq hcomm]

Premises used: Ideal.comp_quotientMap_eq_of_comp_eq
-- 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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
⊢ RingHom.IsIntegral (R := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I φ' ⋯)
      (quotientMap (comap φ' I) (algebraMap R Rₘ) ⋯))

Tactic:
RingHom.IsIntegral.trans _ _ (RingHom.isIntegral_of_surjective _ ?_) (hφ'.quotient _)

Premises used: RingHom.isIntegral_of_surjective, RingHom.IsIntegral.quotient, RingHom.IsIntegral.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ₘ φ ⋯
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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
refine :
  Function.Surjective.{u_5 + 1, u_6 + 1} (α :=
    HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) (β :=
    HasQuotient.Quotient Rₘ (B := Ideal Rₘ) (comap φ' I))
    (⇑(quotientMap (comap φ' I) (algebraMap R Rₘ) ⋯) : (a : R ⧸ comap φ (comap (algebraMap S Sₘ) I)) → Rₘ ⧸ comap φ' I)
⊢ RingHom.IsIntegral (R := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (quotientMap I φ' ⋯)
      (quotientMap (comap φ' I) (algebraMap R Rₘ) ⋯))

Tactic:
refine RingHom.IsIntegral.trans _ _ (RingHom.isIntegral_of_surjective _ ?_) (hφ'.quotient _)

Premises used: RingHom.isIntegral_of_surjective, RingHom.IsIntegral.quotient, RingHom.IsIntegral.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ₘ φ ⋯
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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
hI₁ : IsMaximal (under R (comap φ' I))
⊢ Function.Surjective.{u_5 + 1, u_6 + 1} (α :=
    HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) (β :=
    HasQuotient.Quotient Rₘ (B := Ideal Rₘ) (comap φ' I))
    (⇑(quotientMap (comap φ' I) (algebraMap R Rₘ) ⋯) : (a : R ⧸ comap φ (comap (algebraMap S Sₘ) I)) → Rₘ ⧸ comap φ' I)

Tactic:
apply IsLocalization.surjective_quotientMap_of_maximal_of_localization (Submonoid.powers x)

Premises used: IsLocalization.surjective_quotientMap_of_maximal_of_localization, Submonoid.powers
-- 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.{u_5} (α := HasQuotient.Quotient R (B := Ideal R) (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))) ⊥
hI₁ : IsMaximal (comap (F := R →+* Rₘ) (algebraMap R Rₘ) (comap φ' I))
hI₂ : IsMaximal (comap (F := R →+* Sₘ) (φ'.comp (algebraMap R Rₘ)) I)
hI₃ : IsMaximal (comap (F := R →+* Sₘ) (RingHom.comp (algebraMap S Sₘ) φ) I)
hI₄ hI₅ hI₆ hI₇ :
  IsMaximal.{u_5} (α :=
    HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* Sₘ) (RingHom.comp (algebraMap S Sₘ) φ) I)) ⊥
⊢ IsMaximal (under R (comap φ' I))

Tactic:
rwa [under_def, comap_comap, hcomm, ← bot_quotient_isMaximal_iff]

Premises used: Ideal.under_def, Ideal.bot_quotient_isMaximal_iff, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
pos : ∀ (Pb : P = ⊥), P.jacobson = P
neg : ∀ (Pb : ¬P = ⊥), P.jacobson = P
⊢ P.jacobson = P

Tactic:
by_cases Pb : P = ⊥
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : P = ⊥
⊢ P.jacobson = P

Tactic:
Pb.symm ▸
      jacobson_bot_polynomial_of_jacobson_bot (hR.out isRadical_bot_of_noZeroDivisors)

Premises used: Eq.rec, IsJacobsonRing.out, Ideal.isRadical_bot_of_noZeroDivisors, Ideal.jacobson_bot_polynomial_of_jacobson_bot, Eq.symm
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : P = ⊥
⊢ P.jacobson = P

Tactic:
exact Pb.symm ▸
      jacobson_bot_polynomial_of_jacobson_bot (hR.out isRadical_bot_of_noZeroDivisors)
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
neg : Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
⊢ P.jacobson = P

Tactic:
rw [jacobson_eq_iff_jacobson_quotient_eq_bot]

Premises used: Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
⊢ P'.IsPrime

Tactic:
have : P'.IsPrime := comap_isPrime C P
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
⊢ IsJacobsonRing.{u_5} (R ⧸ P')

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
⊢ IsJacobsonRing.{u_5} (R ⧸ P')

Tactic:
have hR' : IsJacobsonRing (R ⧸ P') := by infer_instance
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
neg :
  ∀ (p : R[X]) (pP : p ∈ P)
    (p0 :
      Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
        (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0),
    Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥

Tactic:
obtain ⟨p, pP, p0⟩ := exists_nonzero_mem_of_ne_bot Pb hP

Premises used: Ideal.exists_nonzero_mem_of_ne_bot
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
rwa : ¬x = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ¬map (Ideal.Quotient.mk P') p = 0
⊢ x ≠ 0

Tactic:
rwa [Ne, leadingCoeff_eq_zero]

Premises used: Ne, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := by rwa [Ne, leadingCoeff_eq_zero]
-- Module: Mathlib.RingTheory.Jacobson.Ring
Goal:
R : Type u_5
inst : CommRing R
inst_1 : IsDomain R
hR : IsJacobsonRing R
P : Ideal R[X]
inst_2 : P.IsPrime
hP : ∀ (x : R), Membership.mem (α := R[X]) P ((C : (a : R) → R[X]) x : R[X]) → x = 0
Pb : ¬P = ⊥
P' : Ideal R := comap (F := R →+* R[X]) C P
this : P'.IsPrime
hR' : IsJacobsonRing.{u_5} (R ⧸ P')
p : R[X]
pP : p ∈ P
p0 :
  Ne (α := (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* R[X]) C P))[X])
    (map (Ideal.Quotient.mk (comap (F := R →+* R[X]) C P)) p) 0
x : R ⧸ P' := (map (Ideal.Quotient.mk P') p).leadingCoeff
hx : x ≠ 0
φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C ⋯
hφ : Function.Injective (α := R ⧸ P') (β := R[X] ⧸ P) (⇑φ : (a : R ⧸ P') → R[X] ⧸ P) := ⋯
Rₘ : Type u_5 := Localization.Away x
Sₘ : Type u_5 := Localization (Submonoid.map φ (Submonoid.powers x))
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥

Tactic:
jacobson_bot_of_integral_localization (S := R[X] ⧸ P) (R := R ⧸ P') Rₘ Sₘ _ hφ _ hx ?_

Premises used: Polynomial.jacobson_bot_of_integral_localization