awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
⊢ LE.le (α := ℕ∞)
    ((fun (x1 x2 : ℕ∞) ↦ x1 + x2)
      (⨆ (p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
        (↑(p.length (r :=
              {x_1 :
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                x_1.1 < x_1.2})) :
          ℕ∞))
      1)
    (⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞))
have simp : ∀ (i : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
  HAdd.hAdd (α := ℕ∞)
      (↑(i.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
Tactic: simp only [ENat.iSup_add, iSup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
have hp : Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M))
  (↑(RelSeries.head (r :=
        {x_1 :
          (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
            (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
          match (motive :=
            (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) →
              Prop)
            x_1 with
          | (a, b) => a < b})
        p) :
    PrimeSpectrum R)
Tactic: have hp := p.head.2
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M))
    (↑(RelSeries.head (r :=
          {x_1 :
            (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
            match (motive :=
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) →
                Prop)
              x_1 with
            | (a, b) => a < b})
          p) :
      PrimeSpectrum R)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
have hp₁ : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
    (↑(RelSeries.head (r :=
          {x_1 :
            (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
            x_1.1 < x_1.2})
          p) :
      PrimeSpectrum R) ∧
  x ∈
    (↑(↑(RelSeries.head (r :=
                {x_1 :
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                  x_1.1 < x_1.2})
                p) :
            PrimeSpectrum R).asIdeal :
      Set R)
Tactic: simp only [support_quotSMulTop, Set.mem_inter_iff, mem_zeroLocus, Set.singleton_subset_iff] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (r :=
                  {x_1 :
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                    x_1.1 < x_1.2})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
have le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
Tactic: have le : support R (QuotSMulTop x M) ⊆ support R M := by simp
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (r :=
                  {x_1 :
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                    x_1.1 < x_1.2})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
have obtain : ∀ (r : Ideal R) (hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r)
  (hr :
    r ≤
      (↑(RelSeries.head (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b})
              q) :
          PrimeSpectrum R).asIdeal),
  HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
Tactic: obtain ⟨r, hrm, hr⟩ := exists_minimalPrimes_le (mem_support_iff_of_finite.mp q.head.2)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h_1 : Nontrivial M
h_2 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (r :=
                  {x_1 :
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                    x_1.1 < x_1.2})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
r_1 : Ideal R
hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r_1
hr :
  r_1 ≤
    (↑(RelSeries.head (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal
r : (↑(support R M) : Type u_1) :=
  Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
    { asIdeal := r_1, isPrime := ⋯ } ⋯
h :
  r =
    RelSeries.head (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b})
      q
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M))
    (↑(RelSeries.head (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal
have rwa : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) (↑r : PrimeSpectrum R).asIdeal
Tactic: rwa [← h]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (r :=
                  {x_1 :
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                    x_1.1 < x_1.2})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
r_1 : Ideal R
hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r_1
hr :
  r_1 ≤
    (↑(RelSeries.head (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal
r : (↑(support R M) : Type u_1) :=
  Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
    { asIdeal := r_1, isPrime := ⋯ } ⋯
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (↑(support R M) : Type u_1)),
      (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)
have hr₁ : r <
  RelSeries.head (r :=
    {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
      match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
      | (a, b) => a < b})
    q
Tactic: have hr : r < q.head := lt_of_le_of_ne hr (fun h ↦ hn q.head.1.1 (by rwa [← h]) hp.2)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : Membership.mem (γ := Ideal R) (Ring.jacobson R) x
⊢ ringKrullDim.{u_1} (QuotSMulTop x R) + 1 = ringKrullDim R
have rw : supportDim R (R ⧸ HSMul.hSMul (β := Submodule R R) x ⊤) + 1 = supportDim R R
Tactic: rw [← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : Membership.mem (γ := Ideal R) (Ring.jacobson R) x
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x})) + 1 = ringKrullDim R
have h : span {x} = HSMul.hSMul (β := Ideal R) x ⊤
Tactic: have h : span {x} = x • (⊤ : Ideal R) := by simp [← Submodule.ideal_span_singleton_smul]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : Membership.mem (γ := Ideal R) (Ring.jacobson R) x
h : span {x} = HSMul.hSMul (β := Ideal R) x ⊤
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x})) + 1 = ringKrullDim R
have rw : ringKrullDim.{u_1} (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1 = ringKrullDim R
Tactic: rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R h).toRingEquiv,
    ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson reg hx]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : Membership.mem (γ := Ideal R) (Ring.jacobson R) x
