awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
x : M
hp : IsPrime.{u_1} (α := R) ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
q : Submodule R M
hq1 : q ∈ {x_1 ∈ t | x ∉ x_1}
hq2 : (q.colon Set.univ).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)))
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)

Tactic:
⟨q, Finset.mem_of_mem_filter q hq1, hq2⟩

Premises used: Set.Mem, setOf, Finset.mem_of_mem_filter, And.intro, Exists.intro, Set.image
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
x : M
hp : IsPrime.{u_1} (α := R) ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
q : Submodule R M
hq1 : q ∈ {x_1 ∈ t | x ∉ x_1}
hq2 : (q.colon Set.univ).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)))
    ({x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)

Tactic:
exact ⟨q, Finset.mem_of_mem_filter q hq1, hq2⟩
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
replace :
  ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
replace₁ :
  ∀
    (h :
      ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical),
    (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
replace₂ :
  ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical
replace₃ replace₄ :
  ∀
    (h :
      ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical),
    (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
h :
  ∀
    (h :
      ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
    (p : Ideal R),
    Membership.mem (γ := Set (Ideal R))
        ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p ↔
      p ∈ N.associatedPrimes
h₁ :
  ∀
    (h :
      ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical)
    (p : Ideal R),
    Membership.mem (γ := Set (Ideal R))
        ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p →
      p ∈ N.associatedPrimes
h₂ h₃ :
  ∀
    (h :
      ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun (q : Submodule R M) ↦ (q.colon Set.univ).radical),
    ∀ p ∈ N.associatedPrimes,
      Membership.mem (γ := Set (Ideal R))
        ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) p
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes

Tactic:
classical
  replace h x : radical (N.colon {x}) = (t.filter (x ∉ ·)).inf fun q ↦ radical (q.colon .univ) := by
    simp_rw [← ht.inf_eq, colon_finsetInf, ← radicalInfTopHom_apply, map_finset_inf,
      Function.comp_def, radicalInfTopHom_apply, id_eq]
    rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
  ext p
  constructor
  · rintro ⟨q, hqt, rfl⟩
    obtain ⟨x, hxt, hxq⟩ := SetLike.not_le_iff_exists.mp (ht.minimal hqt)
    use (ht.primary hqt).isPrime_radical_colon, x
    rw [h, ← Finset.insert_erase (Finset.mem_filter.mpr ⟨hqt, hxq⟩), Finset.inf_insert,
      eq_comm, inf_eq_left, Finset.le_inf_iff]
    simp only [mem_finsetInf, Finset.mem_erase] at hxt
    grind
  · rintro ⟨hp, x, rfl⟩
    rw [h] at hp ⊢
    obtain ⟨q, hq1, hq2⟩ := eq_inf_of_isPrime_inf hp
    exact ⟨q, Finset.mem_of_mem_filter q hq1, hq2⟩

Premises used: eq_comm, Finset.inf_insert, Finset.mem_erase, Finset.le_inf_iff, inf_eq_left, Submodule.mem_finsetInf, rfl
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
rw :
  Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) (q.colon Set.univ).radical
⊢ (q.colon Set.univ).radical ∈ N.associatedPrimes

Tactic:
rw [← ht.image_radical_eq_associated_primes]

Premises used: Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) (q.colon Set.univ).radical

Tactic:
Set.mem_image_of_mem _ hq

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.RingTheory.Lasker
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
q : Submodule R M
hq : q ∈ t
⊢ Membership.mem (γ := Set (Ideal R))
    ((fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M))) (q.colon Set.univ).radical

Tactic:
exact Set.mem_image_of_mem _ hq

Premises used: Set.mem_image_of_mem
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
set :
  let S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl;
  comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = if p ∈ s₀ then q else ⊤
⊢ 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) q) =
    if p ∈ s₀ then q else ⊤

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
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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
pos : ∀ (hp : p ∈ s₀), comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = q
neg : ∀ (hp : p ∉ s₀), comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = if p ∈ s₀ then q else ⊤

Tactic:
split_ifs with hp
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = q

Tactic:
le_antisymm (fun x hx ↦ ?_) (map_le_iff_le_comap.mp (map_le_localized₀ S f q))

Premises used: le_antisymm, Iff.mp, Submodule.map_le_iff_le_comap, Submodule.map_le_localized₀
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
pos : ∀ (x : M) (hx : x ∈ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q)), x ∈ q
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = q

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (map_le_iff_le_comap.mp (map_le_localized₀ S f q))

Premises used: le_antisymm, Iff.mp, Submodule.map_le_iff_le_comap, Submodule.map_le_localized₀
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x : M
hx : x ∈ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q)
pos :
  ∀ (b : M) (hb : b ∈ q) (a : ↥S)
    (ha :
      Eq (α := LocalizedModule S M) (IsLocalizedModule.mk' (mkLinearMap S M) b a)
        ((mkLinearMap S M : (a : M) → LocalizedModule S M) x)),
    x ∈ q
⊢ x ∈ q

Tactic:
obtain ⟨b, hb, a, ha⟩ := hx
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
hb : b ∈ q
a : ↥S
ha :
  Eq (α := LocalizedModule S M) (IsLocalizedModule.mk' (mkLinearMap S M) b a)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) x)
⊢ Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) b : LocalizedModule S M)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) (a • x) : LocalizedModule S M)

Tactic:
rw [IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower] at ha

Premises used: 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
hb : b ∈ q
a : ↥S
ha :
  Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) b : LocalizedModule S M)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) (a • x) : LocalizedModule S M)
