awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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:
htop.symm ▸ Set.mem_insert ⊤ _

Premises used: Eq.rec, Set.mem_insert, Top.top, Eq.symm
-- 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
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:
exact htop.symm ▸ Set.mem_insert ⊤ _
-- 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
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:
Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩

Premises used: Set.mem_insert_of_mem, And.left, And.intro, Ideal.map_mono, Top.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
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:
exact Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩
-- 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.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq.{v + 1} (α := Ideal S) (map f I.jacobson) (jacobson (map f I))

Tactic:
map_jacobson_of_surjective hf.right
    (le_trans (le_of_eq ((RingHom.injective_iff_ker_eq_bot f).1 hf.left)) bot_le)

Premises used: And.right, RingHom.injective_iff_ker_eq_bot, And.left, Iff.mp, le_of_eq, bot_le, Ideal.map_jacobson_of_surjective, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
K : Ideal S
⊢ Eq (α := Ideal R) (comap f K.jacobson) (sInf (Set.image (α := Ideal S) (comap f) {J : Ideal S | K ≤ J ∧ J.IsMaximal}))

Tactic:
Trans.trans (comap_sInf' f _) sInf_eq_iInf.symm

Premises used: Trans.trans, Ideal.comap_sInf', sInf_eq_iInf, Eq.symm
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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})

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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})
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}))
⊢ Eq (α := 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 ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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.{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)
⊢ 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:
rw [← top_inf_eq (sInf _), ← sInf_insert, comap_sInf', sInf_eq_iInf]

Premises used: Ideal.comap_sInf', top_inf_eq, sInf_eq_iInf, sInf_insert, InfSet.sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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)

Tactic:
iInf_le_iInf_of_subset fun J hJ => ?_

Premises used: Set.Mem, iInf_le_iInf_of_subset
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 :
  ∀ (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
⊢ 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:
refine iInf_le_iInf_of_subset fun J hJ => ?_

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

Premises used: Ideal.map_eq_top_or_isMaximal_of_surjective, And.right
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
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:
⟨⊤, Set.mem_insert ⊤ _, htop ▸ this⟩

Premises used: Set.Mem, setOf, Eq.rec, And.intro, Exists.intro, Set.mem_insert, Set.image, Top.top
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
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:
exact ⟨⊤, Set.mem_insert ⊤ _, htop ▸ this⟩
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
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:
⟨map f J, Set.mem_insert_of_mem _ ⟨le_map_of_comap_le_of_surjective f hf hJ.1, hmax⟩,
        this⟩

Premises used: Set.Mem, setOf, Set.mem_insert_of_mem, Ideal.map, Ideal.le_map_of_comap_le_of_surjective, And.left, And.intro, Exists.intro, Set.image
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
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:
exact ⟨map f J, Set.mem_insert_of_mem _ ⟨le_map_of_comap_le_of_surjective f hf hJ.1, hmax⟩,
        this⟩
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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_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)
⊢ 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:
simp_rw [comap_sInf, le_iInf_iff]

Premises used: le_iInf_iff, Ideal.comap_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
⊢ 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
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
this : J.IsMaximal
⊢ LE.le (α := Ideal R) (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal}) (comap f J)

Tactic:
sInf_le ⟨comap_mono hJ.left, comap_isMaximal_of_surjective _ hf⟩

Premises used: Set.Mem, Ideal.comap_isMaximal_of_surjective, Ideal.comap_mono, And.left, sInf_le, And.intro
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
this : J.IsMaximal
⊢ LE.le (α := Ideal R) (sInf {J : Ideal R | comap f K ≤ J ∧ J.IsMaximal}) (comap f J)

Tactic:
exact sInf_le ⟨comap_mono hJ.left, comap_isMaximal_of_surjective _ hf⟩
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ I.jacobson
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
⊢ x ∈ J.jacobson

Tactic:
rw [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 J : Ideal R
h : I ≤ J
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 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | J ≤ J_1 ∧ J_1.IsMaximal} I → x ∈ I

Tactic:
fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩

Premises used: Trans.trans, _private.0.Ideal.jacobson_eq_top_iff.match_2, Membership.mem, And.intro
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I J : Ideal R
h : I ≤ J
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 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J_1 : Ideal R | J ≤ J_1 ∧ J_1.IsMaximal} I → x ∈ I