h : span {x} = HSMul.hSMul (β := Ideal R) x ⊤
rw : ringKrullDim.{u_1} (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1 = ringKrullDim R
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x})) + 1 = ringKrullDim R
have rw₁ : ringKrullDim R = ringKrullDim R
Tactic: rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R h).toRingEquiv,
    ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson reg hx]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) r
p : Ideal R
inst_2 : p.IsPrime
h : (↑p.height : WithBot ℕ∞) = ringKrullDim R
hp : r ∈ p
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1 = ringKrullDim R
have refine : (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1
Tactic: refine le_antisymm (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr) (h ▸ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
x : R
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1
have rw : supportDim R R ≤ supportDim R (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1
Tactic: rw [← Module.supportDim_self_eq_ringKrullDim, ← Module.supportDim_quotient_eq_ringKrullDim]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
S : Finset R
hS : (↑S : Set R) ⊆ (↑(maximalIdeal R) : Set R)
⊢ ringKrullDim R ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span (↑S : Set R))) + (↑S.card : WithBot ℕ∞)
have hs : (↑S : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
Tactic: apply ringKrullDim_le_ringKrullDim_quotient_add_card
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)
have h₁ : I ≤ Ring.jacobson R
Tactic: apply ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ I ≤ Ring.jacobson R
have h₁ : I ≤ maximalIdeal R
Tactic: rw [IsLocalRing.ringJacobson_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module.Finite R M
reg : Sequence.IsRegular.{u_1, u_2} (R := R) M []
⊢ supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal R) (β := Submodule R M) (ofList []) ⊤) +
      (↑(List.length.{u_1} (α := R) []) : WithBot ℕ∞) =
    supportDim R M
have nil : supportDim.{u_1, u_2} R (HasQuotient.Quotient M (B := Submodule R M) ⊥) +
    (↑(List.length.{u_1} (α := R) []) : WithBot ℕ∞) =
  supportDim R M
Tactic: rw [ofList_nil, Submodule.bot_smul]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst_6 : AddCommGroup M] [inst_7 : Module R M] [Module.Finite R M] (reg : Sequence.IsRegular M rs'),
    supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList rs') ⊤) +
        (↑rs'.length : WithBot ℕ∞) =
      supportDim R M
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
⊢ supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList (x :: rs')) ⊤) +
      (↑(x :: rs').length : WithBot ℕ∞) =
    supportDim R M
have mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x
Tactic: have mem : x ∈ maximalIdeal R := by
      simpa using fun isu ↦ reg.2 (by simp [span_singleton_eq_top.mpr isu])
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular M rs
⊢ supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList rs) ⊤) +
      (↑rs.length : WithBot ℕ∞) =
    supportDim R M
have nil : ∀ {M : Type u_2} [inst_6 : AddCommGroup M] [inst_7 : Module R M] [Module.Finite R M]
  (reg : Sequence.IsRegular.{u_1, u_2} (R := R) M []),
  supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul.{u_1, u_2, u_2} (α := Ideal R) (β := Submodule R M) (ofList []) ⊤) +
      (↑(List.length.{u_1} (α := R) []) : WithBot ℕ∞) =
    supportDim R M
Tactic: induction rs generalizing M with
  | nil =>
    rw [ofList_nil, Submodule.bot_smul]
    simpa using supportDim_eq_of_equiv (Submodule.quotEquivOfEqBot ⊥ rfl)
  | cons x rs' ih =>
    have mem : x ∈ maximalIdeal R := by
      simpa using fun isu ↦ reg.2 (by simp [span_singleton_eq_top.mpr isu])
    simp [supportDim_eq_of_equiv (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x _),
      ← supportDim_quotSMulTop_succ_eq_supportDim ((isRegular_cons_iff M _ _).mp reg).1 mem,
      ← ih ((isRegular_cons_iff M _ _).mp reg).2, ← add_assoc]
Cleared hypotheses: M, inst_2, inst_3, inst_4, rs, reg