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_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 : 1 - s * b ∈ 𝔪₀
this : 1 - s * b + s * b ∈ J
⊢ 1 ∈ J

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)) 𝔪
I𝔪₀ : I ≤ 𝔪₀
⊢ 𝔪₀.IsMaximal

Tactic:
have 𝔪₀_maximal : IsMaximal 𝔪₀ := by
      refine isMaximal_iff.mpr ⟨
        fun h => r𝔪 (by simpa [𝔪₀] using h),
        fun J b 𝔪₀J b𝔪₀ bJ => ?_⟩
      let K : Ideal R := Ideal.span {b*r} ⊔ 𝔪
      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 _)
      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𝔪]
      have : 1 - s * b + s * b ∈ J := by
        apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)
      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𝔪₀ : I ≤ 𝔪₀
𝔪₀_maximal : 𝔪₀.IsMaximal
⊢ x ∈ 𝔪₀

Tactic:
mem_sInf.mp xJ ⟨I𝔪₀, 𝔪₀_maximal⟩

Premises used: Ideal.mem_sInf, And.intro, Iff.mp
-- 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 ≤ 𝔪₀
𝔪₀_maximal : 𝔪₀.IsMaximal
⊢ x ∈ 𝔪₀

Tactic:
exact mem_sInf.mp xJ ⟨I𝔪₀, 𝔪₀_maximal⟩

Premises used: Ideal.mem_sInf, And.intro, Iff.mp
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.radical ≤ I.jacobson

Tactic:
le_sInf fun _ hJ => (radical_eq_sInf I).symm ▸ sInf_le ⟨hJ.left, IsMaximal.isPrime hJ.right⟩

Premises used: Set.Mem, Eq.rec, Ideal.IsMaximal.isPrime, Ideal.radical_eq_sInf, And.right, And.left, sInf_le, And.intro, le_sInf, Eq.symm
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
h : I.jacobson = I
⊢ I.IsRadical

Tactic:
radical_le_jacobson.trans h.le

Premises used: Eq.le, Ideal.IsRadical, Ideal.radical_le_jacobson, LE.le.trans
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ IsRadical.{u} (R := R) I.jacobson

Tactic:
isRadical_of_eq_jacobson jacobson_idem

Premises used: Ideal.isRadical_of_eq_jacobson, Ideal.jacobson_idem
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
r : R
h : Membership.mem (γ := Ideal R) (jacobson ⊥) (r - 1)
obtain : ∀ (s : R) (hs : Membership.mem (γ := Ideal R) ⊥ (s * r - 1)), IsUnit r
⊢ IsUnit r

Tactic:
obtain ⟨s, hs⟩ := exists_mul_sub_mem_of_sub_one_mem_jacobson r h

Premises used: Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
r : R
h : Membership.mem (γ := Ideal R) (jacobson ⊥) (r - 1)
s : R
hs : Membership.mem (γ := Ideal R) ⊥ (s * r - 1)
⊢ r * s = 1

Tactic:
rw [mem_bot, sub_eq_zero, mul_comm] at hs

Premises used: Ideal.mem_bot, sub_eq_zero, mul_comm
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
r : R
h : Membership.mem (γ := Ideal R) (jacobson ⊥) (r - 1)
s : R
hs : r * s = 1
⊢ IsUnit r

Tactic:
.of_mul_eq_one _ hs

Premises used: IsUnit.of_mul_eq_one
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
r : R
h : Membership.mem (γ := Ideal R) (jacobson ⊥) (r - 1)
s : R
hs : r * s = 1
⊢ IsUnit r

Tactic:
exact .of_mul_eq_one _ hs
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
x : R
hx : Membership.mem (γ := Ideal R) (jacobson ⊥) x
y z : R
hz : Membership.mem (γ := Ideal R) ⊥ (z * y * x + z - 1)
rwa : x * y * z + 1 * z = 1
rwa₁ : x * y * z + z = 1
rwa₂ : x * y * z + z - 1 = 0
rwa₃ : x * z * y + z - 1 = 0
rwa₄ : z * x * y + z - 1 = 0
rwa₅ rwa₆ rwa₇ rwa₈ : z * y * x + z - 1 = 0
⊢ (x * y + 1) * z = 1

Tactic:
rwa [add_mul, one_mul, ← sub_eq_zero, mul_right_comm, mul_comm _ z, mul_right_comm]

Premises used: add_mul, sub_eq_zero, mul_right_comm, mul_comm, one_mul
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
x : R
h : ∀ (y : R), IsUnit (x * y + 1)
y b : R
hb : (x * y + 1) * b = 1
⊢ b * y * x + b - (x * y + 1) * b = 0

Tactic:
ring
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)

Tactic:
have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
mp : I.jacobson = I → Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
mpr : Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥ → I.jacobson = I
⊢ I.jacobson = I ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥

