awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ (fun (J : Submodule R M) ↦ (J.colon Set.univ).radical) '' (↑t : Set (Submodule R M)) = N.associatedPrimes
have 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
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ (q.colon Set.univ).radical ∈ N.associatedPrimes
have 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
Tactic: rw [← ht.image_radical_eq_associated_primes]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = if p ∈ s₀ then q else ⊤
have pos : ∀ (hp : p ∈ s₀), comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = q
Tactic: split_ifs with hp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = if p ∈ s₀ then q else ⊤
have neg : ∀ (hp : p ∉ s₀), comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
Tactic: split_ifs with hp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
have pos : ∀ (x : M) (hx : x ∈ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q)), x ∈ q
Tactic: refine le_antisymm (fun x hx ↦ ?_) (map_le_iff_le_comap.mp (map_le_localized₀ S f q))
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
⊢ x ∈ q
have 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
Tactic: obtain ⟨b, hb, a, ha⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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)
⊢ x ∈ q
have 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)
Tactic: rw [IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
⊢ x ∈ q
have pos : ∀ (c : ↥S) (hc : c • b = c • a • x), x ∈ q
Tactic: obtain ⟨c, hc⟩ := (IsLocalizedModule.eq_iff_exists S f).mp ha
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
⊢ x ∈ q
have hb₁ : (↑c : R) • b ∈ q
Tactic: replace hb := q.smul_mem c hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
⊢ x ∈ q
have hb₁ : (c * a) • x ∈ q
Tactic: rw [← Submonoid.smul_def, hc, smul_smul] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ x ∈ q
have pos : (↑(c * a) : R) ∉ (q.colon Set.univ).radical
Tactic: apply (hqp.mem_or_mem hb).resolve_right
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
have contrapose : ∀ (hp : (↑(q.colon Set.univ) : Set R) ⊆ ⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)), p ∈ s₀
Tactic: contrapose hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
⊢ p ∈ s₀
have obtain : ∀ (r : (↑N.associatedPrimes : Type u_3)) (hrs : r ∈ s₀) (h : q.colon Set.univ ≤ (↑r : Ideal R)), p ∈ s₀
Tactic: obtain ⟨r, hrs, h⟩ := (subset_union_prime p p fun i _ _ _ ↦ i.2.1).mp hp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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 ∈ s₀
have h₁ : (↑p : Ideal R) ≤ (↑r : Ideal R)
Tactic: rw [← r.2.1.radical_le_iff, hq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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) = ⊤
have hq₁ : ¬(↑(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
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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)
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
have 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) = ⊤
Tactic: obtain ⟨y, hy1, hy2⟩ := Set.not_subset_iff_exists_mem_notMem.mp hq
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
have simp : ∀ (a : Ideal R) (b : a ∈ N.associatedPrimes)
  (i : Subtype.mk (p := fun (a : Ideal R) ↦ a ∈ N.associatedPrimes) a b ∈ s₀), y ∉ a
Tactic: simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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₀
⊢ y ∉ r
have contrapose : ∀ (hy2 : y ∈ r), Membership.mem (γ := Set R) (⋃ r ∈ s₀, (↑(↑r : Ideal R) : Set R)) y
Tactic: contrapose hy2
Cleared hypotheses: hy2