awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
L : ModuleCat.{v, u} R
this : ∀ (m : ℕ), Subsingleton.{v + 1} (Ext S.X₂ L (m + 1))
isi : IsIso (X := AddCommGrpCat.of (Ext S.X₁ L (n + 1))) (AddCommGrpCat.ofHom (Ext.precomp hS.extClass L ⋯))
⊢ Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))

Tactic:
(asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr

Premises used: CategoryTheory.Localization.SmallHom, CategoryTheory.Abelian.Ext.precomp, Equiv.subsingleton_congr, add_comm, CategoryTheory.Abelian.Ext, CategoryTheory.Localization.SmallShiftedHom, CategoryTheory.Iso.addCommGroupIsoToAddEquiv, AddCommGrpCat.ofHom, AddEquiv.toEquiv, OfNat.ofNat, CategoryTheory.asIso, CategoryTheory.ShortComplex.ShortExact.extClass
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
L : ModuleCat.{v, u} R
this : ∀ (m : ℕ), Subsingleton.{v + 1} (Ext S.X₂ L (m + 1))
isi : IsIso (X := AddCommGrpCat.of (Ext S.X₁ L (n + 1))) (AddCommGrpCat.ofHom (Ext.precomp hS.extClass L ⋯))
⊢ Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))

Tactic:
exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr

Premises used: CategoryTheory.Abelian.Ext.precomp, Equiv.subsingleton_congr, add_comm, CategoryTheory.Iso.addCommGroupIsoToAddEquiv, AddCommGrpCat.ofHom, AddEquiv.toEquiv, OfNat.ofNat, CategoryTheory.asIso, CategoryTheory.ShortComplex.ShortExact.extClass
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
⊢ ∀ (L : ModuleCat.{v, u} R), Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))

Tactic:
have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat.{v, u} R), Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))
apply : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext S.X₁ L (n + 1))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)

Tactic:
apply hn S.X₁

Premises used: CategoryTheory.ShortComplex.X₁
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
this : ∀ (L : ModuleCat.{v, u} R), Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))
⊢ ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext S.X₁ L (n + 1))

Tactic:
simpa [this] using h
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L n)),
    HasProjectiveDimensionLT M n
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
⊢ HasProjectiveDimensionLT M (n + 1)

Tactic:
match n with
    | 0 =>
      simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
      have : Subsingleton (Ext M S.X₁ 1) := h S.X₁ inferInstance
      rcases Ext.covariant_sequence_exact₃ M hS (Ext.mk₀ (𝟙 M)) (zero_add 1)
        (Subsingleton.eq_zero _) with ⟨f', hf'⟩
      rcases (Ext.mk₀_bijective M S.X₂).2 f' with ⟨f, hf⟩
      rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'
      exact (Retract.mk f S.g hf').projective
    | n + 1 =>
      rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]
      have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr
      apply hn S.X₁
      simpa [this] using h
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
n : ℕ
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L n)
zero :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
        (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L n)),
        HasProjectiveDimensionLT M n)
    (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
⊢ HasProjectiveDimensionLT M n

Tactic:
induction n generalizing M with
  | zero =>
    have : Subsingleton (M ⟶ M) := Ext.homEquiv₀.subsingleton_congr.mp (h M ‹_›)
    have : Limits.IsZero M := (Limits.IsZero.iff_id_eq_zero M).mpr (Subsingleton.eq_zero (𝟙 M))
    exact this.hasProjectiveDimensionLT_zero
  | succ n hn =>
    rcases Module.exists_finite_presentation R M with ⟨_, _, _, _, _, f, surjf⟩
    let S : ShortComplex (ModuleCat.{v} R) := f.shortComplexKer
    have hS : S.ShortExact := LinearMap.shortExact_shortComplexKer surjf
    match n with
    | 0 =>
      simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
      have : Subsingleton (Ext M S.X₁ 1) := h S.X₁ inferInstance
      rcases Ext.covariant_sequence_exact₃ M hS (Ext.mk₀ (𝟙 M)) (zero_add 1)
        (Subsingleton.eq_zero _) with ⟨f', hf'⟩
      rcases (Ext.mk₀_bijective M S.X₂).2 f' with ⟨f, hf⟩
      rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'
      exact (Retract.mk f S.g hf').projective
    | n + 1 =>
      rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]
      have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr
      apply hn S.X₁
      simpa [this] using h

Premises used: Module.exists_finite_presentation, ModuleCat.carrier
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs
mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r
generalize :
  ∀ (n : ℕ) (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
    projectiveDimension M + (↑rs.length : WithBot ℕ∞)

Tactic:
generalize len : rs.length = n

Premises used: List.length
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs
mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r
len : rs.length = 0
zero :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R (HasQuotient.Quotient (↑M : Type v) (B := Submodule R (↑M : Type v)) ⊥)) =
    projectiveDimension M + (↑0 : WithBot ℕ∞)
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
    projectiveDimension M + (↑0 : WithBot ℕ∞)

Tactic:
rw [List.length_eq_zero_iff.mp len, Ideal.ofList_nil, Submodule.bot_smul]

Premises used: Submodule.bot_smul, Ideal.ofList_nil, Iff.mp, List.length_eq_zero_iff
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs
mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r
len : rs.length = 0
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R (HasQuotient.Quotient (↑M : Type v) (B := Submodule R (↑M : Type v)) ⊥)) =
    projectiveDimension M + (↑0 : WithBot ℕ∞)

