awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ Module.supportDim R N > 0

Tactic:
have : Module.supportDim R N > 0 := by
      simp only [Module.supportDim, gt_iff_lt, Order.krullDim_pos_iff, Subtype.exists,
        Subtype.mk_lt_mk, exists_prop]
      use p
      simpa [hp] using ⟨_, IsLocalRing.closedPoint_mem_support R N, this⟩
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this_1 : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : Module.supportDim R N > 0
⊢ False

Tactic:
(ne_of_lt this) dim.symm

Premises used: Eq.symm, ne_of_lt
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
p : PrimeSpectrum R
hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R N) p
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this_1 : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : Module.supportDim R N > 0
⊢ False

Tactic:
exact (ne_of_lt this) dim.symm

Premises used: Eq.symm, ne_of_lt
-- Module: Mathlib.RingTheory.KrullDimension.Module
Goal:
R : Type u_1
inst : CommRing R
N : Type u_3
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsLocalRing R
dim : Module.supportDim R N = 0
h : Nontrivial N := ⋯
⊢ LE.le (α := Set (PrimeSpectrum R)) {{ asIdeal := maximalIdeal R, isPrime := ⋯ }} (Module.support R N)

Tactic:
simpa using IsLocalRing.closedPoint_mem_support R N

Premises used: IsLocalRing.closedPoint_mem_support
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw :
  Order.krullDim.{u_1} (PrimeSpectrum (R ⧸ I)) =
    Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
rw₁ rw₂ :
  Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1) =
    Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)
⊢ ringKrullDim.{u_1} (R ⧸ I) = Order.krullDim.{u_1} (↑(PrimeSpectrum.zeroLocus (↑I : Set R)) : Type u_1)

Tactic:
rw [ringKrullDim, Order.krullDim_eq_of_orderIso I.primeSpectrumQuotientOrderIsoZeroLocus]

Premises used: Ideal.primeSpectrumQuotientOrderIsoZeroLocus, Order.krullDim_eq_of_orderIso, ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
pos :
  ∀ (hr' : Eq (α := Ideal R) (Ideal.span {r}) ⊤),
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
neg :
  ∀ (hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤),
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R

Tactic:
by_cases hr' : Ideal.span {r} = ⊤

Premises used: Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq (α := Ideal R) (Ideal.span {r}) ⊤
pos : HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ ringKrullDim R
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R

Tactic:
rw [hr', ringKrullDim_eq_bot_of_subsingleton]

Premises used: ringKrullDim_eq_bot_of_subsingleton
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq (α := Ideal R) (Ideal.span {r}) ⊤
⊢ HAdd.hAdd (α := WithBot ℕ∞) ⊥ 1 ≤ ringKrullDim R

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
rwa : Set.Nonempty (α := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R))
rwa₁ : Ne (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) ∅
rwa₂ : ¬Eq (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) ∅
rwa₃ rwa₄ rwa₅ rwa₆ : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
⊢ Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)

Tactic:
rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]

Premises used: Set.nonempty_coe_sort, ne_eq, Set.nonempty_iff_ne_empty, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
⊢ Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)

Tactic:
have : Nonempty (PrimeSpectrum.zeroLocus (R := R) (Ideal.span {r})) := by
    rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty, ne_eq,
      PrimeSpectrum.zeroLocus_empty_iff_eq_top]
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
⊢ Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))

Tactic:
have := Ideal.Quotient.nontrivial_iff.mpr hr'
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
⊢ Nontrivial R

