awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
x : R
reg : IsSMulRegular M x
hx : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 = supportDim R M

Tactic:
supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson
    (fun _ ↦ reg.notMem_of_mem_minimalPrimes) hx

Premises used: IsSMulRegular.notMem_of_mem_minimalPrimes, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
rw : supportDim R (R ⧸ HSMul.hSMul (β := Submodule R R) x ⊤) + 1 = supportDim R R
⊢ ringKrullDim.{u_1} (QuotSMulTop x R) + 1 = ringKrullDim R

Tactic:
rw [← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]

Premises used: Module.supportDim_self_eq_ringKrullDim, Module.supportDim_quotient_eq_ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ supportDim R (R ⧸ HSMul.hSMul (β := Submodule R R) x ⊤) + 1 = supportDim R R

Tactic:
supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson reg
    ((annihilator R R).ringJacobson_le_jacobson hx)

Premises used: Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Ideal.ringJacobson_le_jacobson
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ supportDim R (R ⧸ HSMul.hSMul (β := Submodule R R) x ⊤) + 1 = supportDim R R

Tactic:
exact supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson reg
    ((annihilator R R).ringJacobson_le_jacobson hx)

Premises used: Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Ideal.ringJacobson_le_jacobson
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ span {x} = HSMul.hSMul (β := Ideal R) x ⊤

Tactic:
simp [← Submodule.ideal_span_singleton_smul]

Premises used: Submodule.ideal_span_singleton_smul
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ span {x} = HSMul.hSMul (β := Ideal R) x ⊤

Tactic:
have h : span {x} = x • (⊤ : Ideal R) := by simp [← Submodule.ideal_span_singleton_smul]
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
rw₁ rw₂ : ringKrullDim R = ringKrullDim R
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x})) + 1 = ringKrullDim R

Tactic:
rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R h).toRingEquiv,
    ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson reg hx]

Premises used: Ideal.quotientEquivAlgOfEq, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, ringKrullDim_eq_of_ringEquiv, AlgEquiv.toRingEquiv
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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

Tactic:
le_antisymm (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr) (h ▸ ?_)

Premises used: Eq.rec, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
refine : (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1 = ringKrullDim R

Tactic:
refine le_antisymm (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hr) (h ▸ ?_)

Premises used: Eq.rec, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, le_antisymm
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1

Tactic:
Ideal.height_le_ringKrullDim_quotient_add_one hp

Premises used: Ideal.height_le_ringKrullDim_quotient_add_one
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ (↑p.height : WithBot ℕ∞) ≤ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {r})) + 1

Tactic:
exact Ideal.height_le_ringKrullDim_quotient_add_one hp

Premises used: Ideal.height_le_ringKrullDim_quotient_add_one
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
x : R
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ supportDim R M ≤ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson ((maximalIdeal_le_jacobson _) hx)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
rw : supportDim R R ≤ supportDim R (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1

Tactic:
rw [← Module.supportDim_self_eq_ringKrullDim, ← Module.supportDim_quotient_eq_ringKrullDim]

Premises used: Module.supportDim_self_eq_ringKrullDim, Module.supportDim_quotient_eq_ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ supportDim R R ≤ supportDim R (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1

Tactic:
supportDim_le_supportDim_quotSMulTop_succ hx

Premises used: Module.supportDim_le_supportDim_quotSMulTop_succ
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
⊢ supportDim R R ≤ supportDim R (R ⧸ HSMul.hSMul (β := Ideal R) x ⊤) + 1

Tactic:
exact supportDim_le_supportDim_quotSMulTop_succ hx

Premises used: Module.supportDim_le_supportDim_quotSMulTop_succ
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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)
hs : (↑S : Set R) ⊆ (↑(Ring.jacobson R) : Set R)
⊢ ringKrullDim R ≤
    ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span (↑S : Set R))) + (↑S.card : WithBot ℕ∞)

Tactic:
apply ringKrullDim_le_ringKrullDim_quotient_add_card

Premises used: ringKrullDim_le_ringKrullDim_quotient_add_card
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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)
hs hs₁ hs₂ hs₃ : (↑S : Set R) ⊆ (↑(maximalIdeal R : Ideal R) : Set R)
⊢ (↑S : Set R) ⊆ (↑(Ring.jacobson R) : Set R)

