awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I : Ideal R
by_contra : ∀ (hI : ¬I.minimalPrimes.Finite), False
⊢ I.minimalPrimes.Finite

Tactic:
by_contra hI
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I : Ideal R
hI : ¬I.minimalPrimes.Finite
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
⊢ 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⟩

Premises used: Iff.mpr, Ideal.minimalPrimes, setOf, Set.Finite, Ideal, Exists.intro, set_has_maximal_iff_noetherian, Not
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
⊢ ∀ (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

Premises used: Set.mem_setOf_eq, not_imp_not
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
contrapose : ∀ (hI : I.IsPrime), I.minimalPrimes.Finite
⊢ ¬I.IsPrime

Tactic:
contrapose hI
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
hI : I.IsPrime
⊢ I.minimalPrimes.Finite

Tactic:
simp [minimalPrimes_eq_subsingleton_self]

Premises used: Ideal.minimalPrimes_eq_subsingleton_self
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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

Tactic:
have h1 : ¬ I.IsPrime := by contrapose hI; simp [minimalPrimes_eq_subsingleton_self]
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
contrapose : ∀ (hI : I = ⊤), I.minimalPrimes.Finite
⊢ I ≠ ⊤

Tactic:
contrapose hI
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
I_1 : Ideal R
hI_1 : ¬I_1.minimalPrimes.Finite
I : Ideal R
hmax : ∀ (I_2 : Submodule R R), I < I_2 → (Ideal.minimalPrimes I_2).Finite
h1 : ¬I.IsPrime
hI : I = ⊤
⊢ I.minimalPrimes.Finite

Tactic:
simp [hI, minimalPrimes_top]

Premises used: Ideal.minimalPrimes_top
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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 ≠ ⊤

Tactic:
have h2 : I ≠ ⊤ := by contrapose hI; simp [hI, minimalPrimes_top]
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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 ≠ ⊤
obtain : ∀ (x : R) (hx : x ∉ I) (y : R) (hy : y ∉ I) (h : x * y ∈ I), False
⊢ False

Tactic:
obtain ⟨x, hx, y, hy, h⟩ := (not_isPrime_iff.mp h1).resolve_left h2

Premises used: Or.resolve_left, Ideal.not_isPrime_iff, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
rw : ∀ (hx : I < I ⊔ span {x}) (y : R) (hy : I < I ⊔ span {y}) (h : x * y ∈ I), False
⊢ False

Tactic:
rw [← Ideal.span_singleton_le_iff_mem, ← left_lt_sup] at hx hy

Premises used: left_lt_sup, Ideal.span_singleton_le_iff_mem
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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

Tactic:
hI (((hmax _ hx).union (hmax _ hy)).subset fun p ⟨⟨hp, hI⟩, hmin⟩ ↦ ?_)

Premises used: Set.Finite.union, Ideal.minimalPrimes, _private.0.Ideal.finite_minimalPrimes_of_isNoetherianRing.match_1, Membership.mem, Set.Finite.subset, Max.max, Ideal.span, Union.union, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
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
⊢ False

Tactic:
refine hI (((hmax _ hx).union (hmax _ hy)).subset fun p ⟨⟨hp, hI⟩, hmin⟩ ↦ ?_)

Premises used: Set.Finite.union, Ideal.minimalPrimes, _private.0.Ideal.finite_minimalPrimes_of_isNoetherianRing.match_1, Membership.mem, Set.Finite.subset, Max.max, Ideal.span, Union.union, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
inr : ∀ (hyp : y ∈ p), p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
rcases hp.2 (hI h) with hxp | hyp

Premises used: Ideal.IsPrime.mem_or_mem'
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
hxp : x ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
Or.inl ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hxp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hx.le.trans hq.2⟩ hqp⟩

Premises used: Iff.mpr, Set.union, Set.Mem, setOf, LT.lt.le, Ideal.span_singleton_le_iff_mem, And.right, And.left, And.intro, sup_le, Or.inl, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
hxp : x ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
exact Or.inl ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hxp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hx.le.trans hq.2⟩ hqp⟩

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
hyp : y ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
Or.inr ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hyp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hy.le.trans hq.2⟩ hqp⟩

Premises used: Iff.mpr, Set.union, Set.Mem, setOf, LT.lt.le, Ideal.span_singleton_le_iff_mem, And.right, And.left, And.intro, sup_le, LE.le.trans, Or.inr
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
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
hyp : y ∈ p
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes

Tactic:
exact Or.inr ⟨⟨hp, sup_le hI (p.span_singleton_le_iff_mem.mpr hyp)⟩,
      fun q hq hqp ↦ hmin ⟨hq.1, hy.le.trans hq.2⟩ hqp⟩

Premises used: Or.inr
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Goal:
R : Type u_1
inst : CommSemiring R
hR : IsNoetherianRing R
⊢ Set.Finite (α := Ideal R) (minimalPrimes R)

Tactic:
Ideal.finite_minimalPrimes_of_isNoetherianRing R ⊥

Premises used: setOf, Ideal.finite_minimalPrimes_of_isNoetherianRing, Bot.bot
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
a b : ℕ
hab : a + b = 1
⊢ a = 1 ∨ b = 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
a b : ℕ
hab : a + b = 1
⊢ a = 1 ∨ b = 1

Tactic:
have h : a = 1 ∨ b = 1 := by lia
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
a b : ℕ
hab : a + b = 1
h : a = 1 ∨ b = 1
f : a = 1 → IsUnit a
g : b = 1 → IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
apply h.imp

Premises used: Or.imp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
a b : ℕ
hab : a + b = 1
h : a = 1 ∨ b = 1
⊢ a = 1 → IsUnit a

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
a b : ℕ
hab : a + b = 1
h : a = 1 ∨ b = 1
⊢ b = 1 → IsUnit b

Tactic:
simp +contextual
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
n : ℕ
⊢ Membership.mem (γ := Ideal ℕ) (maximalIdeal ℕ) n ↔ n ≠ 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
h : ∀ (x : ℕ), x ∈ (↑(maximalIdeal ℕ) : Set ℕ) ↔ Membership.mem (γ := Set ℕ) {1}ᶜ x
⊢ (↑(maximalIdeal ℕ) : Set ℕ) = {1}ᶜ

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
x : ℕ
⊢ x ∈ (↑(maximalIdeal ℕ) : Set ℕ) ↔ Membership.mem (γ := Set ℕ) {1}ᶜ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ 2 ∈ (↑(maximalIdeal ℕ) : Set ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ 3 ∈ (↑(maximalIdeal ℕ) : Set ℕ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
refine :
  ∀ (n : ℕ) (h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n),
    Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
⊢ Eq (α := Ideal ℕ) (maximalIdeal ℕ) (span {2, 3})

Tactic:
refine le_antisymm (fun n h ↦ ?_) (span_le.mpr <| Set.pair_subset (by simp) (by simp))

Premises used: Ideal.span_le, Iff.mpr, Set.pair_subset, le_antisymm
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
inl : ∀ (lt : n < 1), Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
inr : ∀ (lt : 1 < n), Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n

Tactic:
obtain lt | lt := (mem_maximalIdeal_iff.mp h).lt_or_gt

Premises used: Nat.mem_maximalIdeal_iff, Iff.mp, Ne.lt_or_gt
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
lt : n < 1
inl :
  ∀ (h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0) (lt : LT.lt (α := ℕ) 0 1),
    Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) 0
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n

Tactic:
obtain rfl := lt_one_iff.mp lt

Premises used: Nat.lt_one_iff, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0
lt : LT.lt (α := ℕ) 0 1
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) 0

Tactic:
zero_mem _

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0
lt : LT.lt (α := ℕ) 0 1
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
lt : 1 < n
⊢ gcd 2 3 ∣ n

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
lt : 1 < n
⊢ 2 ≤ n

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
n : ℕ
h : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
lt : 1 < n
⊢ Membership.mem (γ := Submodule ℕ ℕ) (span {2, 3}) n

Tactic:
exact mem_span_pair.mpr <|
    exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le 2 3 n (by simp) (show 2 ≤ n by lia)

Premises used: Iff.mpr, Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le, Ideal.mem_span_pair, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : Set ℕ
rw : 1 ∉ (↑(span s) : Set ℕ) ↔ 1 ∉ s
⊢ Membership.mem (γ := Ideal ℕ) (span s) 1 ↔ 1 ∈ s

Tactic:
rw [← SetLike.mem_coe, ← not_iff_not]

Premises used: not_iff_not, SetLike.mem_coe
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : Set ℕ
simp_rw : {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ
⊢ 1 ∉ (↑(span s) : Set ℕ) ↔ 1 ∉ s

Tactic:
simp_rw [← Set.mem_compl_iff, ← Set.singleton_subset_iff, Set.subset_compl_comm]

Premises used: Set.singleton_subset_iff, Set.subset_compl_comm, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Ideal.NatInt
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 ℕ)
rw₃ rw₄ : s ⊆ (↑(maximalIdeal ℕ) : Set ℕ) ↔ s ⊆ (↑(maximalIdeal ℕ) : Set ℕ)
⊢ {1} ⊆ (↑(span s) : Set ℕ)ᶜ ↔ s ⊆ {1}ᶜ

Tactic:
rw [Set.subset_compl_comm, ← coe_maximalIdeal, SetLike.coe_subset_coe, span_le]

Premises used: Ideal.span_le, Set.subset_compl_comm, SetLike.coe_subset_coe, Nat.coe_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : Set ℕ
rw : Membership.mem (γ := AddSubmonoid ℕ) (Submodule.toAddSubmonoid (Submodule.span ℕ s)) 1 ↔ 1 ∈ s
⊢ Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure s) 1 ↔ 1 ∈ s

