awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hI : I ∈ (N.colon {x}).minimalPrimes
pos : ∀ (hx : x ∈ N), ∃ (x' : M), I = N.colon {x'}
⊢ ∃ (x' : M), I = N.colon {x'}
have neg : ∀ (hx : x ∉ N), ∃ (x' : M), I = N.colon {x'}
Tactic: by_cases hx : x ∈ N
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
have obtain : ∀ (n : ℕ) (hn : ann.radical ^ n ≤ ann), ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
Tactic: obtain ⟨n, hn⟩ := ann.exists_radical_pow_le_of_fg ann.radical.fg_of_isNoetherianRing
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn : ann.radical ^ n ≤ ann
⊢ n ≠ 0
have contrapose : ∀ (hn : n = 0), ¬ann.radical ^ n ≤ ann
Tactic: contrapose hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn : ann.radical ^ n ≤ ann
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
have hn0 : n ≠ 0
Tactic: have hn0 : n ≠ 0 := by contrapose hn; simpa [hn, ann]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn : ann.radical ^ n ≤ ann
hn0 : n ≠ 0
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
have h : ann.minimalPrimes.Finite
Tactic: have h := ann.finite_minimalPrimes_of_isNoetherianRing R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn : ann.radical ^ n ≤ ann
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn0₁ : n ≠ 0
h₁ : ann.minimalPrimes.Finite
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
have hn₁ : (I ⊓ (h₁.toFinset (s := ann.minimalPrimes).erase I).inf id) ^ n ≤ ann
Tactic: rw [← ann.sInf_minimalPrimes, ← h.coe_toFinset, ← h.toFinset.inf_id_eq_sInf,
      ← Finset.insert_erase (h.mem_toFinset.mpr hI), Finset.inf_insert, id_eq] at hn
Cleared hypotheses: hn, hn0, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : (I ⊓ (h.toFinset (s := ann.minimalPrimes).erase I).inf id) ^ n ≤ ann
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
have hn₁ : I ^ n * (h.toFinset (s := ann.minimalPrimes).erase I).inf id ^ n ≤ ann
Tactic: grw [← Ideal.mul_le_inf, mul_pow] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : I ^ n * (h.toFinset (s := ann.minimalPrimes).erase I).inf id ^ n ≤ ann
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
have refine : ¬(h.toFinset (s := ann.minimalPrimes).erase I).inf id ^ n ≤ I
Tactic: refine ⟨n, hn0, ((h.toFinset.erase I).inf id) ^ n, hn, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : I ^ n * (h.toFinset (s := ann.minimalPrimes).erase I).inf id ^ n ≤ ann
⊢ ¬(h.toFinset (s := ann.minimalPrimes).erase I).inf id ^ n ≤ I
have this : ∀ (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes), K = I
Tactic: have (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes) : K = I :=
      le_antisymm hKI (hI.2 hK.1 hKI)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
