awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
have hy2₁ : 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
Cleared hypotheses: hy2
-- 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 ∈ S
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
have neg : LinearMap.range (mkLinearMap S M) ≤ localized₀ S (mkLinearMap S M) q
Tactic: rw [eq_top_iff, ← map_le_iff_le_comap, map_top]
-- 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 ∈ S
x : M
⊢ Membership.mem (α := LocalizedModule S M) (localized₀ S (mkLinearMap S M) q)
    ((mkLinearMap S M : (a : M) → LocalizedModule S M) x : LocalizedModule S M)
have 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)
Tactic: simp_rw [mem_localized₀, IsLocalizedModule.mk'_eq_iff, ← LinearMap.map_smul_of_tower]
-- 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
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
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) N) = ⨅ q ∈ s, q
have 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)
Tactic: rw [← ht.inf_eq, ← localized₀FrameHom_apply, map_finset_inf, Submodule.comap_finsetInf]
-- 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
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
⊢ 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)
have 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)
Tactic: simp_rw [Function.comp_def, id_eq, localized₀FrameHom_apply]
-- 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
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 ⊤
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have rw : Eq (α := Submodule R M) (t.inf fun (a : Submodule R M) ↦ if a ∈ s then a else ⊤) (⨅ 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]
-- 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
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)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have 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)
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]
-- 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
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)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have rw₂ : Eq (α := Submodule R M) (((Finset.filter (Membership.mem s) t).inf fun (a : Submodule R M) ↦ a) ⊓ ⊤) (⨅ 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]
-- 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
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)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have rw₃ : Eq (α := Submodule R M) ((Finset.filter (Membership.mem s) t).inf fun (a : Submodule R M) ↦ a) (⨅ 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]
-- 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
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)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have rw₄ : Eq (α := Submodule R M) ((t ∩ s).inf fun (a : Submodule R M) ↦ a) (⨅ 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]
-- 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
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)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have rw₅ : Eq (α := Submodule R M) (s.inf fun (a : Submodule R M) ↦ a) (⨅ 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]
-- 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
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)
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have rw₆ : Eq.{u_4 + 1} (α := Submodule R M) (⨅ a ∈ s, a) (⨅ 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]
-- 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
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
⊢ Eq (α := Submodule R M) (t.inf fun (i : Submodule R M) ↦ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) i))
    (⨅ q ∈ s, q)
have suffices : ∀ q ∈ t, comap f (localized₀ S f q) = if q ∈ s then q else ⊤
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]
-- 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
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 ⊤
have refine : ∀ (q : Submodule R M) (hqt : q ∈ t),
  Subtype.mk (p := fun (x : Ideal R) ↦ x ∈ N.associatedPrimes) (q.colon Set.univ).radical sorry ∈ 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: 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)
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
have rw : t.inf radical ≤ p.radical
Tactic: rw [← hp.1.1.radical]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
have refine : t.inf radical ≤ I.radical
Tactic: refine le_trans ?_ (radical_mono hp.1.2)
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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 ≤ I.radical
have rw : t.inf radical ≤ t.inf radical
Tactic: rw [← ht.inf_eq, ← radicalInfTopHom_apply, map_finset_inf]
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
⊢ p ∈ radical '' (↑t : Set (Ideal R))
have htp : 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
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ p ∈ radical '' (↑t : Set (Ideal R))
have obtain : ∀ (q : Ideal R) (hqt : q ∈ t) (hqp : q.radical ≤ p), p ∈ radical '' (↑t : Set (Ideal R))
Tactic: obtain ⟨q, hqt, hqp⟩ := (IsPrime.inf_le' hp.1.1).mp htp
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
have refine : ∀ {a : R} {b : M} (hab : a • b ∈ N), b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
Tactic: refine ⟨h.ne_top, fun {a b} hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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' := ⋯ }
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
have hf : 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
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
have 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
Tactic: obtain ⟨n, hn⟩ := monotone_stabilizes_iff_noetherian.mpr ‹_› ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (hypothesis)
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
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
have h₁ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
Tactic: rcases h with ⟨-, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Lasker (goal)
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
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
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)
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
⊢ b ∈ N ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ N
have specialize : f n ⊓ (N + HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤) = N
Tactic: specialize @h (f n) (N + a ^ n • ⊤) ?_