Tactic:
rw [← Submodule.span_nat_eq_addSubmonoidClosure]

Premises used: Submodule.span_nat_eq_addSubmonoidClosure
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : Set ℕ
⊢ Membership.mem (γ := AddSubmonoid ℕ) (Submodule.toAddSubmonoid (Submodule.span ℕ s)) 1 ↔ 1 ∈ s

Tactic:
one_mem_span_iff

Premises used: Set.Mem, setOf, Nat.one_mem_span_iff
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : Set ℕ
⊢ Membership.mem (γ := AddSubmonoid ℕ) (Submodule.toAddSubmonoid (Submodule.span ℕ s)) 1 ↔ 1 ∈ s

Tactic:
exact one_mem_span_iff

Premises used: Nat.one_mem_span_iff
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℕ
⊢ P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}

Tactic:
.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 ↦ ?_⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, LE.le.antisymm, Classical.or_iff_not_imp_left, IsLocalRing.le_maximalIdeal, Iff.intro, Ideal.IsPrime.ne_top, Iff.symm
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℕ
refine_1 : (P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) → P.IsPrime
refine_2 :
  ∀ (h : P.IsPrime) (h0 : ¬P = ⊥) (hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) (n : ℕ)
    (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n), n ∈ P
⊢ P.IsPrime ↔ P = ⊥ ∨ P = maximalIdeal ℕ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {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 ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ IsPrime (α := ℕ) ⊥

Tactic:
isPrime_bot

Premises used: Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ IsPrime (α := ℕ) ⊥

Tactic:
exact isPrime_bot

Premises used: Ideal.isPrime_bot
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ IsPrime (maximalIdeal ℕ)

Tactic:
(maximalIdeal.isMaximal ℕ).isPrime

Premises used: Ideal.IsMaximal.isPrime, IsLocalRing.maximalIdeal.isMaximal, Nat
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ IsPrime (maximalIdeal ℕ)

Tactic:
exact (maximalIdeal.isMaximal ℕ).isPrime

Premises used: Ideal.IsMaximal.isPrime, IsLocalRing.maximalIdeal.isMaximal, Nat
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
p : ℕ
hp : Nat.Prime p
⊢ p ≠ 0

Tactic:
simp [hp.ne_zero]

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
p : ℕ
hp : Nat.Prime p
refine_1 : Prime p
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : Nat.Prime p
⊢ IsPrime (α := ℕ) (span {p})

Tactic:
rwa [span_singleton_prime (by simp [hp.ne_zero]), ← Nat.prime_iff]

Premises used: Nat.prime_iff, Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ¬P = ⊥
hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}
n : ℕ
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n
refine_2 :
  ∀ (h0 : ∃ x ∈ P, x ∉ ⊥) (hsp : ¬∃ (p : ℕ), Nat.Prime p ∧ P = span {p}) (n : ℕ)
    (hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) n), n ∈ P
