awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
⊢ p.gcd q ∣ n ^ (p.pred * q.pred)

Tactic:
simp [prime.coprime_iff_not_dvd.mpr (Ideal.mem_span_singleton.not.mp hqp)]

Premises used: Iff.mpr, Iff.not, Iff.mp, Ideal.mem_span_singleton, Nat.Prime.coprime_iff_not_dvd
-- 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_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
⊢ 1 < n

Tactic:
lia
-- 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_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
refine_2 : ∀ (a b : ℕ) (eq : a * p + b * q = n ^ (p.pred * q.pred)), n ∈ P
⊢ 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
-- 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_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
a b : ℕ
eq : a * p + b * q = n ^ (p.pred * q.pred)
⊢ n ∈ P

Tactic:
h.mem_of_pow_mem _ (eq ▸ add_mem (P.mul_mem_left _ hp) (P.mul_mem_left _ hq))

Premises used: Set.Mem, Ideal.IsPrime.mem_of_pow_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_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
a b : ℕ
eq : a * p + b * q = n ^ (p.pred * q.pred)
⊢ n ∈ P

Tactic:
exact h.mem_of_pow_mem _ (eq ▸ add_mem (P.mul_mem_left _ hp) (P.mul_mem_left _ hq))

Premises used: Ideal.IsPrime.mem_of_pow_mem
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
I : Ideal ℤ
⊢ map (F := ℕ →+* ℤ) (Nat.castRingHom ℤ) (comap (F := ℕ →+* ℤ) (Nat.castRingHom ℤ) I) = I

Tactic:
map_comap_le.antisymm fun n hn ↦ n.sign_mul_natAbs ▸ mul_mem_left _ _ <| mem_map_of_mem _
    (mem_comap.mpr <| show (n.natAbs : ℤ) ∈ I from n.sign_mul_self ▸ mul_mem_left _ _ hn)

Premises used: LE.le.antisymm, Ideal.map_comap_le
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
P : Ideal ℤ
⊢ P.IsPrime ↔ P = ⊥ ∨ ∃ (p : ℕ), Nat.Prime p ∧ P = span {(↑p : ℤ)}

Tactic:
isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors.trans <| or_congr_right
  ⟨fun ⟨p, hp, eq⟩ ↦ ⟨_, Int.prime_iff_natAbs_prime.mp hp, eq.trans
    p.span_natAbs.symm⟩, fun ⟨_p, hp, eq⟩ ↦ ⟨_, Nat.prime_iff_prime_int.mp hp, eq⟩⟩

Premises used: Nat.Prime, Nat.prime_iff_prime_int, Prime, Int.span_natAbs, Exists, Nat.cast, _private.0.Ideal.isPrime_int_iff.match_1, And, or_congr_right, Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors, _private.0.Ideal.isPrime_int_iff.match_2, And.intro, Iff.intro, Int.natAbs, Exists.intro, Iff.mp, Iff.trans, Ideal.span, Int.prime_iff_natAbs_prime, Singleton.singleton, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
⊢ ringKrullDim ℕ = 2

Tactic:
le_antisymm (iSup_le fun s ↦ le_of_not_gt fun hs ↦ ?_) ?_

Premises used: le_of_not_gt, le_antisymm, iSup_le
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
refine_1 :
  ∀ (s : LTSeries (PrimeSpectrum ℕ))
    (hs :
      LT.lt (α := WithBot ℕ∞) 2
        (↑(s.length (r :=
              {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
                match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
                | (a, b) => a < b})) :
          WithBot ℕ∞)),
    False
refine_2 : 2 ≤ ringKrullDim ℕ
⊢ ringKrullDim ℕ = 2

Tactic:
refine le_antisymm (iSup_le fun s ↦ le_of_not_gt fun hs ↦ ?_) ?_

Premises used: le_antisymm, iSup_le
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : LTSeries (PrimeSpectrum ℕ)
hs :
  LT.lt (α := WithBot ℕ∞) 2
    (↑(s.length (r :=
          {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
            match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞)
⊢ 2 <
    s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})

Tactic:
replace hs : 2 < s.length := ENat.coe_lt_coe.mp (WithBot.coe_lt_coe.mp hs)
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
⊢ 3 <
    s.length (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b}) +
      1

Tactic:
lia
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
⊢ NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))

Tactic:
have : NeZero s.length := ⟨three_ne_zero⟩
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
⊢ ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal

Tactic:
have h1 : ⊥ < (s 1).asIdeal := bot_le.trans_lt (s.step 0)
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
refine_1 :
  ∀
    (hmax :
      (s.toFun (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b})
            1).asIdeal =
        maximalIdeal ℕ),
    False
refine_1₁ :
  ∀ (p : ℕ) (hp : Nat.Prime p)
    (hsp :
      (s.toFun (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b})
            1).asIdeal =
        span {p}),
    False
⊢ False

Tactic:
obtain hmax | ⟨p, hp, hsp⟩ := (Ideal.isPrime_nat_iff.mp (s 1).2).resolve_left h1.ne'

