awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 * Ideal.span {z} ≤ ann
⊢ False
have hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
Tactic: have hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬ J * Ideal.span {z} ≤ I := by
    rw [← mul_assoc, hI.isPrime.mul_le, not_or, Ideal.span_singleton_le_iff_mem]
    exact ⟨hz', hJI, 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
hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
⊢ False
have pos : ∀ (hn' : n - 1 = 0), False
Tactic: by_cases hn' : n - 1 = 0
-- 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
hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
pos : ∀ (hn' : n - 1 = 0), False
⊢ False
have neg : ∀ (hn' : ¬n - 1 = 0), False
Tactic: by_cases hn' : n - 1 = 0
-- 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 * Ideal.span {z} ≤ ann
hK : I ^ (n - 1) * (J * Ideal.span {z}) ≤ ann ∧ ¬J * Ideal.span {z} ≤ I
hn' : n - 1 = 0
⊢ False
have hz'₁ : J * Ideal.span {z} ≤ ann
Tactic: simp [K, show n = 1 by grind] at hz'
Cleared hypotheses: hz'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I : Ideal R
⊢ I.minimalPrimes.Finite
have by_contra : ∀ (hI : ¬I.minimalPrimes.Finite), False
Tactic: by_contra hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I : Ideal R
hI : ¬I.minimalPrimes.Finite
⊢ False
have obtain : ∀ (I : Ideal R) (hI : ¬I.minimalPrimes.Finite)
  (hmax :
    ∀ (I_1 : Submodule R R),
      Membership.mem (γ := Set (Submodule R R)) {I : Ideal R | ¬I.minimalPrimes.Finite} I_1 → ¬I < I_1),
  False
Tactic: obtain ⟨I : Ideal R, hI : ¬ I.minimalPrimes.Finite, hmax⟩ :=
    set_has_maximal_iff_noetherian.mpr hR {I : Ideal R | ¬ I.minimalPrimes.Finite} ⟨I, hI⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax :
  ∀ (I_2 : Submodule R R),
    Membership.mem (γ := Set (Submodule R R)) {I : Ideal R | ¬I.minimalPrimes.Finite} I_2 → ¬I < I_2
⊢ False
have hmax₁ : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
Tactic: simp only [Set.mem_setOf_eq, not_imp_not] at hmax
Cleared hypotheses: hmax
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
⊢ ¬I.IsPrime
have contrapose : ∀ (hI : I.IsPrime), I.minimalPrimes.Finite
Tactic: contrapose hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
⊢ False
have h1 : ¬I.IsPrime
Tactic: have h1 : ¬ I.IsPrime := by contrapose hI; simp [minimalPrimes_eq_subsingleton_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
⊢ I ≠ ⊤
have contrapose : ∀ (hI : I = ⊤), I.minimalPrimes.Finite
Tactic: contrapose hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
⊢ False
have h2 : I ≠ ⊤
Tactic: have h2 : I ≠ ⊤ := by contrapose hI; simp [hI, minimalPrimes_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
⊢ False
have obtain : ∀ (x : R) (hx : x ∉ I) (y : R) (hy : y ∉ I) (h : x * y ∈ I), False
Tactic: obtain ⟨x, hx, y, hy, h⟩ := (not_isPrime_iff.mp h1).resolve_left h2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : x ∉ I
y : R
hy : y ∉ I
h : x * y ∈ I
⊢ False
have rw : ∀ (hx : I < I ⊔ span {x}) (y : R) (hy : I < I ⊔ span {y}) (h : x * y ∈ I), False
Tactic: rw [← Ideal.span_singleton_le_iff_mem, ← left_lt_sup] at hx hy
Cleared hypotheses: hx, y, hy, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
⊢ False
have refine : ∀ p ∈ I.minimalPrimes,
  ∀ (hp : p.IsPrime) (hI : I ≤ p) (hmin : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y),
    p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
Tactic: refine hI (((hmax _ hx).union (hmax _ hy)).subset fun p ⟨⟨hp, hI⟩, hmin⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI_2 : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
h_1 : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
have inl : ∀ (hxp : x ∈ p), p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
Tactic: rcases hp.2 (hI h) with hxp | hyp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hI_2 : ¬I.minimalPrimes.Finite
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
h_1 : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
inl : ∀ (hxp : x ∈ p), p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
have inr : ∀ (hyp : y ∈ p), p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
Tactic: rcases hp.2 (hI h) with hxp | hyp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
a b : ℕ
hab : a + b = 1
⊢ IsUnit a ∨ IsUnit b
have h : a = 1 ∨ b = 1
Tactic: have h : a = 1 ∨ b = 1 := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
a b : ℕ
hab : a + b = 1
h : a = 1 ∨ b = 1
⊢ IsUnit a ∨ IsUnit b
have f : a = 1 → IsUnit a
Tactic: apply h.imp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
a b : ℕ
hab : a + b = 1
h : a = 1 ∨ b = 1
f : a = 1 → IsUnit a
⊢ IsUnit a ∨ IsUnit b
have g : b = 1 → IsUnit b
Tactic: apply h.imp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
⊢ (↑(maximalIdeal ℕ) : Set ℕ) = {1}ᶜ
have h : ∀ (x : ℕ), x ∈ (↑(maximalIdeal ℕ) : Set ℕ) ↔ Membership.mem (γ := Set ℕ) {1}ᶜ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
⊢ Eq (α := Ideal ℕ) (maximalIdeal ℕ) (span {2, 3})
have refine : ∀ (n : ℕ) (h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n),
  Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
Tactic: refine le_antisymm (fun n h ↦ ?_) (span_le.mpr <| Set.pair_subset (by simp) (by simp))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
have inl : ∀ (lt : n < 1), Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
Tactic: obtain lt | lt := (mem_maximalIdeal_iff.mp h).lt_or_gt
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
inl : ∀ (lt : n < 1), Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
have inr : ∀ (lt : 1 < n), Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
Tactic: obtain lt | lt := (mem_maximalIdeal_iff.mp h).lt_or_gt
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
lt : n < 1
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
have inl : ∀ (h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0) (lt : LT.lt (α := ℕ) 0 1),
  Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) 0
Tactic: obtain rfl := lt_one_iff.mp lt
Cleared hypotheses: n, h, lt
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
⊢ Membership.mem (γ := Ideal ℕ) (span s) 1 ↔ 1 ∈ s
have rw : 1 ∉ (↑(span s) : Set ℕ) ↔ 1 ∉ s
Tactic: rw [← SetLike.mem_coe, ← not_iff_not]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
⊢ 1 ∉ (↑(span s) : Set ℕ) ↔ 1 ∉ s
have simp_rw : {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ
Tactic: simp_rw [← Set.mem_compl_iff, ← Set.singleton_subset_iff, Set.subset_compl_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
⊢ {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ
have rw : (↑(span s) : Set ℕ) ⊆ {1}ᶜ ↔ s ⊆ {1}ᶜ
Tactic: rw [Set.subset_compl_comm, ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
rw : (↑(span s) : Set ℕ) ⊆ {1}ᶜ ↔ s ⊆ {1}ᶜ
⊢ {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ
have rw₁ : (↑(span s) : Set ℕ) ⊆ (↑(maximalIdeal ℕ) : Set ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
Tactic: rw [Set.subset_compl_comm, ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
rw : (↑(span s) : Set ℕ) ⊆ {1}ᶜ ↔ s ⊆ {1}ᶜ
rw₁ : (↑(span s) : Set ℕ) ⊆ (↑(maximalIdeal ℕ) : Set ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
⊢ {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ
have rw₂ : LE.le (α := Ideal ℕ) (span s) (maximalIdeal ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
Tactic: rw [Set.subset_compl_comm, ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
rw : (↑(span s) : Set ℕ) ⊆ {1}ᶜ ↔ s ⊆ {1}ᶜ
rw₁ : (↑(span s) : Set ℕ) ⊆ (↑(maximalIdeal ℕ) : Set ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
rw₂ : LE.le (α := Ideal ℕ) (span s) (maximalIdeal ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
⊢ {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ
have rw₃ : s ⊆ (↑(maximalIdeal ℕ) : Set ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
Tactic: rw [Set.subset_compl_comm, ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
s : Set ℕ
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) 1 ↔ 1 ∈ s
have rw : Membership.mem (γ := AddSubmonoid ℕ) (Submodule.toAddSubmonoid (Submodule.span ℕ s)) 1 ↔ 1 ∈ s
Tactic: rw [← Submodule.span_nat_eq_addSubmonoidClosure]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
⊢ P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
have refine_1 : (P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) → P.IsPrime
Tactic: refine .symm ⟨?_, fun h ↦ or_iff_not_imp_left.mpr fun h0 ↦ or_iff_not_imp_right.mpr fun hsp ↦
    (le_maximalIdeal h.ne_top).antisymm fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
refine_1 : (P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) → P.IsPrime
⊢ P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
have refine_2 : ∀ (h : P.IsPrime) (h0 : ¬P = ⊥) (hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) (n : ℕ)
  (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n), n ∈ P
Tactic: refine .symm ⟨?_, fun h ↦ or_iff_not_imp_left.mpr fun h0 ↦ or_iff_not_imp_right.mpr fun hsp ↦
    (le_maximalIdeal h.ne_top).antisymm fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
p : ℕ
hp : Nat.Prime p
⊢ IsPrime (α := ℕ) (span {p})
have refine_1 : Prime p
Tactic: rwa [span_singleton_prime (by simp [hp.ne_zero]), ← Nat.prime_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ¬P = ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
⊢ n ∈ P
have refine_2 : ∀ (h0 : ∃ x ∈ P, x ∉ ⊥) (hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) (n : ℕ)
  (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n), n ∈ P
Tactic: rw [← le_bot_iff, SetLike.not_le_iff_exists] at h0
Cleared hypotheses: h0, hsp, n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
⊢ n ∈ P
have hp : p ∈ P
Tactic: have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
⊢ n ∈ P
have hp0 : p ≠ 0
Tactic: have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
⊢ n ∈ P
have this : p ≠ 1
Tactic: have : p ≠ 1 := ne_of_mem_of_not_mem hp P.one_notMem
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
⊢ n ∈ P
have prime : Nat.Prime p
Tactic: have prime : p.Prime := Nat.prime_iff_not_exists_mul_eq.mpr <| .intro (by lia)
    fun ⟨m, n, hm, hn, eq⟩ ↦ have := mul_ne_zero_iff.mp (eq ▸ hp0)
    (h.mem_or_mem (eq ▸ hp)).elim (Nat.find_min h0 hm ⟨·, this.1⟩) (Nat.find_min h0 hn ⟨·, this.2⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
⊢ n ∈ P
have hsp₁ : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}
Tactic: push Not at hsp
Cleared hypotheses: hsp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}
⊢ n ∈ P
have refine_2 : ∀ (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}), n ∈ P
Tactic: have ⟨q, hq, hqp⟩ := SetLike.exists_of_lt
    ((P.span_singleton_le_iff_mem.mpr hp).lt_of_ne (hsp p prime).symm)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
⊢ n ∈ P
have refine_2 : ∀ (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0), 0 ∈ P
Tactic: obtain rfl | hn1 := eq_or_ne n 0
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
refine_2 : ∀ (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0), 0 ∈ P
⊢ n ∈ P
have refine_2₁ : ∀ (hn1 : n ≠ 0), n ∈ P
Tactic: obtain rfl | hn1 := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (hypothesis)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
hn1 : n ≠ 0
⊢ n ∈ P
have this₁ : n ≠ 1
Tactic: have : n ≠ 1 := Nat.mem_maximalIdeal_iff.mp hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
p : ℕ := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0
hp : p ∈ P
hp0 : p ≠ 0
this_1 : p ≠ 1
prime : Nat.Prime p
hsp : ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}
q : ℕ
hq : q ∈ P
hqp : q ∉ span {p}
hn1 : n ≠ 0
this : n ≠ 1
⊢ n ∈ P
have refine_2 : ∀ (a b : ℕ) (eq : a * p + b * q = n ^ (p.pred * q.pred)), n ∈ P
Tactic: have ⟨a, b, eq⟩ := Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le p q _
    (by simp [prime.coprime_iff_not_dvd.mpr (Ideal.mem_span_singleton.not.mp hqp)])
    (Nat.lt_pow_self (show 1 < n by lia)).le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.NatInt (goal)
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
refine_2 refine_2₁ refine_2₂ : n ∈ P
⊢ n ∈ P
have refine_2₃ : let p := Nat.find (p := fun (n : ℕ) ↦ n ∈ P ∧ n ∉ ⊥) h0;
∀ (hp : p ∈ P) (hp0 : p ≠ 0), n ∈ P
Tactic: classical
  let p := Nat.find h0
  have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
  have : p ≠ 1 := ne_of_mem_of_not_mem hp P.one_notMem
  have prime : p.Prime := Nat.prime_iff_not_exists_mul_eq.mpr <| .intro (by lia)
    fun ⟨m, n, hm, hn, eq⟩ ↦ have := mul_ne_zero_iff.mp (eq ▸ hp0)
    (h.mem_or_mem (eq ▸ hp)).elim (Nat.find_min h0 hm ⟨·, this.1⟩) (Nat.find_min h0 hn ⟨·, this.2⟩)
  push Not at hsp
  have ⟨q, hq, hqp⟩ := SetLike.exists_of_lt
    ((P.span_singleton_le_iff_mem.mpr hp).lt_of_ne (hsp p prime).symm)
  obtain rfl | hn1 := eq_or_ne n 0
  · exact Ideal.zero_mem _
  have : n ≠ 1 := Nat.mem_maximalIdeal_iff.mp hn
  have ⟨a, b, eq⟩ := Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le p q _
    (by simp [prime.coprime_iff_not_dvd.mpr (Ideal.mem_span_singleton.not.mp hqp)])
    (Nat.lt_pow_self (show 1 < n by lia)).le
  exact h.mem_of_pow_mem _ (eq ▸ add_mem (P.mul_mem_left _ hp) (P.mul_mem_left _ hq))