awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
P : Type v
w : AddCommGroup P
w_1 : Module R P
w_2 : Module.Free R P
w_3 : Module.Finite R P
f : P →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := P) (β := (↑M : Type v)) (⇑f : (a : P) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl)) :=
  fun (p : MaximalSpectrum R) ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
ih :
  HasProjectiveDimensionLE (C := ModuleCat.{v, u} R) (of R ↥f.ker) n ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (localizedModule (of R ↥f.ker) m.asIdeal.primeCompl) n
⊢ HasProjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) (n + 1)
have projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
Tactic: have projp (p : MaximalSpectrum R) : Projective (Sp p).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} p.1.primeCompl).projective_obj_of_projective proj
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
P : Type v
w : AddCommGroup P
w_1 : Module R P
w_2 : Module.Free R P
w_3 : Module.Finite R P
f : P →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := P) (β := (↑M : Type v)) (⇑f : (a : P) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl)) :=
  fun (p : MaximalSpectrum R) ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
ih :
  HasProjectiveDimensionLT (C := ModuleCat.{v, u} R) (of R ↥f.ker) (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT (localizedModule (of R ↥f.ker) m.asIdeal.primeCompl) (n + 1)
projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
⊢ HasProjectiveDimensionLT M (n + 1 + 1) ↔
    ∀ (m : MaximalSpectrum R),
      HasProjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)
have succ : (∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT (localizedModule (of R ↥f.ker) m.asIdeal.primeCompl) (n + 1)) ↔
  ∀ (m : MaximalSpectrum R),
    HasProjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)
Tactic: rw [S_exact.hasProjectiveDimensionLT_X₃_iff n proj, ih]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
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)
⊢ HasProjectiveDimensionLE M n ↔
    ∀ (m : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) n
have zero : ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)],
  HasProjectiveDimensionLE M 0 ↔
    ∀ (m : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) 0
Tactic: induction n generalizing M with
  | zero =>
    simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
    refine ⟨fun h p ↦ ?_, fun h ↦ ?_⟩
    · let : Small.{v} (Localization p.asIdeal.primeCompl) :=
        small_of_surjective Localization.mkHom_surjective
      rw [← IsProjective.iff_projective]
      exact Module.projective_of_isLocalizedModule p.1.primeCompl
        (M.localizedModuleMkLinearMap p.1.primeCompl)
    · rw [← IsProjective.iff_projective]
      have : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
      apply Module.projective_of_localization_maximal (fun p hp ↦ ?_)
      have : Module.Projective (Localization.AtPrime p) (M.localizedModule p.primeCompl) := by
        let : Small.{v} (Localization.AtPrime p) :=
          small_of_surjective Localization.mkHom_surjective
        simpa [IsProjective.iff_projective] using h ⟨p, hp⟩
      exact Module.Projective.of_equiv (LinearEquiv.extendScalarsOfIsLocalization p.primeCompl
        (Localization.AtPrime p) (IsLocalizedModule.linearEquiv p.primeCompl
        (M.localizedModuleMkLinearMap p.primeCompl)
        (LocalizedModule.mkLinearMap p.primeCompl M)))
  | succ n ih =>
    rcases Module.exists_finite_presentation R M with ⟨P, _, _, _, _, f, surjf⟩
    let S := f.shortComplexKer
    have S_exact := LinearMap.shortExact_shortComplexKer surjf
    have proj := ModuleCat.projective_of_categoryTheory_projective S.X₂
    let Sp (p : MaximalSpectrum R) := S.map (ModuleCat.localizedModuleFunctor p.1.primeCompl)
    have Sp_exact (p : MaximalSpectrum R) : (Sp p).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor p.asIdeal.primeCompl)
    specialize ih (ModuleCat.of R (LinearMap.ker f))
    have projp (p : MaximalSpectrum R) : Projective (Sp p).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} p.1.primeCompl).projective_obj_of_projective proj
    simp only [HasProjectiveDimensionLE] at ih ⊢
    rw [S_exact.hasProjectiveDimensionLT_X₃_iff n proj, ih]
    exact (forall_congr' (fun p ↦ (Sp_exact p).hasProjectiveDimensionLT_X₃_iff n (projp p))).symm
Cleared hypotheses: n, M, inst_3
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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 : ℕ
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑n : WithBot ℕ∞)
have simp : HasProjectiveDimensionLE M n ↔
  ∀ (i : PrimeSpectrum R),
    HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
      (M.localizedModule i.asIdeal.primeCompl) n
Tactic: simp only [projectiveDimension_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
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)
⊢ projectiveDimension M =
    ⨆ (p : PrimeSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)
have aux : ∀ (n : ℕ),
  projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑n : WithBot ℕ∞)
Tactic: have aux (n : ℕ) : projectiveDimension M ≤ n ↔ ⨆ (p : PrimeSpectrum R), projectiveDimension
    (M.localizedModule p.1.primeCompl) ≤ n := by
    simp only [projectiveDimension_le_iff, iSup_le_iff]
    exact M.hasProjectiveDimensionLE_iff_forall_primeSpectrum n
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ projectiveDimension M =
    ⨆ (p : PrimeSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)
have refine : ∀ (N : WithBot ℕ∞),
  projectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
Tactic: refine eq_of_forall_ge_iff (fun N ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ projectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
have bot : Subsingleton.{v + 1} (↑M : Type v) ↔
  ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
Tactic: simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
have bot : ∀ (h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
  Subsingleton.{v + 1} (↑M : Type v)
Tactic: refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑M : Type v)
have bot : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
Tactic: apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
  LE.le (α := WithBot ℕ∞)
    (⨆ (p : PrimeSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl))
    (↑⊤ : WithBot ℕ∞)
Tactic: induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
coe :
  projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have coe₁ : ∀ (n : ℕ),
  projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑(↑n : ℕ∞) : WithBot ℕ∞)
Tactic: induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
⊢ projectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have bot : projectiveDimension M ≤ ⊥ ↔
  LE.le (α := WithBot ℕ∞)
    (⨆ (p : PrimeSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl))
    ⊥
Tactic: induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp.isPrime⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot :
  projectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
⊢ projectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have coe : ∀ (N : ℕ∞),
  projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
Tactic: induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp.isPrime⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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 : ℕ
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑n : WithBot ℕ∞)
have simp : HasProjectiveDimensionLE M n ↔
  ∀ (i : MaximalSpectrum R),
    HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
      (M.localizedModule i.asIdeal.primeCompl) n
Tactic: simp only [projectiveDimension_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
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)
⊢ projectiveDimension M =
    ⨆ (p : MaximalSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)
have aux : ∀ (n : ℕ),
  projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑n : WithBot ℕ∞)
Tactic: have aux (n : ℕ) : projectiveDimension M ≤ n ↔ ⨆ (p : MaximalSpectrum R), projectiveDimension
    (M.localizedModule p.1.primeCompl) ≤ n := by
    simp only [projectiveDimension_le_iff, iSup_le_iff]
    exact M.hasProjectiveDimensionLE_iff_forall_maximalSpectrum n
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ projectiveDimension M =
    ⨆ (p : MaximalSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)
have refine : ∀ (N : WithBot ℕ∞),
  projectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
Tactic: refine eq_of_forall_ge_iff (fun N ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ projectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
have bot : Subsingleton.{v + 1} (↑M : Type v) ↔
  ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
Tactic: simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
have bot : ∀ (h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
  Subsingleton.{v + 1} (↑M : Type v)
Tactic: refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.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)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑M : Type v)
have bot : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
Tactic: apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)