pos : ∀ (c : ↥S) (hc : c • b = c • a • x), x ∈ q
⊢ x ∈ q

Tactic:
obtain ⟨c, hc⟩ := (IsLocalizedModule.eq_iff_exists S f).mp ha

Premises used: Iff.mp, IsLocalizedModule.eq_iff_exists
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
hb : b ∈ q
a : ↥S
ha :
  Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) b : LocalizedModule S M)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) (a • x) : LocalizedModule S M)
c : ↥S
hc : c • b = c • a • x
⊢ (↑c : R) • b ∈ q

Tactic:
replace hb := q.smul_mem c hb
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha :
  Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) b : LocalizedModule S M)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) (a • x) : LocalizedModule S M)
c : ↥S
hc : c • b = c • a • x
hb : (↑c : R) • b ∈ q
⊢ (c * a) • x ∈ q

Tactic:
rw [← Submonoid.smul_def, hc, smul_smul] at hb

Premises used: smul_smul, Submonoid.smul_def
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha :
  Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) b : LocalizedModule S M)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) (a • x) : LocalizedModule S M)
c : ↥S
hc : c • b = c • a • x
hb : (c * a) • x ∈ q
pos : (↑(c * a) : R) ∉ (q.colon Set.univ).radical
⊢ x ∈ q

Tactic:
apply (hqp.mem_or_mem hb).resolve_right

Premises used: Or.resolve_right, Submodule.IsPrimary.mem_or_mem
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∈ s₀
x b : M
a : ↥S
ha :
  Eq (α := LocalizedModule S M) ((mkLinearMap S M : (a : M) → LocalizedModule S M) b : LocalizedModule S M)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) (a • x) : LocalizedModule S M)
c : ↥S
hc : c • b = c • a • x
hb : (c * a) • x ∈ q
⊢ (↑(c * a) : R) ∉ (q.colon Set.univ).radical

Tactic:
grind [Submonoid.mem_iInf, mem_primeCompl_iff]

Premises used: Ideal.mem_primeCompl_iff, Submonoid.mem_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
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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
contrapose : ∀ (hp : (↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)), p ∈ s₀
⊢ ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)

Tactic:
contrapose hp
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : (↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
obtain : ∀ (r : (↑N.associatedPrimes : Type u_3)) (hrs : r ∈ s₀) (h : q.colon Set.univ ≤ (↑r : Ideal R)), p ∈ s₀
⊢ p ∈ s₀

Tactic:
obtain ⟨r, hrs, h⟩ := (subset_union_prime p p fun i _ _ _ ↦ i.2.1).mp hp

Premises used: LocalizedModule.r, Iff.mp, Ideal.subset_union_prime, Subtype.property, Submodule.IsAssociatedPrime.toIsPrime
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : (↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
r : (↑N.associatedPrimes : Type u_3)
hrs : r ∈ s₀
h : q.colon Set.univ ≤ (↑r : Ideal R)
⊢ (↑p : Ideal R) ≤ (↑r : Ideal R)

Tactic:
rw [← r.2.1.radical_le_iff, hq] at h

Premises used: Ideal.IsPrime.radical_le_iff, Subtype.property, Submodule.IsAssociatedPrime.toIsPrime
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : (↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
r : (↑N.associatedPrimes : Type u_3)
hrs : r ∈ s₀
h : (↑p : Ideal R) ≤ (↑r : Ideal R)
⊢ p ∈ s₀

Tactic:
hs₀ h hrs
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : (↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)
r : (↑N.associatedPrimes : Type u_3)
hrs : r ∈ s₀
h : (↑p : Ideal R) ≤ (↑r : Ideal R)
⊢ p ∈ s₀

Tactic:
exact hs₀ h hrs
-- 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)
hq : (q.colon Set.univ).radical = (↑p : Ideal R)
S : Submonoid R := ⨅ q ∈ s₀, (↑q : Ideal R).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
⊢ ¬(↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)

Tactic:
replace hq : ¬ (q.colon Set.univ : Set R) ⊆ ⋃ r ∈ s₀, r := by
      contrapose hp
      obtain ⟨r, hrs, h⟩ := (subset_union_prime p p fun i _ _ _ ↦ i.2.1).mp hp
      rw [← r.2.1.radical_le_iff, hq] at h
      exact hs₀ h hrs
-- 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)
neg :
  ∀ (y : R) (hy1 : y ∈ (↑(q.colon Set.univ) : Set R)) (hy2 : y ∉ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)),
    comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤

Tactic:
obtain ⟨y, hy1, hy2⟩ := Set.not_subset_iff_exists_mem_notMem.mp hq

Premises used: Set.not_subset_iff_exists_mem_notMem, Iff.mp
-- 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)
simp :
  ∀ (a : Ideal R) (b : a ∈ N.associatedPrimes)
    (i : Subtype.mk (p := fun (a : Ideal R) ↦ a ∈ N.associatedPrimes) a b ∈ s₀), y ∉ a
⊢ y ∈ S

Tactic:
simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S]

Premises used: Subtype.forall, Ideal.mem_primeCompl_iff, Submonoid.mem_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
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)
r : Ideal R
hrI : r ∈ N.associatedPrimes
hrs : Subtype.mk (p := fun (a : Ideal R) ↦ a ∈ N.associatedPrimes) r hrI ∈ s₀
contrapose : ∀ (hy2 : y ∈ r), Membership.mem (γ := Set R) (⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)) y
⊢ y ∉ r

Tactic:
contrapose 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)
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:
Set.mem_biUnion hrs hy2

Premises used: Set.Mem, Set.mem_biUnion