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ₘ φ ⋯
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ₘ
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥
have hSₘ : IsJacobsonRing Sₘ
Tactic: have hSₘ : IsJacobsonRing Sₘ := isJacobsonRing_of_isIntegral' φ' hφ'
-- 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ₘ φ ⋯
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 ⊥) ⊥
have refine : LE.le (α := Ideal S) (jacobson ⊥) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥)
Tactic: refine eq_bot_iff.mpr (le_trans ?_ (le_of_eq hϕ'))
-- 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ₘ φ ⋯
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 ⊥) (comap (F := S →+* Sₘ) (algebraMap S Sₘ) ⊥)
have 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}))
Tactic: rw [← hSₘ.out isRadical_bot_of_noZeroDivisors, comap_jacobson]
-- 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 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
⊢ Eq.{u_2 + 1} (α := Ideal S) (jacobson ⊥) ⊥
have suffices : ∀ (I : Ideal Sₘ), I.IsMaximal → IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
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⟩
-- 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 : IsDomain Sₘ := ⋯
φ' : Rₘ →+* Sₘ := IsLocalization.map (M := Submonoid.powers x) Sₘ φ ⋯
I : Ideal Sₘ
hI : I.IsMaximal
⊢ IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have this₁ : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
Tactic: have : (I.comap (algebraMap S Sₘ)).IsPrime := comap_isPrime _ I
-- 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 : IsPrime (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
⊢ IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have this₁ : IsPrime (comap φ' I)
Tactic: have : (I.comap φ').IsPrime := comap_isPrime φ' I
-- 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 : IsPrime (comap φ' I)
⊢ IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have this₁ : 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
-- 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 : IsPrime.{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)
have hcomm : φ'.comp (algebraMap R Rₘ) = RingHom.comp (algebraMap S Sₘ) φ
Tactic: have hcomm : φ'.comp (algebraMap R Rₘ) = (algebraMap S Sₘ).comp φ := IsLocalization.map_comp _
-- 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 : 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 (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have this₁ : IsMaximal (comap φ' I)
Tactic: have := isMaximal_comap_of_isIntegral_of_isMaximal' φ' hφ' I
-- 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 : IsMaximal (comap φ' I)
⊢ IsMaximal (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I)
have this₁ : IsMaximal (under R (comap φ' I))
Tactic: have := ((IsLocalization.isMaximal_iff_isMaximal_disjoint Rₘ x _).1 this).left
-- 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 : IsMaximal (under R (comap φ' I))
⊢ IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
have rwa : ∀ (this : IsMaximal (comap (F := R →+* Rₘ) (algebraMap R Rₘ) (comap φ' I))),
  IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
Tactic: rwa [under_def, comap_comap, hcomm, ← comap_comap] 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 : 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))
⊢ IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
have rwa₁ : ∀ (this : IsMaximal (comap (F := R →+* Sₘ) (φ'.comp (algebraMap R Rₘ)) I)),
  IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
Tactic: rwa [under_def, comap_comap, hcomm, ← comap_comap] 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 : 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))
⊢ IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
have rwa₂ : ∀ (this : IsMaximal (comap (F := R →+* Sₘ) (RingHom.comp (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
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 : 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))
⊢ IsMaximal (comap φ (comap (F := S →+* Sₘ) (algebraMap S Sₘ) I))
have rwa₃ : ∀ (this : 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
Cleared hypotheses: this