Tactic:
constructor
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.jacobson = I
⊢ Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson) (map (F := R →+* R ⧸ I) (Quotient.mk I) I)

Tactic:
replace h := congr_arg (Ideal.map (Ideal.Quotient.mk I)) h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h :
  Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson) (map (F := R →+* R ⧸ I) (Quotient.mk I) I)
⊢ Eq (α := Ideal (R ⧸ I)) (jacobson (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) I)

Tactic:
rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h

Premises used: Ideal.mk_ker, le_of_eq, Ideal.map_jacobson_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h :
  Eq (α := Ideal (R ⧸ I)) (jacobson (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) I)
⊢ Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (jacobson ⊥) ⊥
⊢ Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥)) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)

Tactic:
replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h :
  Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥)) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)
⊢ Eq (α := Ideal R) (jacobson (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))

Tactic:
rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h

Premises used: Ideal.comap_jacobson_of_surjective, Ideal.Quotient.mk, RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h :
  Eq (α := Ideal R) (jacobson (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))
⊢ I.jacobson = I

Tactic:
simpa using h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
mp : I.radical = I.jacobson → Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
mpr : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥) → I.radical = I.jacobson
⊢ I.radical = I.jacobson ↔ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.radical = I.jacobson
⊢ Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.radical)
    (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson)

Tactic:
have := congr_arg (map (Ideal.Quotient.mk I)) h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.radical = I.jacobson
this :
  Eq (α := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) I.radical)
    (map (F := R →+* R ⧸ I) (Quotient.mk I) I.jacobson)