Tactic:
have := (Ideal.Quotient.mk (Ideal.span {r})).domain_nontrivial
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
neg :
  ∀ (i : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)),
    HAdd.hAdd (α := ℕ∞)
        (↑(i.length (r :=
              {x :
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
                match (motive :=
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                      (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                    Prop)
                  x with
                | (a, b) => a < b})) :
          ℕ∞)
        1 ≤
      ⨆ (p : LTSeries (PrimeSpectrum R)),
        (↑(p.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1 ≤ ringKrullDim R

Tactic:
rw [ringKrullDim_quotient, Order.krullDim_eq_iSup_length, ringKrullDim,
    Order.krullDim_eq_iSup_length, ← WithBot.coe_one, ← WithBot.coe_add,
    ENat.iSup_add, WithBot.coe_le_coe, iSup_le_iff]

Premises used: ringKrullDim_quotient, Order.krullDim_eq_iSup_length, WithBot.coe_le_coe, ENat.iSup_add, WithBot.coe_one, ringKrullDim, iSup_le_iff, WithBot.coe_add
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
neg :
  ∀ (p : Ideal R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p)
    (hp' :
      p ≤
        (↑(RelSeries.head (r :=
                {x :
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
                  match (motive :=
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                        (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                      Prop)
                    x with
                  | (a, b) => a < b})
                l) :
            PrimeSpectrum R).asIdeal),
    HAdd.hAdd (α := ℕ∞)
        (↑(l.length (r :=
              {x :
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
                match (motive :=
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                      (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                    Prop)
                  x with
                | (a, b) => a < b})) :
          ℕ∞)
        1 ≤
      ⨆ (p : LTSeries (PrimeSpectrum R)),
        (↑(p.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (PrimeSpectrum R)),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

Tactic:
obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le (J := l.head.1.asIdeal) bot_le

Premises used: Ideal.exists_minimalPrimes_le, bot_le
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
hp' :
  p ≤
    (↑(RelSeries.head (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})
            l) :
        PrimeSpectrum R).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
h :
  p' =
    (↑(RelSeries.head (r :=
          {x :
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
            match (motive :=
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                Prop)
              x with
            | (a, b) => a < b})
          l) :
      PrimeSpectrum R)
⊢ r ∈ p

Tactic:
simpa [← h] using l.head.2

Premises used: RelSeries.head, Subtype.property
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
hp' :
  p ≤
    (↑(RelSeries.head (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})
            l) :
        PrimeSpectrum R).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
⊢ p' <
    (↑(RelSeries.head (r :=
          {x :
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
            match (motive :=
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                Prop)
              x with
            | (a, b) => a < b})
          l) :
      PrimeSpectrum R)

Tactic:
have hp' : p' < l.head := lt_of_le_of_ne hp' fun h ↦ Set.disjoint_iff.mp
    (Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes hp)
    ⟨show r ∈ p by simpa [← h] using l.head.2, hr⟩
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
hp'_1 :
  p ≤
    (↑(RelSeries.head (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})
            l) :
        PrimeSpectrum R).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
hp' :
  p' <
    (↑(RelSeries.head (r :=
          {x :
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
            match (motive :=
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                Prop)
              x with
            | (a, b) => a < b})
          l) :
      PrimeSpectrum R)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (PrimeSpectrum R)),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)

Tactic:
le_trans ?_ (le_iSup _ ((l.map Subtype.val (fun _ _ ↦ id)).cons p' hp'))

Premises used: le_iSup, id, RelSeries.cons, LTSeries.map, Subtype.val, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
hp'_1 :
  p ≤
    (↑(RelSeries.head (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})
            l) :
        PrimeSpectrum R).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
hp' :
  p' <
    (↑(RelSeries.head (r :=
          {x :
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
            match (motive :=
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                Prop)
              x with
            | (a, b) => a < b})
          l) :
      PrimeSpectrum R)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    (↑(RelSeries.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          (RelSeries.cons (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            (l.map
              (Subtype.val (p := fun (x : PrimeSpectrum R) ↦
                Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) x))
              ⋯)
            p' hp')) :
      ℕ∞)

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ ringKrullDim S + 1 ≤ ringKrullDim R

Tactic:
le_trans ?_ (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr)

Premises used: ringKrullDim_quotient_succ_le_of_nonZeroDivisor, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
refine : ringKrullDim S + 1 ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1
⊢ ringKrullDim S + 1 ≤ ringKrullDim R

Tactic:
refine le_trans ?_ (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr)

Premises used: ringKrullDim_quotient_succ_le_of_nonZeroDivisor, le_trans
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
bc : ringKrullDim S ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
⊢ ringKrullDim S + 1 ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r})) + 1

Tactic:
gcongr
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ ringKrullDim S ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))

Tactic:
ringKrullDim_le_of_surjective (Ideal.Quotient.lift _ f (RingHom.ker f
    |>.span_singleton_le_iff_mem.mpr hr')) (Ideal.Quotient.lift_surjective_of_surjective _ _ hf)

Premises used: Iff.mpr, Ideal.Quotient.lift_surjective_of_surjective, Ideal.span_singleton_le_iff_mem, Ideal.Quotient.lift, ringKrullDim_le_of_surjective, RingHom.ker
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ ringKrullDim S ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))

Tactic:
exact ringKrullDim_le_of_surjective (Ideal.Quotient.lift _ f (RingHom.ker f
    |>.span_singleton_le_iff_mem.mpr hr')) (Ideal.Quotient.lift_surjective_of_surjective _ _ hf)

Premises used: Iff.mpr, Ideal.Quotient.lift_surjective_of_surjective, Ideal.span_singleton_le_iff_mem, Ideal.Quotient.lift, ringKrullDim_le_of_surjective, RingHom.ker
-- Module: Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Goal:
R : Type u_1
inst : CommRing R
⊢ ringKrullDim R + 1 ≤ ringKrullDim.{u_1} R[X]

Tactic:
ringKrullDim_succ_le_of_surjective constantCoeff (⟨C ·, coeff_C_zero⟩)
    X_mem_nonzeroDivisors coeff_X_zero

Premises used: Polynomial.C, ringKrullDim_succ_le_of_surjective, Polynomial.coeff_X_zero, Polynomial.constantCoeff, Polynomial.X_mem_nonzeroDivisors, Exists.intro, Polynomial.coeff_C_zero, DFunLike.coe