Tactic:
exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : Ideal R
⊢ Ring.jacobson R ≤ I.jacobson

Tactic:
jacobson_bot.symm.trans_le (jacobson_mono bot_le)

Premises used: Ideal.jacobson_bot, Eq.trans_le, Ideal.jacobson_mono, Eq.symm, bot_le
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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
apply : ∀ ⦃I_2 : Ideal R⦄, Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsMaximal} I_2 → x * r ∈ I_2
⊢ x * r ∈ I.jacobson

Tactic:
apply mem_sInf.mpr

Premises used: Iff.mpr, Ideal.mem_sInf
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ∈ 𝔪
neg : ∀ (r𝔪 : r ∉ 𝔪), x * r ∈ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
by_cases r𝔪 : r ∈ 𝔪
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ∈ 𝔪
⊢ x * r ∈ 𝔪

Tactic:
apply 𝔪.smul_mem _ r𝔪

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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)) 𝔪
this : x ∈ 𝔪₀
⊢ x * r ∈ 𝔪

Tactic:
simpa [𝔪₀] using this
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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)) 𝔪
neg : x ∈ 𝔪₀
⊢ x * r ∈ 𝔪

Tactic:
suffices x ∈ 𝔪₀ by simpa [𝔪₀] using this
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀

Tactic:
have I𝔪₀ : I ≤ 𝔪₀ := fun i iI =>
      𝔪_mem.left (I.mul_mem_right _ iI)
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
h : 1 ∈ 𝔪₀
⊢ r ∈ 𝔪

Tactic:
simpa [𝔪₀] using h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
refine : ∀ (J : Ideal R) (b : R) (𝔪₀J : 𝔪₀ ≤ J) (b𝔪₀ : b ∉ 𝔪₀) (bJ : b ∈ J), 1 ∈ J
⊢ 𝔪₀.IsMaximal

Tactic:
refine isMaximal_iff.mpr ⟨
        fun h => r𝔪 (by simpa [𝔪₀] using h),
        fun J b 𝔪₀J b𝔪₀ bJ => ?_⟩

Premises used: Iff.mpr, Ideal.isMaximal_iff, And.intro
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
have : ∀ (s y : R) (y𝔪 : y ∈ 𝔪) (sbyr : s * (b * r) + y = r * 1), 1 ∈ J
⊢ 1 ∈ J

Tactic:
have ⟨s, y, y𝔪, sbyr⟩ :=
        mem_span_singleton_sup.mp <|
          mul_mem_left _ r <|
            (isMaximal_iff.mp 𝔪_mem.right).right K (b * r)
            le_sup_right b𝔪₀
            (mem_sup_left <| mem_span_singleton_self _)
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
⊢ y = r - s * (b * r)

Tactic:
rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr

Premises used: eq_sub_iff_add_eq, add_comm, mul_one
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ r - s * b * r ∈ 𝔪

Tactic:
rw [sbyr, ← mul_assoc] at y𝔪

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : y = r - s * (b * r)
y𝔪₁ : r - s * b * r ∈ 𝔪
⊢ y = r - s * (b * r)

Tactic:
rw [sbyr, ← mul_assoc] at y𝔪

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : r - s * b * r ∈ 𝔪
sbyr : y = r - s * (b * r)
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
simp [𝔪₀, sub_mul, y𝔪]

Premises used: sub_mul
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
⊢ 1 - s * b ∈ 𝔪₀

Tactic:
have : 1 - s * b ∈ 𝔪₀ := by
        rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr
        rw [sbyr, ← mul_assoc] at y𝔪
        simp [𝔪₀, sub_mul, y𝔪]
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this : 1 - s * b ∈ 𝔪₀
⊢ 1 - s * b + s * b ∈ J

Tactic:
apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)

Premises used: AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Jacobson.Ideal
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 ≤ 𝔪₀
J : Ideal R
b : R
𝔪₀J : 𝔪₀ ≤ J
b𝔪₀ : b ∉ 𝔪₀
bJ : b ∈ J
K : Ideal R := span {b * r} ⊔ 𝔪
s y : R
y𝔪 : y ∈ 𝔪
sbyr : s * (b * r) + y = r * 1
this : 1 - s * b ∈ 𝔪₀
⊢ 1 - s * b + s * b ∈ J

Tactic:
have : 1 - s * b + s * b ∈ J := by
        apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)