awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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})
simp_rw₄ : Eq.{u + 1} (α := Ideal R) (sInf {J : Ideal R | J.IsMaximal}) (sInf {m : Submodule R R | IsCoatom m})
⊢ Eq (α := Ideal R) (jacobson ⊥) (Ring.jacobson R)

Tactic:
simp_rw [jacobson, Ring.jacobson, Module.jacobson, bot_le, true_and, isMaximal_def]

Premises used: Module.jacobson, Ideal.jacobson, Ring.jacobson, bot_le, true_and, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I.jacobson = ⊤ ↔ I = ⊤

Tactic:
⟨fun H =>
    by_contradiction fun hi => let ⟨M, hm, him⟩ := exists_le_maximal I hi
      lt_top_iff_ne_top.1
        (lt_of_le_of_lt (show jacobson I ≤ M from sInf_le ⟨him, hm⟩) <|
          lt_top_iff_ne_top.2 hm.ne_top) H,
    fun H => eq_top_iff.2 <| le_sInf fun _ ⟨hij, _⟩ => H ▸ hij⟩

Premises used: Iff.mpr, lt_of_le_of_lt, False, _private.0.Ideal.jacobson_eq_top_iff.match_2, eq_top_iff, Eq.rec, LE.le, lt_top_iff_ne_top, sInf_le, And.intro, Iff.intro, by_contradiction, Iff.mp, _private.0.Ideal.jacobson_eq_top_iff.match_1, le_sInf, Ideal.exists_le_maximal, Ideal.IsMaximal.ne_top, Top.top
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I.jacobson = ⊥ → I = ⊥

Tactic:
fun h => eq_bot_iff.mpr (h ▸ le_jacobson)

Premises used: Iff.mpr, Eq.rec, eq_bot_iff, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
H : I.IsMaximal
⊢ I.jacobson = I

Tactic:
le_antisymm (sInf_le ⟨le_of_eq rfl, H⟩) le_jacobson

Premises used: le_antisymm, sInf_le, And.intro, le_of_eq, rfl, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
I : Ideal R
H : I.IsMaximal
⊢ I.jacobson.IsMaximal

Tactic:
⟨⟨fun htop => H.1.1 (jacobson_eq_top_iff.1 htop), fun _ hJ =>
    H.1.2 _ (lt_of_le_of_lt le_jacobson hJ)⟩⟩

Premises used: lt_of_le_of_lt, Ideal.jacobson_eq_top_iff, Ideal.IsMaximal.mk, And.right, Ideal.IsMaximal.out, And.left, And.intro, Iff.mp, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
rw : -p ∈ I
⊢ r * y * x + r - 1 ∈ I

Tactic:
rw [mul_assoc, ← mul_add_one, hr, ← hpq, ← neg_sub, add_sub_cancel_right]

Premises used: neg_sub, mul_assoc, add_sub_cancel_right, mul_add_one
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
⊢ -p ∈ I

Tactic:
I.neg_mem hpi

Premises used: Set.Mem, Submodule.neg_mem
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
⊢ -p ∈ I

Tactic:
exact I.neg_mem hpi

Premises used: Submodule.neg_mem
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
rw : z * i ∈ M
⊢ z * -y * x + z ∈ M

Tactic:
rw [mul_assoc, ← mul_add_one, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub,
            sub_add_cancel]

Premises used: Iff.mpr, neg_sub, mul_assoc, sub_eq_iff_eq_add, neg_mul, mul_add_one, Eq.symm, sub_add_cancel
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 * i ∈ M

Tactic:
M.mul_mem_left _ hi

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 * i ∈ M

Tactic:
exact M.mul_mem_left _ hi

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
obtain : ∀ (s : R) (hs : s * 1 * r + s - 1 ∈ I), ∃ (s : R), s * (r + 1) - 1 ∈ I
⊢ ∃ (s : R), s * (r + 1) - 1 ∈ I

Tactic:
obtain ⟨s, hs⟩ := mem_jacobson_iff.1 h 1

Premises used: Ideal.mem_jacobson_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
h₁ : s * (r + 1) - 1 ∈ I
⊢ ∃ (s : R), s * (r + 1) - 1 ∈ I

Tactic:
use s
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
h₁ : s * r + s - 1 ∈ I
⊢ s * (r + 1) - 1 ∈ I

Tactic:
rw [mul_add, mul_one]

Premises used: mul_add, mul_one
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 - 1 ∈ I

Tactic:
simpa using hs
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
⊢ ∃ (s : R), s * (r - 1 + 1) - 1 ∈ I

Tactic:
exists_mul_add_sub_mem_of_mem_jacobson _ h

Premises used: Ideal.exists_mul_add_sub_mem_of_mem_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
h₁ : ∀ (x : R), r = r - 1 + 1
⊢ ∃ (s : R), s * r - 1 ∈ I

Tactic:
convert! exists_mul_add_sub_mem_of_mem_jacobson _ h

