awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
q : Submodule R M
hqp : q.IsPrimary
p : (↑N.associatedPrimes : Type u_3)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
y : R
hy1 : y ∈ (↑(q.colon Set.univ) : Set R)
r : Ideal R
hrI : r ∈ N.associatedPrimes
hrs : Subtype.mk (p := fun (a : Ideal R) ↦ a ∈ N.associatedPrimes) r hrI ∈ s₀
hy2 : y ∈ r
⊢ Membership.mem (γ := Set R) (⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)) y

Tactic:
exact Set.mem_biUnion hrs hy2

Premises used: Set.mem_biUnion
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
q : Submodule R M
hqp : q.IsPrimary
p : (↑N.associatedPrimes : Type u_3)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
y : R
hy1 : y ∈ (↑(q.colon Set.univ) : Set R)
hy2 : y ∉ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
⊢ y ∈ S

Tactic:
replace hy2 : y ∈ S := by
      simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S]
      intro r hrI hrs
      contrapose hy2
      exact Set.mem_biUnion hrs hy2
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
q : Submodule R M
hqp : q.IsPrimary
p : (↑N.associatedPrimes : Type u_3)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
y : R
hy1 : y ∈ (↑(q.colon Set.univ) : Set R)
hy2 : y ∈ S
neg : LinearMap.range (mkLinearMap S M) ≤ localized₀ S (mkLinearMap S M) q
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤

Tactic:
rw [eq_top_iff, ← map_le_iff_le_comap, map_top]

Premises used: eq_top_iff, Submodule.map_top, Submodule.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
q : Submodule R M
hqp : q.IsPrimary
p : (↑N.associatedPrimes : Type u_3)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
y : R
hy1 : y ∈ (↑(q.colon Set.univ) : Set R)
hy2 : y ∈ S
x : M
neg :
  ∃ m ∈ q,
    ∃ (s : ↥S),
      Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
        ((mkLinearMap S M : (a : M) → LocalizedModule S M) (s • x) : LocalizedModule S M)
⊢ Membership.mem (α := LocalizedModule S M) (localized₀ S (mkLinearMap S M) q)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M)

Tactic:
simp_rw [mem_localized₀, IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower]

Premises used: Submodule.mem_localized₀, LinearMap.map_smul_of_tower, IsLocalizedModule.mk'_eq_iff
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
q : Submodule R M
hqp : q.IsPrimary
p : (↑N.associatedPrimes : Type u_3)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
y : R
hy1 : y ∈ (↑(q.colon Set.univ) : Set R)
hy2 : y ∈ S
x : M
⊢ ∃ m ∈ q,
    ∃ (s : ↥S),
      Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
        ((mkLinearMap S M : (a : M) → LocalizedModule S M) (s • x) : LocalizedModule S M)

Tactic:
⟨y • x, hy1 (Set.smul_mem_smul_set (Set.mem_univ x)), ⟨y, hy2⟩, rfl⟩

Premises used: Subtype.mk, And.intro, Exists.intro, Set.mem_univ, HSMul.hSMul, rfl, Set.smul_mem_smul_set
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
q : Submodule R M
hqp : q.IsPrimary
p : (↑N.associatedPrimes : Type u_3)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
y : R
hy1 : y ∈ (↑(q.colon Set.univ) : Set R)
hy2 : y ∈ S
x : M
⊢ ∃ m ∈ q,
    ∃ (s : ↥S),
      Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
        ((mkLinearMap S M : (a : M) → LocalizedModule S M) (s • x) : LocalizedModule S M)

Tactic:
exact ⟨y • x, hy1 (Set.smul_mem_smul_set (Set.mem_univ x)), ⟨y, hy2⟩, rfl⟩
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
set :
  let S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl;
  comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) N) = ⨅ q ∈ s, q
⊢ comap (M₂ := LocalizedModule.{u_3, u_4} (R := R) (⨅ q ∈ s₀, (↑q : Ideal R).primeCompl) M)
      (mkLinearMap (⨅ q ∈ s₀, (↑q : Ideal R).primeCompl) M)
      (localized₀ (⨅ q ∈ s₀, (↑q : Ideal R).primeCompl) (mkLinearMap (⨅ q ∈ s₀, (↑q : Ideal R).primeCompl) M) N) =
    ⨅ q ∈ s, q

