awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ
⊢ HasProjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
M.hasProjectiveDimensionLE_iff_forall_primeSpectrum n

Premises used: ModuleCat.hasProjectiveDimensionLE_iff_forall_primeSpectrum
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ
⊢ HasProjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
exact M.hasProjectiveDimensionLE_iff_forall_primeSpectrum n

Premises used: ModuleCat.hasProjectiveDimensionLE_iff_forall_primeSpectrum
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ),
    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
-- Module: Mathlib.RingTheory.LocalProperties.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)
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)

Tactic:
eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
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
⊢ projectiveDimension M =
    ⨆ (p : PrimeSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
bot :
  Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ 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:
simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Equiv.subsingleton_congr, CategoryTheory.projectiveDimension_eq_bot_iff, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))

Tactic:
⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩

Premises used: LocalizedModule.instSubsingleton, Iff.intro, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
bot :
  ∀ (h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
    Subsingleton.{v + 1} (↑M : Type v)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))

Tactic:
refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))
bot : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑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)

Premises used: Module.subsingleton_of_localization_maximal, LocalizedModule, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
h ⟨p, hp.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
exact h ⟨p, hp.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ≤ (↑⊤ : 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:
simp
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞) ↔
    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:
simpa using aux n
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
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 ℕ∞)
⊢ 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
    | top => simp
    | coe n => simpa using aux n
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))
      ⊥
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 ℕ∞)
⊢ projectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N

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

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Module.subsingleton_of_localization_maximal, LocalizedModule, Equiv.subsingleton_congr, CategoryTheory.projectiveDimension_eq_bot_iff, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ
simp :
  HasProjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) 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:
simp only [projectiveDimension_le_iff, iSup_le_iff]

Premises used: CategoryTheory.projectiveDimension_le_iff, iSup_le_iff
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ
⊢ HasProjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
M.hasProjectiveDimensionLE_iff_forall_maximalSpectrum n

Premises used: ModuleCat.hasProjectiveDimensionLE_iff_forall_maximalSpectrum
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ
⊢ HasProjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
exact M.hasProjectiveDimensionLE_iff_forall_maximalSpectrum n

Premises used: ModuleCat.hasProjectiveDimensionLE_iff_forall_maximalSpectrum
-- Module: Mathlib.RingTheory.LocalProperties.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 : ℕ),
    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
-- Module: Mathlib.RingTheory.LocalProperties.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)
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)

Tactic:
eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
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
⊢ projectiveDimension M =
    ⨆ (p : MaximalSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
bot :
  Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ projectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥

Tactic:
simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Equiv.subsingleton_congr, CategoryTheory.projectiveDimension_eq_bot_iff, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))

Tactic:
⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩

Premises used: MaximalSpectrum.asIdeal, LocalizedModule.instSubsingleton, Iff.intro, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.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)
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 ℕ∞)
bot :
  ∀ (h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
    Subsingleton.{v + 1} (↑M : Type v)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))

Tactic:
refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.LocalProperties.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)
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))
bot : ∀ (P : Ideal R) [inst_4 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑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)

Premises used: Module.subsingleton_of_localization_maximal, LocalizedModule, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl