awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
simp_rw : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (Ring.jacobson R)
simp_rw₁ : Eq (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} : Ideal R) (Module.jacobson R R : Submodule R R)
simp_rw₂ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
simp_rw₃ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | True ∧ J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
⊢ Eq (α := Ideal R) (jacobson ⊥) (Ring.jacobson R)
have simp_rw₄ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
Tactic: simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : Membership.mem (γ := Submodule R R) (span {y * x + 1}) q
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I
have rw : -p ∈ I
Tactic: rw [mul_assoc, ← mul_add_one, hr, ← hpq, ← neg_sub, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I
M : Ideal R
h : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} M
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * -y * x + z ∈ M
have rw : z * i ∈ M
Tactic: rw [mul_assoc, ← mul_add_one, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub,
            sub_add_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
⊢ ∃ (s : R), s * (r + 1) - 1 ∈ I
have obtain : ∀ (s : R) (hs : s * 1 * r + s - 1 ∈ I), ∃ (s : R), s * (r + 1) - 1 ∈ I
Tactic: obtain ⟨s, hs⟩ := mem_jacobson_iff.1 h 1
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ ∃ (s : R), s * (r + 1) - 1 ∈ I
have h₁ : s * (r + 1) - 1 ∈ I
Tactic: use s
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
s : R
hs : s * 1 * r + s - 1 ∈ I
⊢ s * (r + 1) - 1 ∈ I
have h₁ : s * r + s - 1 ∈ I
Tactic: rw [mul_add, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
⊢ ∃ (s : R), s * r - 1 ∈ I
have h₁ : ∀ (x : R), r = r - 1 + 1
Tactic: convert! exists_mul_add_sub_mem_of_mem_jacobson _ h
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
have mpr : (∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M) → I.jacobson = I
Tactic: use fun hI => ⟨{ J : Ideal R | I ≤ J ∧ J.IsMaximal }, ⟨fun _ hJ => Or.inl hJ.right, hI.symm⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
⊢ I.jacobson = I
have mpr : ∀ (x : R) (hx : x ∈ I.jacobson), x ∈ I
Tactic: refine le_antisymm (fun x hx => ?_) le_jacobson
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I
have mpr : ∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I
Tactic: rw [hInf, mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I_1 : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I_1 = sInf M
x : R
hx : x ∈ I_1.jacobson
I : Ideal R
hI : I ∈ M
⊢ x ∈ I
have mpr : ∀ (is_max : I.IsMaximal), x ∈ I
Tactic: rcases hM I hI with is_max | is_top
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I_1 : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I_1 = sInf M
x : R
hx : x ∈ I_1.jacobson
I : Ideal R
hI : I ∈ M
mpr : ∀ (is_max : I.IsMaximal), x ∈ I
⊢ x ∈ I
have mpr₁ : ∀ (is_top : I = ⊤), x ∈ I
Tactic: rcases hM I hI with is_max | is_top
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
have mp : I.jacobson = I → ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
mp : I.jacobson = I → ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
have mpr : (∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : x ∉ I
⊢ ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
have hx₁ : ¬∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
Tactic: rw [← h, Ideal.jacobson, mem_sInf] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
inst : Ring R
I : Ideal R
h : I.jacobson = I
x : R
hx : ¬∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
⊢ ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
have hx₁ : ∃ (I_1 : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 ∧ x ∉ I_1
Tactic: push Not at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I
have mpr : ∀ (h : ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) (x : R) (hx : x ∈ I.jacobson), x ∈ I
Tactic: refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I
have mpr : ∀ (hx : x ∉ I), x ∉ I.jacobson
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ x ∉ I.jacobson
have mpr : ¬∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
Tactic: rw [Ideal.jacobson, mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
h : ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
x : R
hx : x ∉ I
⊢ ¬∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
have mpr : ∃ (I_1 : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 ∧ x ∉ I_1
Tactic: push Not
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
⊢ Eq.{v + 1} (α := Ideal S) (map (R := R) f (sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
have this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
Tactic: have : ∀ J ∈ { J : Ideal R | I ≤ J ∧ J.IsMaximal }, RingHom.ker f ≤ J :=
    fun J hJ => le_trans h hJ.left
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
⊢ Eq.{v + 1} (α := Ideal S) (map (R := R) f (sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
have refine_1 : LE.le.{v} (α := Ideal S) (sInf (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
  (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
Tactic: refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
refine_1 :
  LE.le.{v} (α := Ideal S) (sInf (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
⊢ Eq.{v + 1} (α := Ideal S) (map (R := R) f (sInf {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
have refine_2 : LE.le.{v} (α := Ideal S) (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
  (sInf (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
Tactic: refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
⊢ LE.le.{v} (α := Ideal S) (sInf (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
have refine_1 : ∀ (J : Ideal S) (hJ : Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsMaximal} J),
  IsMaximal (comap f J)
Tactic: refine
      sInf_le_sInf fun J hJ =>
        ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, ?_⟩, map_comap_of_surjective f hf J⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
J : Ideal S
hJ : Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsMaximal} J
⊢ IsMaximal (comap f J)
have this₁ : J.IsMaximal
Tactic: haveI : J.IsMaximal := hJ.right
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
⊢ LE.le.{v} (α := Ideal S) (sInf {J : Ideal S | map f I ≤ J ∧ J.IsMaximal})
    (sInf (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}))
have refine_2 : ∀ (j : Ideal S)
  (hj :
    Membership.mem (γ := Set (Ideal S)) (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}) j)
  (J : Ideal R) (hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J ∧ map f J = j),
  Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) j
Tactic: refine sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}) j
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J ∧ map f J = j
⊢ Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) j
have refine_2 : Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) (map f J)
Tactic: rw [← hJ.2]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}) j
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J ∧ map f J = j
⊢ Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) (map f J)
have refine_2 : ∀ (htop : Eq.{v + 1} (α := Ideal S) (map f J) ⊤),
  Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) (map f J)
Tactic: rcases map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop | hmax
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J → RingHom.ker f ≤ J
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (Set.image.{u, v} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsMaximal}) j
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} J ∧ map f J = j
refine_2 :
  ∀ (htop : Eq.{v + 1} (α := Ideal S) (map f J) ⊤),
    Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) (map f J)
⊢ Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) (map f J)
have refine_2₁ : ∀ (hmax : IsMaximal.{v} (α := S) (map f J)),
  Membership.mem (γ := Set (Ideal S)) (insert ⊤ {J : Ideal S | map f I ≤ J ∧ J.IsMaximal}) (map f J)
Tactic: rcases map_eq_top_or_isMaximal_of_surjective f hf hJ.left.right with htop | hmax
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
⊢ Eq (α := Ideal R) (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
have refine_1 : LE.le (α := Ideal R) (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
  (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
refine_1 :
  LE.le (α := Ideal R) (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
⊢ Eq (α := Ideal R) (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
have refine_2 : LE.le (α := Ideal R) (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
  (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
⊢ LE.le (α := Ideal R) (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
    (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
have refine_1 : LE.le.{u} (α := Ideal R)
  (⨅ (I : Ideal R),
    ⨅ (_ :
      Membership.mem (γ := Set (Ideal R))
        (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) I),
      I)
  (⨅ (a : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal} a), a)
Tactic: rw [← top_inf_eq (sInf _), ← sInf_insert, comap_sInf', sInf_eq_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
⊢ LE.le.{u} (α := Ideal R)
    (⨅ (I : Ideal R),
      ⨅ (_ :
        Membership.mem (γ := Set (Ideal R))
          (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) I),
        I)
    (⨅ (a : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal} a), a)
have refine_1 : ∀ (J : Ideal R) (hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal} J),
  Membership.mem (γ := Set (Ideal R))
    (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
Tactic: refine iInf_le_iInf_of_subset fun J hJ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal} J
⊢ Membership.mem (γ := Set (Ideal R))
    (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
have this : comap f (map f J) = J
Tactic: have : comap f (map f J) = J :=
      Trans.trans (comap_map_of_surjective f hf J)
        (le_antisymm (sup_le_iff.2 ⟨le_of_eq rfl, le_trans (comap_mono bot_le) hJ.left⟩)
          le_sup_left)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal} J
this : comap f (map f J) = J
⊢ Membership.mem (γ := Set (Ideal R))
    (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
have refine_1 : ∀ (htop : Eq.{v + 1} (α := Ideal S) (map f J) ⊤),
  Membership.mem (γ := Set (Ideal R))
    (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
Tactic: rcases map_eq_top_or_isMaximal_of_surjective _ hf hJ.right with htop | hmax
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal} J
this : comap f (map f J) = J
refine_1 :
  ∀ (htop : Eq.{v + 1} (α := Ideal S) (map f J) ⊤),
    Membership.mem (γ := Set (Ideal R))
      (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
⊢ Membership.mem (γ := Set (Ideal R))
    (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
have refine_1₁ : ∀ (hmax : IsMaximal.{v} (α := S) (map f J)),
  Membership.mem (γ := Set (Ideal R))
    (Set.image (α := Ideal S) (comap f) (insert ⊤ {J : Ideal S | K ≤ J ∧ J.IsMaximal})) J
Tactic: rcases map_eq_top_or_isMaximal_of_surjective _ hf hJ.right with htop | hmax
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
⊢ LE.le (α := Ideal R) (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal})
    (comap f (sInf {J : Ideal S | K ≤ J ∧ J.IsMaximal}))
have refine_2 : ∀ (i : Ideal S) (i_1 : Membership.mem (γ := Set (Ideal S)) {J : Ideal S | K ≤ J ∧ J.IsMaximal} i),
  LE.le (α := Ideal R) (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal}) (comap f i)
Tactic: simp_rw [comap_sInf, le_iInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K J : Ideal S
hJ : Membership.mem (γ := Set (Ideal S)) {J : Ideal S | K ≤ J ∧ J.IsMaximal} J
⊢ LE.le (α := Ideal R) (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal}) (comap f J)
have this : J.IsMaximal
Tactic: haveI : J.IsMaximal := hJ.right
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ I.jacobson
⊢ x ∈ J.jacobson
have rw : ∀ (hx : ∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1)
  ⦃I : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | J ≤ J_1 ∧ J_1.IsMaximal} I → x ∈ I
Tactic: rw [jacobson, mem_sInf] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
⊢ x * r ∈ I.jacobson
have apply : ∀ ⦃I_2 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_2 → x * r ∈ I_2
Tactic: apply mem_sInf.mpr
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
⊢ x * r ∈ 𝔪
have pos : ∀ (r𝔪 : r ∈ 𝔪), x * r ∈ 𝔪
Tactic: by_cases r𝔪 : r ∈ 𝔪
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
pos : ∀ (r𝔪 : r ∈ 𝔪), x * r ∈ 𝔪
⊢ x * r ∈ 𝔪
have neg : ∀ (r𝔪 : r ∉ 𝔪), x * r ∈ 𝔪
Tactic: by_cases r𝔪 : r ∈ 𝔪
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x * r ∈ 𝔪
have neg : x ∈ 𝔪₀
Tactic: suffices x ∈ 𝔪₀ by simpa [𝔪₀] using this
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
⊢ x ∈ 𝔪₀
have I𝔪₀ : I ≤ 𝔪₀
Tactic: have I𝔪₀ : I ≤ 𝔪₀ := fun i iI =>
      𝔪_mem.left (I.mul_mem_right _ iI)
-- Lean 4 proof step from Mathlib.RingTheory.Jacobson.Ideal (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I_1 I : Ideal R
inst_2 : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} 𝔪
r𝔪 : r ∉ 𝔪
𝔪₀ : Ideal R := Submodule.comap (DistribSMul.toLinearMap R R (MulOpposite.op r)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
⊢ 𝔪₀.IsMaximal
have refine : ∀ (J : Ideal R) (b : R) (𝔪₀J : 𝔪₀ ≤ J) (b𝔪₀ : b ∉ 𝔪₀) (bJ : b ∈ J), 1 ∈ J
Tactic: refine isMaximal_iff.mpr ⟨
        fun h => r𝔪 (by simpa [𝔪₀] using h),
        fun J b 𝔪₀J b𝔪₀ bJ => ?_⟩