Tactic:
set S := ⨅ q ∈ s₀, q.1.primeCompl
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
rw :
  Eq (α := Submodule R M)
    (t.inf fun (i : Submodule R M) ↦
      comap (mkLinearMap S M)
        (((⇑(localized₀FrameHom S (mkLinearMap S M)) : (a : Submodule R M) → Submodule R (LocalizedModule S M)) ∘ id)
          i))
    (⨅ q ∈ s, q)
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) N) = ⨅ q ∈ s, q

Tactic:
rw [← ht.inf_eq, ← localized₀FrameHom_apply, map_finset_inf, Submodule.comap_finsetInf]

Premises used: Submodule.IsMinimalPrimaryDecomposition.inf_eq, Submodule.comap_finsetInf, Submodule.IsLocalizedModule.localized₀FrameHom_apply, map_finset_inf
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
simp_rw :
  Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
⊢ Eq (α := Submodule R M)
    (t.inf fun (i : Submodule R M) ↦
      comap (mkLinearMap S M)
        (((⇑(localized₀FrameHom S (mkLinearMap S M)) : (a : Submodule R M) → Submodule R (LocalizedModule S M)) ∘ id)
          i))
    (⨅ q ∈ s, q)

Tactic:
simp_rw [Function.comp_def, id_eq, localized₀FrameHom_apply]

Premises used: Submodule.IsLocalizedModule.localized₀FrameHom_apply, Function.comp_def, id_eq
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
this : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
rw : Eq (α := Submodule R M) (t.inf fun (a : Submodule R M) ↦ if a ∈ s then a else ⊤) (⨅ q ∈ s, q)
rw₁ :
  Eq (α := Submodule R M)
    (((Finset.filter (Membership.mem s) t).inf fun (a : Submodule R M) ↦ a) ⊓
      {i ∈ t | i ∉ s}.inf fun (a : Submodule R M) ↦ ⊤)
    (⨅ q ∈ s, q)
rw₂ : Eq (α := Submodule R M) (((Finset.filter (Membership.mem s) t).inf fun (a : Submodule R M) ↦ a) ⊓ ⊤) (⨅ q ∈ s, q)
rw₃ : Eq (α := Submodule R M) ((Finset.filter (Membership.mem s) t).inf fun (a : Submodule R M) ↦ a) (⨅ q ∈ s, q)
rw₄ : Eq (α := Submodule R M) ((t ∩ s).inf fun (a : Submodule R M) ↦ a) (⨅ q ∈ s, q)
rw₅ : Eq (α := Submodule R M) (s.inf fun (a : Submodule R M) ↦ a) (⨅ q ∈ s, q)
rw₆ rw₇ : Eq.{u_4 + 1} (α := Submodule R M) (⨅ a ∈ s, a) (⨅ q ∈ s, q)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)

Tactic:
rw [Finset.inf_congr rfl this, Finset.inf_ite, Finset.inf_top, inf_top_eq,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.mpr hs, Finset.inf_eq_iInf]

Premises used: Iff.mpr, Finset.inf_ite, inf_top_eq, Finset.inf_congr, Finset.inter_eq_right, Finset.inf_eq_iInf, Finset.inf_top, Finset.filter_mem_eq_inter, rfl
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
suffices : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)

Tactic:
suffices ∀ q ∈ t, (localized₀ S f q).comap f = if q ∈ s then q else ⊤ by
    rw [Finset.inf_congr rfl this, Finset.inf_ite, Finset.inf_top, inf_top_eq,
      Finset.filter_mem_eq_inter, Finset.inter_eq_right.mpr hs, Finset.inf_eq_iInf]
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
⊢ ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤

Tactic:
fun q hqt ↦ (IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite s₀ hs₀ q
    (ht.primary hqt) ⟨(q.colon Set.univ).radical, ht.mem_associatedPrimes hqt⟩ rfl).trans
    (ite_cond_congr (Iff.trans ?_ (ht.injOn.mem_image_iff hs hqt)).eq)