⊢ ∃ (x' : M), I = N.colon {x'}
have key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
Tactic: have key : ∃ n ≠ 0, ∃ J : Ideal R, I ^ n * J ≤ ann ∧ ¬ J ≤ I := by
    -- let `n` be large enough so that `ann.radical ^ n ≤ ann` (uses Noetherian)
    obtain ⟨n, hn⟩ := ann.exists_radical_pow_le_of_fg ann.radical.fg_of_isNoetherianRing
    have hn0 : n ≠ 0 := by contrapose hn; simpa [hn, ann]
    -- then take `J` to be the product of the other minimal primes raised to the `n`th power
    have h := ann.finite_minimalPrimes_of_isNoetherianRing R
    rw [← ann.sInf_minimalPrimes, ← h.coe_toFinset, ← h.toFinset.inf_id_eq_sInf,
      ← Finset.insert_erase (h.mem_toFinset.mpr hI), Finset.inf_insert, id_eq] at hn
    grw [← Ideal.mul_le_inf, mul_pow] at hn
    refine ⟨n, hn0, ((h.toFinset.erase I).inf id) ^ n, hn, ?_⟩
    have (K : Ideal R) (hKI : K ≤ I) (hK : K ∈ ann.minimalPrimes) : K = I :=
      le_antisymm hKI (hI.2 hK.1 hKI)
    simpa [hI.isPrime.pow_le_iff hn0, hI.isPrime.inf_le', imp_not_comm, not_imp_not]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
⊢ ∃ (x' : M), I = N.colon {x'}
have neg : ∀ (hn0 : Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key ≠ 0) (J : Ideal R)
  (hJ : I ^ Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key * J ≤ ann)
  (hJI : ¬J ≤ I), ∃ (x' : M), I = N.colon {x'}
Tactic: obtain ⟨hn0, J, hJ, hJI⟩ := Nat.find_spec key
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
y : R
hy : y ∈ K
p : R
hp : p ∈ I
⊢ p ∈ N.colon {y • x}
have rw : p * y ∈ N.colon {x}
Tactic: rw [mem_colon_singleton, smul_smul, ← mem_colon_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
y : R
hy : y ∈ K
p : R
hp : p ∈ I
⊢ p * y ∈ N.colon {x}
have a : p * y ∈ I ^ n * J
Tactic: apply hJ
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hn0 : n ≠ 0
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
⊢ ∃ (x' : M), I = N.colon {x'}
have step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
Tactic: have step1 : ∀ y ∈ K, I ≤ colon N {y • x} := by
    intro y hy p hp
    rw [mem_colon_singleton, smul_smul, ← mem_colon_singleton]
    apply hJ
    simpa [K, ← mul_assoc, mul_pow_sub_one hn0] using mul_mem_mul hp hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
step2 : ∃ (y : ↥K), N.colon {y • x} ≤ I
⊢ ∃ (x' : M), I = N.colon {x'}
have obtain : ∀ (y : ↥K) (hyI : N.colon {y • x} ≤ I), ∃ (x' : M), I = N.colon {x'}
Tactic: obtain ⟨y, hyI⟩ := step2
Cleared hypotheses: step2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
⊢ ∃ (x' : M), I = N.colon {x'}
have neg : ∃ (y : ↥K), N.colon {y • x} ≤ I
Tactic: suffices step2 : ∃ y : K, colon N {y • x} ≤ I by
    obtain ⟨y, hyI⟩ := step2
    exact ⟨y • x, le_antisymm (step1 y y.2) hyI⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
⊢ ∃ (y : ↥K), N.colon {y • x} ≤ I
have neg : ∀ (h' : ∀ (y : ↥K), ¬N.colon {y • x} ≤ I), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
h' : ∀ (y : ↥K), ¬N.colon {y • x} ≤ I
⊢ False
have h'₁ : ∀ (y : ↥K), ∃ x_1 ∈ N.colon {y • x}, x_1 ∉ I
Tactic: simp only [SetLike.not_le_iff_exists] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
h' : ∀ (y : ↥K), ∃ x_1 ∈ N.colon {y • x}, x_1 ∉ I
⊢ False
have neg : ∀ (f : (y : ↥K) → R) (g : ∀ (y : ↥K), f y ∈ N.colon {y • x}) (h : ∀ (y : ↥K), f y ∉ I), False
Tactic: choose f g h using h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
⊢ False
have neg : ∀ (s : Finset ↥K) (hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤), False
Tactic: obtain ⟨s, hs⟩ : (⊤ : Submodule R K).FG := Module.Finite.fg_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤
z : R := ∏ y ∈ s, f y
⊢ False
have hz : z ∉ I
Tactic: have hz : z ∉ I := by simp [z, hI.isPrime.prod_mem_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
⊢ K ≤ N.colon {z • x}
have rw : ∀ (hs : map (Submodule.subtype K) (span R (↑s : Set ↥K)) = K),
  let z : R := ∏ y ∈ s, f y;
  ∀ (hz : z ∉ I), K ≤ N.colon {z • x}
Tactic: rw [← (map_injective_of_injective K.subtype_injective).eq_iff, map_subtype_top] at hs
Cleared hypotheses: hs, z, hz
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R (↑s : Set ↥K)) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
⊢ K ≤ N.colon {z • x}
have rw : (↑s : Set ↥K) ⊆ (⇑(Submodule.subtype K) : (a : ↥K) → R) ⁻¹' (↑(N.colon {z • x}) : Set R)
Tactic: rw [← hs, map_span, span_le, Set.image_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R (↑s : Set ↥K)) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
i : ↥K
hi : i ∈ (↑s : Set ↥K)
⊢ Membership.mem (γ := Set ↥K) ((⇑(Submodule.subtype K) : (a : ↥K) → R) ⁻¹' (↑(N.colon {z • x}) : Set R)) i
have rw : z ∈ N.colon {HSMul.hSMul (α := R) ((Submodule.subtype K : (a : ↥K) → R) i : R) x}
Tactic: rw [Set.mem_preimage, SetLike.mem_coe, mem_colon_singleton, smul_comm, ← mem_colon_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R (↑s : Set ↥K)) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
i : ↥K
hi : i ∈ (↑s : Set ↥K)
⊢ z ∈ N.colon {HSMul.hSMul (α := R) ((Submodule.subtype K : (a : ↥K) → R) i : R) x}
have obtain : ∀ (y : R) (hy : z = f i * y), z ∈ N.colon {HSMul.hSMul (α := R) ((Submodule.subtype K : (a : ↥K) → R) i : R) x}
Tactic: obtain ⟨y, hy : z = f i * y⟩ := Finset.dvd_prod_of_mem f hi
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
⊢ False
have hz' : K ≤ N.colon {z • x}
Tactic: have hz' : K ≤ colon N {z • x} := by
    rw [← (map_injective_of_injective K.subtype_injective).eq_iff, map_subtype_top] at hs
    rw [← hs, map_span, span_le, Set.image_subset_iff]
    intro i hi
    rw [Set.mem_preimage, SetLike.mem_coe, mem_colon_singleton, smul_comm, ← mem_colon_singleton]
    obtain ⟨y, hy : z = f i * y⟩ := Finset.dvd_prod_of_mem f hi
    exact hy ▸ Ideal.mul_mem_right y _ (g i)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
⊢ K * Ideal.span {z} ≤ ann
have rw : ∀ z_1 ∈ K, z * z_1 ∈ ann
Tactic: rw [mul_comm, Ideal.span_singleton_mul_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (hypothesis)
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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
⊢ False
have hz'₁ : K * Ideal.span {z} ≤ ann
Tactic: replace hz' : K * Ideal.span {z} ≤ ann := by
    rw [mul_comm, Ideal.span_singleton_mul_le_iff]
    intro i hi
    simpa only [ann, mem_colon_singleton, mul_comm, mul_smul] using hz' hi
Cleared hypotheses: hz'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Colon (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
I : Ideal R
x : M
inst_3 : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ (n : ℕ), n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ≠ 0 ∧ ∃ (J : Ideal R), I ^ n * J ≤ ann ∧ ¬J ≤ I) key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : (y : ↥K) → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : Eq (α := Submodule R ↥K) (span R (↑s : Set ↥K)) ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K * Ideal.span {z} ≤ ann
⊢ I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
have rw : I ^ (n - 1) * J * Ideal.span {z} ≤ ann ∧ ¬J ≤ I ∧ z ∉ I
Tactic: rw [← mul_assoc, hI.isPrime.mul_le, not_or, Ideal.span_singleton_le_iff_mem]