⊢ n ∈ P

Tactic:
rw [← le_bot_iff, SetLike.not_le_iff_exists] at h0

Premises used: le_bot_iff, SetLike.not_le_iff_exists
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
⊢ p ∈ P

Tactic:
have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
⊢ p ≠ 0

Tactic:
have ⟨(hp : p ∈ P), (hp0 : p ≠ 0)⟩ := Nat.find_spec h0
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
⊢ p ≠ 1

Tactic:
have : p ≠ 1 := ne_of_mem_of_not_mem hp P.one_notMem
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
⊢ 2 ≤ p

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
⊢ 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⟩)
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
⊢ ∀ (p : ℕ) (_ : Nat.Prime p), P ≠ span {p}

Tactic:
push Not at hsp

Premises used: Not
-- Module: Mathlib.RingTheory.Ideal.NatInt
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}
refine_2 : ∀ (q : ℕ) (hq : q ∈ P) (hqp : q ∉ span {p}), n ∈ 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)
-- Module: Mathlib.RingTheory.Ideal.NatInt
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
refine_2₁ : ∀ (hn1 : n ≠ 0), n ∈ P
⊢ n ∈ P

Tactic:
obtain rfl | hn1 := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
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}
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0
⊢ 0 ∈ P

Tactic:
Ideal.zero_mem _

Premises used: Set.Mem, Ideal.zero_mem
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℕ
h : P.IsPrime
h0 : ∃ x ∈ P, x ∉ ⊥
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}
hn : Membership.mem (γ := Submodule ℕ ℕ) (maximalIdeal ℕ) 0
⊢ 0 ∈ P

Tactic:
exact Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- Module: Mathlib.RingTheory.Ideal.NatInt
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 ≠ 1

Tactic:
have : n ≠ 1 := Nat.mem_maximalIdeal_iff.mp hn