Premises used: Submodule.colon, Set.univ, Submodule.IsMinimalPrimaryDecomposition.mem_associatedPrimes, Set.InjOn.mem_image_iff, Subtype.mk, Submodule.IsMinimalPrimaryDecomposition.injOn, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, ite_cond_congr, Submodule.IsMinimalPrimaryDecomposition.primary, Iff.trans, Iff.eq, Ideal.radical, rfl, Eq.trans
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
refine :
  ∀ (q : Submodule R M) (hqt : q ∈ t),
    Subtype.mk (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes) (q.colon Set.univ).radical ⋯ ∈ s₀ ↔
      Membership.mem (γ := Set (Ideal R))
        ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑s : Set (Submodule R M)))
        (q.colon Set.univ).radical
⊢ ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤

Tactic:
refine fun q hqt ↦ (IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite s₀ hs₀ q
    (ht.primary hqt) ⟨(q.colon Set.univ).radical, ht.mem_associatedPrimes hqt⟩ rfl).trans
    (ite_cond_congr (Iff.trans ?_ (ht.injOn.mem_image_iff hs hqt)).eq)

Premises used: Submodule.colon, Set.univ, Submodule.IsMinimalPrimaryDecomposition.mem_associatedPrimes, Set.InjOn.mem_image_iff, Subtype.mk, Submodule.IsMinimalPrimaryDecomposition.injOn, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, ite_cond_congr, Submodule.IsMinimalPrimaryDecomposition.primary, Iff.trans, Iff.eq, Ideal.radical, rfl, Eq.trans
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
s₀ : Finset (↑N.associatedPrimes : Type u_3)
hs₀ : IsLowerSet (↑s₀ : Set (↑N.associatedPrimes : Type u_3))
s : Finset (Submodule R M)
hs : s ⊆ t
hs' :
  Finset.image (fun (q : Submodule R M) ↦ (q.colon Set.univ).radical) s =
    Finset.image (Subtype.val (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes)) s₀
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
q : Submodule R M
hqt : q ∈ t
⊢ Subtype.mk (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes) (q.colon Set.univ).radical ⋯ ∈ s₀ ↔
    Membership.mem (γ := Set (Ideal R))
      ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑s : Set (Submodule R M))) (q.colon Set.univ).radical

Tactic:
grind [Finset.mem_image_of_mem]

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
rw : t.inf radical ≤ p.radical
⊢ t.inf radical ≤ p

Tactic:
rw [← hp.1.1.radical]

Premises used: And.left, Ideal.IsPrime.radical
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ p.radical

Tactic:
le_trans ?_ (radical_mono hp.1.2)

Premises used: Ideal.radical_mono, And.right, And.left, le_trans
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
refine : t.inf radical ≤ I.radical
⊢ t.inf radical ≤ p.radical

Tactic:
refine le_trans ?_ (radical_mono hp.1.2)

Premises used: Ideal.radical_mono, And.right, And.left, le_trans
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
rw : t.inf radical ≤ t.inf radical
⊢ t.inf radical ≤ I.radical

Tactic:
rw [← ht.inf_eq, ← radicalInfTopHom_apply, map_finset_inf]

Premises used: Submodule.IsMinimalPrimaryDecomposition.inf_eq, map_finset_inf, Ideal.radicalInfTopHom_apply
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ t.inf radical

Tactic:
rfl
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ t.inf radical ≤ p

Tactic:
have htp : t.inf radical ≤ p := by
    rw [← hp.1.1.radical]
    refine le_trans ?_ (radical_mono hp.1.2)
    rw [← ht.inf_eq, ← radicalInfTopHom_apply, map_finset_inf]
    rfl
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
htp : t.inf radical ≤ p
obtain : ∀ (q : Ideal R) (hqt : q ∈ t) (hqp : q.radical ≤ p), p ∈ radical '' (↑t : Set (Ideal R))
⊢ p ∈ radical '' (↑t : Set (Ideal R))

