awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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 (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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))
⊢ IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have 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)) ⊥
Tactic: rw [← bot_quotient_isMaximal_iff] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)) ⊥
have refine : f.IsIntegral
Tactic: refine isMaximal_of_isIntegral_of_isMaximal_comap' f ?_ ⊥
    ((eq_bot_iff.2 (comap_bot_le_of_injective f quotientMap_injective)).symm ▸ this)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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))) ⊥
⊢ f.IsIntegral
have apply : (g.comp f).IsIntegral
Tactic: apply RingHom.IsIntegral.tower_bot f g quotientMap_injective
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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))) ⊥
⊢ (g.comp f).IsIntegral
have 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 φ' sorry)
    (quotientMap (comap φ' I) (algebraMap R Rₘ) sorry))
Tactic: rw [comp_quotientMap_eq_of_comp_eq hcomm]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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ₘ) ⋯))
have 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ₘ) sorry) : (a : R ⧸ comap φ (comap (algebraMap S Sₘ) I)) → Rₘ ⧸ comap φ' I)
Tactic: refine RingHom.IsIntegral.trans _ _ (RingHom.isIntegral_of_surjective _ ?_) (hφ'.quotient _)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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 (under R (comap φ' I))
have hI₁ : IsMaximal (comap (F := R →+* Rₘ) (algebraMap R Rₘ) (comap φ' I))
Tactic: rwa [under_def, comap_comap, hcomm, ← bot_quotient_isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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))
⊢ IsMaximal (under R (comap φ' I))
have hI₂ : IsMaximal (comap (F := R →+* Sₘ) (φ'.comp (algebraMap R Rₘ)) I)
Tactic: rwa [under_def, comap_comap, hcomm, ← bot_quotient_isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
⊢ IsMaximal (under R (comap φ' I))
have hI₃ : IsMaximal (comap (F := R →+* Sₘ) (RingHom.comp (algebraMap S Sₘ) φ) I)
Tactic: rwa [under_def, comap_comap, hcomm, ← bot_quotient_isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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)
⊢ IsMaximal (under R (comap φ' I))
have hI₄ : IsMaximal.{u_5} (α :=
  HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* Sₘ) (RingHom.comp (algebraMap S Sₘ) φ) I)) ⊥
Tactic: rwa [under_def, comap_comap, hcomm, ← bot_quotient_isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ P.jacobson = P
have pos : ∀ (Pb : P = ⊥), P.jacobson = P
Tactic: by_cases Pb : P = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
⊢ P.jacobson = P
have neg : ∀ (Pb : ¬P = ⊥), P.jacobson = P
Tactic: by_cases Pb : P = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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
have neg : Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
Tactic: rw [jacobson_eq_iff_jacobson_quotient_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
have this : P'.IsPrime
Tactic: have : P'.IsPrime := comap_isPrime C P
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
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
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
have hR' : IsJacobsonRing.{u_5} (R ⧸ P')
Tactic: have hR' : IsJacobsonRing (R ⧸ P') := by infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
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')
⊢ Eq.{u_5 + 1} (α := Ideal (R[X] ⧸ P)) (jacobson ⊥) ⊥
have 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 ⊥) ⊥
Tactic: obtain ⟨p, pP, p0⟩ := exists_nonzero_mem_of_ne_bot Pb hP