Premises used: PrimeSpectrum.isPrime, Or.resolve_left, LT.lt.ne', Ideal.isPrime_nat_iff, Iff.mp, RelSeries.toFun, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
hmax :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    maximalIdeal ℕ
⊢ False

Tactic:
(le_maximalIdeal_of_isPrime (s 2).asIdeal).not_gt (hmax.symm.trans_lt (s.step 1))

Premises used: LE.le.not_gt, Eq.trans_lt, RelSeries.toFun, RelSeries.step, IsLocalRing.le_maximalIdeal_of_isPrime, OfNat.ofNat, Eq.symm, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
hmax :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    maximalIdeal ℕ
⊢ False

Tactic:
exact (le_maximalIdeal_of_isPrime (s 2).asIdeal).not_gt (hmax.symm.trans_lt (s.step 1))

Premises used: LE.le.not_gt, Eq.trans_lt, RelSeries.toFun, RelSeries.step, IsLocalRing.le_maximalIdeal_of_isPrime, OfNat.ofNat, Eq.symm, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    span {p}
refine_1 :
  ∀
    (hmax :
      (s.toFun (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b})
            2).asIdeal =
        maximalIdeal ℕ),
    False
refine_1₁ :
  ∀ (q : ℕ) (hq : Nat.Prime q)
    (hsq :
      (s.toFun (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b})
            2).asIdeal =
        span {q}),
    False
⊢ False

Tactic:
obtain hmax | ⟨q, hq, hsq⟩ :=
      (Ideal.isPrime_nat_iff.mp (s 2).2).resolve_left (h1.trans (s.step 1)).ne'

Premises used: PrimeSpectrum.isPrime, Or.resolve_left, LT.lt.ne', Ideal.isPrime_nat_iff, Iff.mp, LT.lt.trans, RelSeries.toFun, RelSeries.step, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    span {p}
hmax :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        2).asIdeal =
    maximalIdeal ℕ
⊢ False

Tactic:
(le_maximalIdeal_of_isPrime (s 3).asIdeal).not_gt (hmax.symm.trans_lt (s.step 2))

Premises used: LE.le.not_gt, Eq.trans_lt, RelSeries.toFun, RelSeries.step, IsLocalRing.le_maximalIdeal_of_isPrime, OfNat.ofNat, Eq.symm, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    span {p}
hmax :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        2).asIdeal =
    maximalIdeal ℕ
⊢ False

Tactic:
exact (le_maximalIdeal_of_isPrime (s 3).asIdeal).not_gt (hmax.symm.trans_lt (s.step 2))

Premises used: LE.le.not_gt, Eq.trans_lt, RelSeries.toFun, RelSeries.step, IsLocalRing.le_maximalIdeal_of_isPrime, OfNat.ofNat, Eq.symm, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    span {p}
q : ℕ
hq : Nat.Prime q
hsq :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        2).asIdeal =
    span {q}
⊢ False

Tactic:
hq.not_isUnit <| (Ideal.span_singleton_lt_span_singleton.mp
        ((hsp.symm.trans_lt (s.step 1)).trans_eq hsq)).isUnit_of_irreducible_right hp

Premises used: Irreducible.not_isUnit, LT.lt.trans_eq, DvdNotUnit.isUnit_of_irreducible_right, Eq.trans_lt, Iff.mp, Ideal.span_singleton_lt_span_singleton, RelSeries.step, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.NatInt
Goal:
s_1 : LTSeries (PrimeSpectrum ℕ)
hs :
  2 <
    s_1.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b})
s : RelSeries (α := PrimeSpectrum ℕ)
  {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
    match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
    | (a, b) => a < b} :=
  RelSeries.take (r :=
    {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
      match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
      | (a, b) => a < b})
    s_1
    (⟨3, ⋯⟩ :
      Fin
        (s_1.length (r :=
            {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
              match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
              | (a, b) => a < b}) +
          1))
this :
  NeZero
    (s.length (r :=
      {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
        match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
        | (a, b) => a < b}))
h1 :
  ⊥ <
    (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        1).asIdeal =
    span {p}
q : ℕ
hq : Nat.Prime q
hsq :
  (s.toFun (r :=
        {x : PrimeSpectrum ℕ × PrimeSpectrum ℕ |
          match (motive := PrimeSpectrum ℕ × PrimeSpectrum ℕ → Prop) x with
          | (a, b) => a < b})
        2).asIdeal =
    span {q}
⊢ False

Tactic:
exact hq.not_isUnit <| (Ideal.span_singleton_lt_span_singleton.mp
        ((hsp.symm.trans_lt (s.step 1)).trans_eq hsq)).isUnit_of_irreducible_right hp

Premises used: Irreducible.not_isUnit, LT.lt.trans_eq, DvdNotUnit.isUnit_of_irreducible_right, Eq.trans_lt, Iff.mp, Ideal.span_singleton_lt_span_singleton, RelSeries.step, OfNat.ofNat, Eq.symm