Tactic:
simpa using projectiveDimension_eq_of_iso (Submodule.quotEquivOfEqBot ⊥ rfl).toModuleIso

Premises used: LinearEquiv.toModuleIso, Submodule.quotEquivOfEqBot, Bot.bot, CategoryTheory.projectiveDimension_eq_of_iso, rfl
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
reg : IsWeaklyRegular.{u, v} (R := R) (↑M : Type v) []
mem : ∀ (r : R), Membership.mem (γ := List R) [] r → Membership.mem (γ := Ideal R) (maximalIdeal R) r
len : List.length.{u} (α := R) [] = n + 1
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R
        ((↑M : Type v) ⧸ HSMul.hSMul.{u, v, v} (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList []) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)

Tactic:
simp at len
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
x : R
rs' : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) (x :: rs')
mem : ∀ r ∈ x :: rs', Membership.mem (γ := Ideal R) (maximalIdeal R) r
len : (x :: rs').length = n + 1
⊢ Membership.mem (γ := Ideal R) (maximalIdeal R) x ∧ ∀ a ∈ rs', Membership.mem (γ := Ideal R) (maximalIdeal R) a

Tactic:
simp only [List.mem_cons, forall_eq_or_imp] at mem

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
x : R
rs' : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) (x :: rs')
len : (x :: rs').length = n + 1
mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x ∧ ∀ a ∈ rs', Membership.mem (γ := Ideal R) (maximalIdeal R) a
⊢ IsSMulRegular.{u, v} (↑M : Type v) x ∧ IsWeaklyRegular.{u, v} (QuotSMulTop x (↑M : Type v)) rs'

Tactic:
simp only [isWeaklyRegular_cons_iff] at reg

Premises used: RingTheory.Sequence.isWeaklyRegular_cons_iff
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
x : R
rs' : List R
len : (x :: rs').length = n + 1
mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x ∧ ∀ a ∈ rs', Membership.mem (γ := Ideal R) (maximalIdeal R) a
reg : IsSMulRegular.{u, v} (↑M : Type v) x ∧ IsWeaklyRegular.{u, v} (QuotSMulTop x (↑M : Type v)) rs'
⊢ Nontrivial.{v} (QuotSMulTop x (↑M : Type v))

Tactic:
have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
x : R
rs' : List R
len : (x :: rs').length = n + 1
mem : Membership.mem (γ := Ideal R) (maximalIdeal R) x ∧ ∀ a ∈ rs', Membership.mem (γ := Ideal R) (maximalIdeal R) a
reg : IsSMulRegular.{u, v} (↑M : Type v) x ∧ IsWeaklyRegular.{u, v} (QuotSMulTop x (↑M : Type v)) rs'
this : Nontrivial.{v} (QuotSMulTop x (↑M : Type v))
⊢ rs'.length = n

Tactic:
simp only [List.length_cons, Nat.add_right_cancel_iff] at len

Premises used: Nat.add_right_cancel_iff, List.length_cons
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsLocalRing R
inst_3 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Nontrivial.{v} (↑M : Type v)] [Module.Finite.{u, v} R (↑M : Type v)] (rs : List R)
    (reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs) (mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r)
    (len : rs.length = n),
    projectiveDimension (C := ModuleCat.{v, u} R)
        (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
      projectiveDimension M + (↑n : WithBot ℕ∞)
M : ModuleCat.{v, u} R
inst_4 : Nontrivial.{v} (↑M : Type v)
inst_5 : Module.Finite.{u, v} R (↑M : Type v)
rs : List R
reg : IsWeaklyRegular.{u, v} (↑M : Type v) rs
mem : ∀ r ∈ rs, Membership.mem (γ := Ideal R) (maximalIdeal R) r
len : rs.length = n + 1
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)

Tactic:
match rs with
    | [] => simp at len
    | x :: rs' =>
      simp only [List.mem_cons, forall_eq_or_imp] at mem
      simp only [isWeaklyRegular_cons_iff] at reg
      have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
      simp only [List.length_cons, Nat.add_right_cancel_iff] at len
      rw [Nat.cast_add, Nat.cast_one, projectiveDimension_eq_of_iso
        (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x rs').toModuleIso, add_comm _ 1,
        ← add_assoc, ← projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular M x reg.1 mem.1,
        ← hn (ModuleCat.of R (QuotSMulTop x M)) rs' reg.2 mem.2 len]