awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
f : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
rw : (↑(Submodule.map f (Module.jacobson R (R ⧸ I))) : Set (R ⧸ I)) = (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I))
⊢ (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) = (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I))
have rw₁ : f.ker ≤ Module.jacobson R (R ⧸ I)
Tactic: rw [jacobson, ← Module.map_jacobson_of_ker_le (f := f) Function.surjective_id]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
le : I ≤ jacobson R
⊢ LinearMap.ker (τ₁₂ := Ideal.Quotient.mk I) (RingHom.toSemilinearMap (Ideal.Quotient.mk I)) ≤ Module.jacobson R R
have rwa : ∀
  (le :
    LE.le.{u_1} (α := Ideal R)
      (LinearMap.ker (R₂ := R) (M₂ := R ⧸ I) (τ₁₂ := RingHom.id R) (Submodule.mkQ I) : Submodule R R)
      (jacobson R : Ideal R)),
  LinearMap.ker (τ₁₂ := Ideal.Quotient.mk I) (RingHom.toSemilinearMap (Ideal.Quotient.mk I)) ≤ Module.jacobson R R
Tactic: rwa [← I.ker_mkQ] at le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
h : Eq.{u_1 + 1} (α := Ideal (R ⧸ I)) (jacobson (R ⧸ I)) ⊥
⊢ Eq (α := Submodule R (R ⧸ I)) (Module.jacobson R (R ⧸ I)) ⊥
have rw : ∀ (h : (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))),
  (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
Tactic: rw [← le_bot_iff, ← SetLike.coe_subset_coe] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
h : (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
⊢ (↑(Module.jacobson R (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
have rwa : (↑(jacobson (R ⧸ I)) : Set (R ⧸ I)) ⊆ (↑⊥ : Set (R ⧸ I))
Tactic: rwa [← coe_jacobson_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : N.FG
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N < N
have fg₁ : Module.Finite.{u_1, u_3} R ↥N
Tactic: rw [← Module.Finite.iff_fg] at fg
Cleared hypotheses: fg
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : N ≠ ⊥
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N < N
have ne_bot₁ : Nontrivial.{u_3} ↥N
Tactic: rw [← nontrivial_iff_ne_bot] at ne_bot
Cleared hypotheses: ne_bot, fg
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N < N
have h : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
  Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)
Tactic: convert! map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h :
  HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N < N
have h₁ : N = Submodule.map N.subtype ⊤
Tactic: convert! map_strictMono_of_injective N.injective_subtype (jacobson_smul_lt_top ⊤)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)
have h : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
  HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)
Tactic: rw [map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    Submodule.map N.subtype (HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (Ring.jacobson R) ⊤)
have h : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
  HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)
Tactic: on_goal 1 => rw [map_smul'']
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)
have h : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N = HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N.subtype.range
Tactic: rw [Submodule.map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N = HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N.subtype.range
⊢ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N =
    HSMul.hSMul (α := Ideal R) (Ring.jacobson R) (Submodule.map N.subtype ⊤)
have h₁ : HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N = HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
Tactic: rw [Submodule.map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
⊢ N = Submodule.map N.subtype ⊤
have h : N = N.subtype.range
Tactic: rw [Submodule.map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
ne_bot : Nontrivial.{u_3} ↥N
fg : Module.Finite.{u_1, u_3} R ↥N
h : N = N.subtype.range
⊢ N = Submodule.map N.subtype ⊤
have h₁ : N = N
Tactic: rw [Submodule.map_top, range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Radical (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
fg : N.FG
le : N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
⊢ N = ⊥
have contrapose! : ∀ (le : N ≠ ⊥), ¬N ≤ HSMul.hSMul (α := Ideal R) (Ring.jacobson R) N
Tactic: contrapose! le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ IsJacobsonRing R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
have refine : (∀ (P : Ideal R), P.IsPrime → P.jacobson = P) → ∀ (I : Ideal R), I.IsRadical → I.jacobson = I
Tactic: refine isJacobsonRing_iff.trans ⟨fun h I hI => h I hI.isRadical, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ (∀ (P : Ideal R), P.IsPrime → P.jacobson = P) → ∀ (I : Ideal R), I.IsRadical → I.jacobson = I
have refine : ∀ (h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P) (I : Ideal R) (hI : I.IsRadical) (x : R) (hx : x ∈ I.jacobson),
  x ∈ I
Tactic: refine fun h I hI ↦ le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ mem_sInf.mpr fun _ hJ ↦ hJ.left hx)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I
have rw : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} I_1 → x ∈ I_1
Tactic: rw [← hI.radical, radical_eq_sInf I, mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} P
⊢ x ∈ P
have hP₁ : I ≤ P ∧ P.IsPrime
Tactic: rw [Set.mem_setOf_eq] at hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : x ∈ I.jacobson
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P
have rw : ∀ (hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1)
  ⦃P : Ideal R⦄ (hP : I ≤ P ∧ P.IsPrime), x ∈ P
Tactic: rw [jacobson, mem_sInf] at hx
Cleared hypotheses: hx, P, hP
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
I : Ideal R
hI : I.IsRadical
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
P : Ideal R
hP : I ≤ P ∧ P.IsPrime
⊢ x ∈ P
have rw : ∀ ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | P ≤ J ∧ J.IsMaximal} I → x ∈ I
Tactic: rw [← h P hP.right, jacobson, mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ IsJacobsonRing S
have rw : ∀ {I : Ideal S}, I.IsPrime → ∃ (M : Set (Ideal S)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
Tactic: rw [isJacobsonRing_iff_sInf_maximal]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
⊢ ∃ (M : Set (Ideal S)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ p = sInf M
have h : (∀ (J : Ideal S),
    Membership.mem (γ := Set (Ideal S))
        (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal}) J →
      J.IsMaximal ∨ J = ⊤) ∧
  p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})
Tactic: use map f '' { J : Ideal R | comap f p ≤ J ∧ J.IsMaximal }
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
⊢ (∀ (J : Ideal S),
      Membership.mem (γ := Set (Ideal S))
          (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal}) J →
        J.IsMaximal ∨ J = ⊤) ∧
    p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})
have right : p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})
Tactic: use fun j ⟨J, hJ, hmap⟩ => hmap ▸ (map_eq_top_or_isMaximal_of_surjective f hf hJ.right).symm
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
H : IsJacobsonRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
hp : p.IsPrime
⊢ p = sInf (Set.image.{u_1, u_2} (α := Ideal R) (Ideal.map f) {J : Ideal R | comap f p ≤ J ∧ J.IsMaximal})
have this : p = Ideal.map f (jacobson (comap f p))
Tactic: have : p = map f (comap f p).jacobson :=
    (IsJacobsonRing.out' _ <| hp.isRadical.comap f).symm ▸ (map_comap_of_surjective f hf p).symm
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
inst_2 : IsJacobsonRing R
b : R ⧸ I
x : R
⊢ ∃ (a : R),
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x :
        Quot (α := R) (⇑(Submodule.quotientRel I) : R → R → Prop))
have h : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
  (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x : Quot (α := R) (⇑(Submodule.quotientRel I) : R → R → Prop))
Tactic: use x
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
⊢ IsJacobsonRing S
have rw : ∀ (P : Ideal S), P.IsPrime → P.jacobson = P
Tactic: rw [isJacobsonRing_iff_prime_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
⊢ P.jacobson = P
have pos : ∀ (hP_top : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤), P.jacobson = P
Tactic: by_cases hP_top : comap (algebraMap R S) P = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
pos : ∀ (hP_top : Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤), P.jacobson = P
⊢ P.jacobson = P
have neg : ∀ (hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤), P.jacobson = P
Tactic: by_cases hP_top : comap (algebraMap R S) P = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
⊢ Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
have rwa : Ne (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
Tactic: rwa [Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
⊢ P.jacobson = P
have this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
Tactic: have : Nontrivial (R ⧸ comap (algebraMap R S) P) := by rwa [Quotient.nontrivial_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
⊢ P.jacobson = P
have neg : Eq.{u_2 + 1} (α := Ideal (S ⧸ P)) (jacobson ⊥) ⊥
Tactic: rw [jacobson_eq_iff_jacobson_quotient_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
⊢ Eq.{u_2 + 1} (α := Ideal (S ⧸ P)) (jacobson ⊥) ⊥
have neg : Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
  (comap (F :=
    RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
    (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)) (jacobson ⊥))
  ⊥
Tactic: refine eq_bot_of_comap_eq_bot (R := R ⧸ comap (algebraMap R S) P) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
⊢ Eq (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (comap (F :=
      RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
      (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
      (jacobson ⊥))
    ⊥
have neg : LE.le (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
  (sInf
    (Set.image (α := Ideal (S ⧸ P))
      (comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
      {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal}))
  (jacobson ⊥)
Tactic: rw [eq_bot_iff, ← jacobson_eq_iff_jacobson_quotient_eq_bot.1
    ((isJacobsonRing_iff_prime_eq.1 ‹_›) (comap (algebraMap R S) P) (comap_isPrime _ _)),
    comap_jacobson]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
⊢ LE.le (α := Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
    (sInf
      (Set.image (α := Ideal (S ⧸ P))
        (comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
        {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal}))
    (jacobson ⊥)
have neg : ∀ (J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)))
  (hJ :
    Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
      {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) |
        ⊥ ≤ J ∧ J.IsMaximal}
      J),
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    (Set.image (α := Ideal (S ⧸ P))
      (comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
      {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal})
    J
Tactic: refine sInf_le_sInf fun J hJ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) | ⊥ ≤ J ∧ J.IsMaximal}
    J
⊢ Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    (Set.image (α := Ideal (S ⧸ P))
      (comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)))
      {J : Ideal (S ⧸ P) | ⊥ ≤ J ∧ J.IsMaximal})
    J
have neg : ∃ (x : Ideal (S ⧸ P)),
  x.IsMaximal ∧
    comap (F :=
        RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
        (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)) x =
      J
Tactic: simp only [true_and, Set.mem_image, bot_le, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsIntegral R S
inst_4 : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬Eq (α := Ideal R) (comap (F := R →+* S) (algebraMap R S) P) ⊤
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))
hJ :
  Membership.mem (γ := Set (Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P))))
    {J : Ideal (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) | ⊥ ≤ J ∧ J.IsMaximal}
    J
⊢ ∃ (x : Ideal (S ⧸ P)),
    x.IsMaximal ∧
      comap (F :=
          RingHom.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P))
          (algebraMap (HasQuotient.Quotient R (B := Ideal R) (comap (F := R →+* S) (algebraMap R S) P)) (S ⧸ P)) x =
        J
have this₁ : J.IsMaximal
Tactic: have : J.IsMaximal := by simpa using hJ
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ J.IsMaximal ↔ IsMaximal (under R J) ∧ y ∉ under R J
have mp : J.IsMaximal → IsMaximal (under R J) ∧ y ∉ under R J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
mp : J.IsMaximal → IsMaximal (under R J) ∧ y ∉ under R J
⊢ J.IsMaximal ↔ IsMaximal (under R J) ∧ y ∉ under R J
have mpr : IsMaximal (under R J) ∧ y ∉ under R J → J.IsMaximal
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
⊢ J.IsMaximal → IsMaximal (under R J) ∧ y ∉ under R J
have mp : ∀ (h : J.IsMaximal), IsMaximal (under R J)
Tactic: refine fun h => ⟨?_, fun hy =>
      h.ne_top (Ideal.eq_top_of_isUnit_mem _ hy (map_units _ ⟨y, Submonoid.mem_powers _⟩))⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ring (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
y : R
inst_2 : Algebra R S
inst_3 : Away y S
H : IsJacobsonRing R
J : Ideal S
h : J.IsMaximal
⊢ IsMaximal (under R J)
have hJ : J.IsPrime
Tactic: have hJ : J.IsPrime := IsMaximal.isPrime h