Tactic:
rwa [IsLocalRing.ringJacobson_eq_maximalIdeal]

Premises used: IsLocalRing.ringJacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
h₁ : I ≤ Ring.jacobson R
⊢ ringKrullDim R ≤ ringKrullDim.{u_1} (R ⧸ I) + (↑(Submodule.spanFinrank I) : WithBot ℕ∞)

Tactic:
apply ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank

Premises used: ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
h₁ : I ≤ maximalIdeal R
⊢ I ≤ Ring.jacobson R

Tactic:
rw [IsLocalRing.ringJacobson_eq_maximalIdeal]

Premises used: IsLocalRing.ringJacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ I ≤ maximalIdeal R

Tactic:
le_maximalIdeal h

Premises used: IsLocalRing.le_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ I ≤ maximalIdeal R

Tactic:
exact le_maximalIdeal h

Premises used: IsLocalRing.le_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 = supportDim R M

Tactic:
supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson hn <|
    (maximalIdeal_le_jacobson _) hx

Premises used: IsLocalRing.maximalIdeal_le_jacobson, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
x : R
reg : IsSMulRegular M x
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 = supportDim R M

Tactic:
supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson reg ((maximalIdeal_le_jacobson _) hx)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ Membership.mem (γ := Ideal R) (Ring.jacobson R) x

Tactic:
simpa [ringJacobson_eq_maximalIdeal R]

Premises used: IsLocalRing.ringJacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Ideal R) (maximalIdeal R : Ideal R) x
⊢ Membership.mem (γ := Ideal R) (Ring.jacobson R) x

Tactic:
rwa [ringJacobson_eq_maximalIdeal R]

Premises used: IsLocalRing.ringJacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
x : R
reg : Membership.mem (γ := Submonoid R) R⁰ x
hx : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (span {x})) + 1 = ringKrullDim R

Tactic:
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim
    (Module.Flat.isSMulRegular_of_nonZeroDivisors reg) hx

Premises used: ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, Module.Flat.isSMulRegular_of_nonZeroDivisors
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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 []
nil :
  supportDim.{u_1, u_2} R (HasQuotient.Quotient M (B := Submodule R M) ⊥) +
      (↑(List.length.{u_1} (α := R) []) : WithBot ℕ∞) =
    supportDim 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:
rw [ofList_nil, Submodule.bot_smul]

Premises used: Submodule.bot_smul, Ideal.ofList_nil
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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 (HasQuotient.Quotient M (B := Submodule R M) ⊥) +
      (↑(List.length.{u_1} (α := R) []) : WithBot ℕ∞) =
    supportDim R M

Tactic:
simpa using supportDim_eq_of_equiv (Submodule.quotEquivOfEqBot ⊥ rfl)

Premises used: Submodule.quotEquivOfEqBot, Bot.bot, Module.supportDim_eq_of_equiv, rfl
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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')
isu : IsUnit x
⊢ ⊤ = HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList (x :: rs')) ⊤

Tactic:
simp [span_singleton_eq_top.mpr isu]

Premises used: Iff.mpr, Ideal.span_singleton_eq_top
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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')
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
simpa using fun isu ↦ reg.2 (by simp [span_singleton_eq_top.mpr isu])

Premises used: RingTheory.Sequence.IsRegular.top_ne_smul
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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')
⊢ 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])
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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')
mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList (x :: rs')) ⊤) +
      (↑(x :: rs').length : WithBot ℕ∞) =
    supportDim R M

Tactic:
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]

Premises used: RingTheory.Sequence.isRegular_cons_iff, add_assoc, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner, Module.supportDim_quotSMulTop_succ_eq_supportDim, And.right, And.left, Iff.mp, Module.supportDim_eq_of_equiv
-- Module: Mathlib.RingTheory.KrullDimension.Regular
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
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
cons :
  ∀ (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_6 : AddCommGroup M] [inst_7 : Module R M] [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
⊢ supportDim.{u_1, u_2} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (ofList rs) ⊤) +
      (↑rs.length : 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]

Premises used: add_assoc, Submodule.bot_smul, Submodule.quotEquivOfEqBot, Bot.bot, Ideal.ofList_nil, Module.supportDim_eq_of_equiv, rfl
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤

Tactic:
have eq : ofList rs = ofList rs • (⊤ : Ideal R) := by simp
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
eq : ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤
rw :
  supportDim R (R ⧸ HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤) + (↑rs.length : WithBot ℕ∞) =
    supportDim R R
⊢ ringKrullDim.{u_1} (HasQuotient.Quotient R (B := Ideal R) (ofList rs)) + (↑rs.length : WithBot ℕ∞) = ringKrullDim R

Tactic:
rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R eq).toRingEquiv,
    ← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]