⊢ Eq (α := Ideal (R ⧸ I)) (radical (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
    (jacobson (map (F := R →+* R ⧸ I) (Quotient.mk I) I))

Tactic:
rw [map_radical_of_surjective hf (le_of_eq mk_ker),
      map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this

Premises used: Ideal.map_radical_of_surjective, Ideal.mk_ker, le_of_eq, Ideal.map_jacobson_of_surjective
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : I.radical = I.jacobson
this :
  Eq (α := Ideal (R ⧸ I)) (radical (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
    (jacobson (map (F := R →+* R ⧸ I) (Quotient.mk I) I))
⊢ Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
⊢ Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (radical ⊥))
    (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥))

Tactic:
have := congr_arg (comap (Ideal.Quotient.mk I)) h
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
this :
  Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (radical ⊥))
    (comap (F := R →+* R ⧸ I) (Quotient.mk I) (jacobson ⊥))
⊢ Eq (α := Ideal R) (radical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (jacobson (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))

Tactic:
rw [comap_radical, comap_jacobson_of_surjective hf,
      ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this

Premises used: Ideal.comap_jacobson_of_surjective, Ideal.Quotient.mk, RingHom.ker_eq_comap_bot, Ideal.comap_radical
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hf : Function.Surjective (α := R) (β := R ⧸ I) (⇑(Quotient.mk I) : (a : R) → R ⧸ I)
h : Eq.{u + 1} (α := Ideal (R ⧸ I)) (radical ⊥) (jacobson ⊥)
this :
  Eq (α := Ideal R) (radical (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
    (jacobson (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I)))
⊢ I.radical = I.jacobson

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.radical.jacobson = I.jacobson

Tactic:
le_antisymm
    (le_trans (le_of_eq (congr_arg jacobson (radical_eq_sInf I)))
      (sInf_le_sInf fun _ hJ => ⟨sInf_le ⟨hJ.1, hJ.2.isPrime⟩, hJ.2⟩))
    (jacobson_mono le_radical)

Premises used: Ideal.le_radical, sInf_le_sInf, Ideal.jacobson, Ideal.IsMaximal.isPrime, congr_arg, Ideal.radical_eq_sInf, le_antisymm, Ideal.jacobson_mono, And.right, And.left, sInf_le, And.intro, le_of_eq, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
⊢ I.IsLocal ↔ I.jacobson.IsMaximal

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Iff.intro, Ideal.IsLocal.out, Ideal.IsLocal.mk
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I.IsLocal

Tactic:
⟨have : radical I = jacobson I :=
      le_antisymm (le_sInf fun _ ⟨him, hm⟩ => hm.isPrime.radical_le_iff.2 him)
        (sInf_le ⟨le_radical, hi⟩)
    show IsMaximal (jacobson I) from this ▸ hi⟩

Premises used: Iff.mpr, _private.0.Ideal.isLocal_of_isMaximal_radical.match_1, Ideal.le_radical, Eq.rec, LE.le, Ideal.IsMaximal.isPrime, le_antisymm, sInf_le, And.intro, le_sInf, Ideal.IsPrime.radical_le_iff, Ideal.radical, Ideal.IsLocal.mk
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I J : Ideal R
hi : I.IsLocal
hij : I ≤ J
hj : J ≠ ⊤
⊢ J ≤ I.jacobson

Tactic:
let ⟨_, hm, hjm⟩ := exists_le_maximal J hj
  le_trans hjm <| le_of_eq <| Eq.symm <| hi.1.eq_of_le hm.1.1 <| sInf_le ⟨le_trans hij hjm, hm⟩

Premises used: Ideal.jacobson, LE.le, Ideal.IsMaximal.out, And.left, Ideal.IsMaximal.eq_of_le, sInf_le, And.intro, Ideal.exists_le_maximal, le_of_eq, Eq.symm, _private.0.Ideal.IsLocal.le_jacobson.match_1, Ideal.IsLocal.out, le_trans
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpq : p + q = 1
r : R
hr : q = x * r
rw : -p ∈ I
⊢ r * x - 1 ∈ I

Tactic:
rw [← hpq, mul_comm, ← hr, ← neg_sub, add_sub_cancel_right]

Premises used: neg_sub, mul_comm, add_sub_cancel_right
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -p ∈ I

Tactic:
I.neg_mem hpi

Premises used: Set.Mem, Submodule.neg_mem
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : Membership.mem (γ := Submodule R R) (span {x}) q
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -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 : TwoSidedIdeal R
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.jacobson : Ideal R) x ↔
      Membership.mem (γ := Ideal R) (Ideal.jacobson ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x
⊢ Eq (α := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.jacobson : Ideal R)
    (Ideal.jacobson ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) : Ideal R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
I : TwoSidedIdeal R
x : R
⊢ Membership.mem (γ := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.jacobson : Ideal R) x ↔
    Membership.mem (γ := Ideal R) (Ideal.jacobson ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x

Tactic:
simp [jacobson]

Premises used: TwoSidedIdeal.jacobson
-- Module: Mathlib.RingTheory.Jacobson.Ideal
Goal:
R : Type u
inst : Ring R
x : R
I : TwoSidedIdeal R
⊢ x ∈ I.jacobson ↔ ∀ (y : R), ∃ (z : R), z * y * x + z - 1 ∈ I

Tactic:
simp [jacobson, Ideal.mem_jacobson_iff]

Premises used: TwoSidedIdeal.jacobson, Ideal.mem_jacobson_iff
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
mp :
  Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂ →
    N₁ = N₂
mpr :
  N₁ = N₂ →
    Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂ ↔
    N₁ = N₂

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
⊢ N₂ ≤ HSMul.hSMul (α := Ideal R) 𝔪 N₂ ⊔ N₁

Tactic:
simpa using Submodule.comap_mono (f := Submodule.mkQ (𝔪 • N₂)) hN.ge
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
⊢ N₂ ≤ HSMul.hSMul (α := Ideal R) 𝔪 N₂ ⊔ N₁

Tactic:
have : N₂ ≤ 𝔪 • N₂ ⊔ N₁ := by
      simpa using Submodule.comap_mono (f := Submodule.mkQ (𝔪 • N₂)) hN.ge
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ HSMul.hSMul (α := Ideal R) 𝔪 N₂ ⊔ N₁
⊢ N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂

Tactic:
rw [sup_comm] at this

Premises used: sup_comm
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂
h₁ : Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤
⊢ LE.le (α := Ideal R) 𝔪 (Ideal.jacobson ⊥)

Tactic:
rw [jacobson_eq_maximalIdeal]

Premises used: IsLocalRing.jacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂
⊢ Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤

Tactic:
bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂
⊢ Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤

Tactic:
exact bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ HSMul.hSMul (α := Ideal R) 𝔪 N₂
⊢ N₁ = N₂

Tactic:
exact h.antisymm (Submodule.le_of_le_smul_of_le_jacobson_bot h'
      (by rw [jacobson_eq_maximalIdeal]; exact bot_ne_top) this)

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, LE.le.antisymm
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N₁ : Submodule R M
h : N₁ ≤ N₁
h' : N₁.FG
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₁).mkQ N₁ = Submodule.map (HSMul.hSMul (α := Ideal R) 𝔪 N₁).mkQ N₁

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
rw :
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
      Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ ⊤
rw₁ :
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N =
      (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ.range
rw₂ rw₃ :
  Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔
    Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤
⊢ Submodule.map (HSMul.hSMul (α := Ideal R) (β := Submodule R M) 𝔪 ⊤).mkQ N = ⊤ ↔ N = ⊤

Tactic:
rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]

Premises used: Module.Finite.fg_top, IsLocalRing.map_mkQ_eq, Submodule.map_top, Submodule.range_mkQ, le_top
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
inst_4 : Module.Finite R M
mp :
  Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤ →
    N = ⊤
mpr :
  N = ⊤ →
    Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤
⊢ Eq (α := Submodule R (k ⊗[R] M))
      (Submodule.map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R k M : (a : k) → M →ₗ[R] k ⊗[R] M) 1) N) ⊤ ↔
    N = ⊤

Tactic:
constructor