-- 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
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 ℕ∞)
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 + 1 + (↑n : WithBot ℕ∞)
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 (C := ModuleCat.{v, u} R) (of R (QuotSMulTop x (↑M : Type v))) + (↑n : 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
      (QuotSMulTop x (↑M : Type v) ⧸
        HSMul.hSMul (α := Ideal R) (β := Submodule R (QuotSMulTop x (↑M : Type v))) (Ideal.ofList rs') ⊤)) =
  projectiveDimension (C := ModuleCat.{v, u} R)
    (of R
      ((↑(of R (QuotSMulTop x (↑M : Type v))) : Type v) ⧸
        HSMul.hSMul (α := Ideal R) (β := Submodule R (↑(of R (QuotSMulTop x (↑M : Type v))) : Type v))
          (Ideal.ofList rs') ⊤))
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]