Premises used: Ideal.quotientEquivAlgOfEq, ringKrullDim_eq_of_ringEquiv, Module.supportDim_self_eq_ringKrullDim, AlgEquiv.toRingEquiv, Module.supportDim_quotient_eq_ringKrullDim
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
eq : ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤
⊢ supportDim R (R ⧸ HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤) + (↑rs.length : WithBot ℕ∞) =
    supportDim R R

Tactic:
supportDim_add_length_eq_supportDim_of_isRegular rs reg

Premises used: Module.supportDim_add_length_eq_supportDim_of_isRegular, Set.Mem
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
eq : ofList rs = HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤
⊢ supportDim R (R ⧸ HSMul.hSMul (α := Ideal R) (β := Ideal R) (ofList rs) ⊤) + (↑rs.length : WithBot ℕ∞) =
    supportDim R R

Tactic:
exact supportDim_add_length_eq_supportDim_of_isRegular rs reg

Premises used: Module.supportDim_add_length_eq_supportDim_of_isRegular
-- Module: Mathlib.RingTheory.KrullDimension.Zero
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
I J : Ideal R
⊢ I ∈ J.minimalPrimes ↔ I.IsPrime ∧ J ≤ I

Tactic:
⟨fun H ↦ H.1, fun H ↦ ⟨H, fun _ h e ↦ (h.1.isMaximal'.eq_of_le H.1.ne_top e).ge⟩⟩

Premises used: Eq.ge, And.left, Ideal.IsMaximal.eq_of_le, And.intro, Iff.intro, Ideal.IsPrime.ne_top, Ideal.IsPrime.isMaximal'
-- Module: Mathlib.RingTheory.KrullDimension.Zero
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
I J : Ideal R
inst_2 : I.IsPrime
rwa : I.IsPrime ∧ J ≤ I ↔ J ≤ I
rwa₁ : J ≤ I ↔ J ≤ I
rwa₂ : I.IsPrime
rwa₃ : J ≤ I ↔ J ≤ I
rwa₄ rwa₅ rwa₆ : I.IsPrime
⊢ I ∈ J.minimalPrimes ↔ J ≤ I

Tactic:
rwa [mem_minimalPrimes_iff, and_iff_right]

Premises used: and_iff_right, Ring.KrullDimLE.mem_minimalPrimes_iff
-- Module: Mathlib.RingTheory.KrullDimension.Zero
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
h :
  ∀ (x : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x ↔
      Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsPrime} x
⊢ Eq (α := Set (Ideal R)) (minimalPrimes R) {I : Ideal R | I.IsPrime}

Tactic:
ext
-- Module: Mathlib.RingTheory.KrullDimension.Zero
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
x : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x ↔
    Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsPrime} x

Tactic:
Ideal.mem_minimalPrimes_iff_isPrime

Premises used: Set.Mem, setOf, Ideal.mem_minimalPrimes_iff_isPrime
-- Module: Mathlib.RingTheory.KrullDimension.Zero
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
x : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x ↔
    Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsPrime} x

Tactic:
exact Ideal.mem_minimalPrimes_iff_isPrime

Premises used: Ideal.mem_minimalPrimes_iff_isPrime
-- Module: Mathlib.RingTheory.KrullDimension.Zero
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : KrullDimLE 0 R
h :
  ∀ (x : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x ↔
      Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} x
⊢ Eq (α := Set (Ideal R)) (minimalPrimes R) {I : Ideal R | I.IsMaximal}

Tactic:
ext