Tactic:
obtain ⟨q, hqt, hqp⟩ := (IsPrime.inf_le' hp.1.1).mp htp

Premises used: Ideal.IsPrime.inf_le', And.left, Iff.mp
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
htp : t.inf radical ≤ p
q : Ideal R
hqt : q ∈ t
hqp : q.radical ≤ p
⊢ p ∈ radical '' (↑t : Set (Ideal R))

Tactic:
⟨q, hqt, le_antisymm hqp (hp.2 ⟨isPrime_radical (ht.primary hqt),
    ht.inf_eq.symm.trans_le ((Finset.inf_le hqt).trans le_radical)⟩ hqp)⟩

Premises used: Set.Mem, Ideal.le_radical, setOf, Submodule.IsMinimalPrimaryDecomposition.inf_eq, Eq.trans_le, le_antisymm, And.right, And.intro, Submodule.IsMinimalPrimaryDecomposition.primary, Exists.intro, Ideal.isPrime_radical, Set.image, LE.le.trans, Finset.inf_le, Eq.symm
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
t : Finset (Ideal R)
ht : Submodule.IsMinimalPrimaryDecomposition I t
p : Ideal R
hp : p ∈ I.minimalPrimes
htp : t.inf radical ≤ p
q : Ideal R
hqt : q ∈ t
hqp : q.radical ≤ p
⊢ p ∈ radical '' (↑t : Set (Ideal R))

Tactic:
exact ⟨q, hqt, le_antisymm hqp (hp.2 ⟨isPrime_radical (ht.primary hqt),
    ht.inf_eq.symm.trans_le ((Finset.inf_le hqt).trans le_radical)⟩ hqp)⟩
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
⊢ N ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ N → x ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ N

Tactic:
⟨h.ne_top, fun {a b} hab ↦ ?_⟩

Premises used: InfIrred.ne_top, And.intro
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
refine : ∀ {a : R} {b : M} (hab : a • b ∈ N), b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
⊢ N ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ N → x ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ N

Tactic:
refine ⟨h.ne_top, fun {a b} hab ↦ ?_⟩
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
a_1 b_1 : M
hx : Membership.mem (γ := Set M) {x : M | a ^ n • x ∈ N} a_1
hy : Membership.mem (γ := Set M) {x : M | a ^ n • x ∈ N} b_1
⊢ Membership.mem (γ := Set M) {x : M | a ^ n • x ∈ N} (a_1 + b_1)

Tactic:
simp [N.add_mem hx hy]

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
⊢ Membership.mem (γ := Set M) {x : M | a ^ n • x ∈ N} 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h_1 : InfIrred N
a : R
b : M
hab : a • b ∈ N
n : ℕ
x : R
y : M
h : Membership.mem (γ := Set M) {x : M | a ^ n • x ∈ N} y
⊢ Membership.mem (γ := Set M) {x : M | a ^ n • x ∈ N} (x • y)

Tactic:
simp [smul_comm _ x, N.smul_mem x h]

Premises used: SMulCommClass.smul_comm, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
n m : ℕ
hnm : n ≤ m
x : M
hx : x ∈ f n
⊢ x ∈ f m

Tactic:
simpa [hnm, smul_smul, ← pow_add] using N.smul_mem (a ^ (m - n)) hx

Premises used: HSub.hSub, pow_add, smul_smul, HPow.hPow, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ Monotone f

Tactic:
have hf : Monotone f := by
    intro n m hnm x hx
    simpa [hnm, smul_smul, ← pow_add] using N.smul_mem (a ^ (m - n)) hx
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
N : Submodule R M
h : InfIrred N
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M :=
  fun (n : ℕ) ↦ { carrier := {x : M | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
obtain :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Submodule R M)
            (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) n : Submodule R M)
            (({ toFun := f, monotone' := hf : ℕ →o Submodule R M } : (a : ℕ) → Submodule R M) m : Submodule R M)),
    b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N

Tactic:
obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr ‹_› ⟨f, hf⟩

Premises used: Iff.mpr, monotone_stabilizes_iff_noetherian, OrderHom.mk