Premises used: Ideal.exists_mul_add_sub_mem_of_mem_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
r : R
h : r - 1 ∈ I.jacobson
x : R
⊢ r = r - 1 + 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
mpr : (∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M) → I.jacobson = I
⊢ I.jacobson = I ↔ ∃ (M : Set (Ideal R)), (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M

Tactic:
use fun hI => ⟨{ J : Ideal R | I ≤ J ∧ J.IsMaximal }, ⟨fun _ hJ => Or.inl hJ.right, hI.symm⟩⟩
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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

Tactic:
le_antisymm (fun x hx => ?_) le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
mpr : ∀ (x : R) (hx : x ∈ I.jacobson), x ∈ I
⊢ I.jacobson = I

Tactic:
refine le_antisymm (fun x hx => ?_) le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
mpr : ∀ ⦃I : Ideal R⦄, I ∈ M → x ∈ I
⊢ x ∈ I

Tactic:
rw [hInf, mem_sInf]

Premises used: Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
mpr₁ : ∀ (is_top : I = ⊤), x ∈ I
⊢ x ∈ I

Tactic:
rcases hM I hI with is_max | is_top
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
is_max : I.IsMaximal
⊢ x ∈ I

Tactic:
(mem_sInf.1 hx) ⟨le_sInf_iff.1 (le_of_eq hInf) I hI, is_max⟩

Premises used: le_sInf_iff, Ideal.mem_sInf, And.intro, Iff.mp, le_of_eq
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
is_max : I.IsMaximal
⊢ x ∈ I

Tactic:
exact (mem_sInf.1 hx) ⟨le_sInf_iff.1 (le_of_eq hInf) I hI, is_max⟩

Premises used: le_sInf_iff, Ideal.mem_sInf, And.intro, Iff.mp, le_of_eq
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
is_top : I = ⊤
⊢ x ∈ I

Tactic:
is_top.symm ▸ Submodule.mem_top

Premises used: Eq.rec, Eq.symm, Submodule.mem_top
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
is_top : I = ⊤
⊢ x ∈ I

Tactic:
exact is_top.symm ▸ Submodule.mem_top
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ I.jacobson = I ↔ ∃ (M : Set (Ideal R)), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M

Tactic:
eq_jacobson_iff_sInf_maximal.trans
    ⟨fun h =>
      let ⟨M, hM⟩ := h
      ⟨M,
        ⟨fun J hJ K hK =>
          Or.recOn (hM.1 J hJ) (fun h => h.1.2 K hK) fun h => eq_top_iff.2 (le_of_lt (h ▸ hK)),
          hM.2⟩⟩,
      fun h =>
      let ⟨M, hM⟩ := h
      ⟨M,
        ⟨fun J hJ =>
          Or.recOn (Classical.em (J = ⊤)) (fun h => Or.inr h) fun h => Or.inl ⟨⟨h, hM.1 J hJ⟩⟩,
          hM.2⟩⟩⟩

Premises used: Ideal.eq_jacobson_iff_sInf_maximal, Or.recOn, Exists, And, And.right, And.left, And.intro, Iff.intro, Classical.em, Exists.intro, Iff.trans, _private.0.Ideal.eq_jacobson_iff_sInf_maximal'.match_1, Top.top, Eq, InfSet.sInf, _private.0.Ideal.eq_jacobson_iff_sInf_maximal'.match_2
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
mpr : (∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I
⊢ I.jacobson = I ↔ ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M

Tactic:
constructor
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
h : I.jacobson = I
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

Tactic:
rw [← h, Ideal.jacobson, mem_sInf] at hx

Premises used: Ideal.jacobson, Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
⊢ ∃ (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

Premises used: Not
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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

Tactic:
hx

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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

Tactic:
exact hx
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ (∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I

Tactic:
fun h => le_antisymm (fun x hx => ?_) le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
mpr : ∀ (h : ∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) (x : R) (hx : x ∈ I.jacobson), x ∈ I
⊢ (∀ x ∉ I, ∃ (M : Ideal R), (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M) → I.jacobson = I

Tactic:
refine fun h => le_antisymm (fun x hx => ?_) le_jacobson

Premises used: le_antisymm, Ideal.le_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
mpr : ∀ (hx : x ∉ I), x ∉ I.jacobson
⊢ x ∈ I

Tactic:
contrapose hx
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
mpr : ¬∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1
⊢ x ∉ I.jacobson

Tactic:
rw [Ideal.jacobson, mem_sInf]

Premises used: Ideal.jacobson, Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
mpr : ∃ (I_1 : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 ∧ x ∉ I_1
⊢ ¬∀ ⦃I_1 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_1 → x ∈ I_1

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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

Tactic:
h x hx

Premises used: Set.Mem, setOf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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

Tactic:
exact h x hx
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
⊢ ∀ (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
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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})

Tactic:
Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)

Premises used: Trans.trans, le_antisymm, Ideal.map_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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})
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}))
⊢ 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})

Tactic:
refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)

Premises used: Trans.trans, le_antisymm, Ideal.map_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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})

Tactic:
sInf_le_sInf fun J hJ =>
        ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, ?_⟩, map_comap_of_surjective f hf J⟩⟩

Premises used: Ideal.le_comap_of_map_le, Set.Mem, sInf_le_sInf, And.left, And.intro, Ideal.comap, Exists.intro, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 :
  ∀ (J : Ideal S) (hJ : Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsMaximal} J),
    IsMaximal (comap 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})

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⟩⟩
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
⊢ J.IsMaximal

Tactic:
haveI : J.IsMaximal := hJ.right
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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_1 : ∀ (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
this : J.IsMaximal
⊢ IsMaximal (comap f J)

Tactic:
comap_isMaximal_of_surjective f hf

Premises used: Ideal.comap_isMaximal_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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_1 : ∀ (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
this : J.IsMaximal
⊢ IsMaximal (comap f J)

Tactic:
exact comap_isMaximal_of_surjective f hf

Premises used: Ideal.comap_isMaximal_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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}))

Tactic:
sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => ?_

Premises used: Set.Mem, sInf_le_sInf_of_subset_insert_top, Exists.recOn
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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_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
⊢ 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 sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => ?_

Premises used: sInf_le_sInf_of_subset_insert_top
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 : 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}) j

Tactic:
rw [← hJ.2]

Premises used: And.right
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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)
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)
⊢ 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

Premises used: Ideal.map_eq_top_or_isMaximal_of_surjective, And.right, And.left