awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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)
⊢ HasProjectiveDimensionLT M n
have 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
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
Cleared hypotheses: M, inst_3, n, h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
⊢ HasProjectiveDimensionLT M n
have 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)
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
Cleared hypotheses: M, inst_3, n, h
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
⊢ 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 ℕ∞)
have 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 ℕ∞)
Tactic: generalize len : rs.length = n
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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 ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList rs) ⊤)) =
    projectiveDimension M + (↑0 : WithBot ℕ∞)
have zero : projectiveDimension (C := ModuleCat.{v, u} R)
    (of R (HasQuotient.Quotient (↑M : Type v) (B := Submodule R (↑M : Type v)) ⊥)) =
  projectiveDimension M + (↑0 : WithBot ℕ∞)
Tactic: rw [List.length_eq_zero_iff.mp len, Ideal.ofList_nil, Submodule.bot_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have mem₁ : 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
Cleared hypotheses: mem
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have reg₁ : IsSMulRegular.{u, v} (↑M : Type v) x ∧ IsWeaklyRegular.{u, v} (QuotSMulTop x (↑M : Type v)) rs'
Tactic: simp only [isWeaklyRegular_cons_iff] at reg
Cleared hypotheses: reg
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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'
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have this : Nontrivial.{v} (QuotSMulTop x (↑M : Type v))
Tactic: have := nontrivial_quotSMulTop_of_mem_maximalIdeal M mem.1
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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))
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have len₁ : rs'.length = n
Tactic: simp only [List.length_cons, Nat.add_right_cancel_iff] at len
Cleared hypotheses: len
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
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))
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 (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have rw : projectiveDimension (C := ModuleCat.{v, u} R)
    (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
  projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑1 : WithBot ℕ∞)
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
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))
len : rs'.length = n
rw :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑1 : WithBot ℕ∞)
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have rw₁ : projectiveDimension (C := ModuleCat.{v, u} R)
    (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
  projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
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))
len : rs'.length = n
rw :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑1 : WithBot ℕ∞)
rw₁ :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have rw₂ : projectiveDimension (C := ModuleCat.{v, u} R)
    (of R
      (QuotSMulTop x (↑M : Type v) ⧸
        HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
  projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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
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))
len : rs'.length = n
rw :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) (↑1 : WithBot ℕ∞)
rw₁ :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
rw₂ :
  projectiveDimension (C := ModuleCat.{v, u} R)
      (of R
        (QuotSMulTop x (↑M : Type v) ⧸
          HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
    projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) (↑n : WithBot ℕ∞) 1
⊢ projectiveDimension (C := ModuleCat.{v, u} R)
      (of R ((↑M : Type v) ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R (↑M : Type v)) (Ideal.ofList (x :: rs')) ⊤)) =
    projectiveDimension M + (↑(n + 1) : WithBot ℕ∞)
have rw₃ : projectiveDimension (C := ModuleCat.{v, u} R)
    (of R
      (QuotSMulTop x (↑M : Type v) ⧸
        HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
  projectiveDimension M + HAdd.hAdd (α := WithBot ℕ∞) 1 (↑n : WithBot ℕ∞)
Tactic: 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]