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)
zero :
  Projective M ↔
    ∀ (m : MaximalSpectrum R),
      Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)
⊢ HasProjectiveDimensionLE M 0 ↔
    ∀ (m : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) 0

Tactic:
simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one]

Premises used: CategoryTheory.HasProjectiveDimensionLE, zero_add, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- 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)
⊢ Projective M ↔
    ∀ (m : MaximalSpectrum R),
      Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)

Tactic:
⟨fun h p ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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)
zero :
  ∀ (h : Projective M) (p : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
      (M.localizedModule p.asIdeal.primeCompl)
zero₁ :
  ∀
    (h :
      ∀ (m : MaximalSpectrum R),
        Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl)),
    Projective M
⊢ Projective M ↔
    ∀ (m : MaximalSpectrum R),
      Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)

Tactic:
refine ⟨fun h p ↦ ?_, 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)
h : Projective M
p : MaximalSpectrum R
this : Small.{v, u} (Localization (M := R) p.asIdeal.primeCompl) := ⋯
zero :
  Module.Projective.{u, v} (Localization (M := R) p.asIdeal.primeCompl)
    (↑(M.localizedModule p.asIdeal.primeCompl) : Type v)
⊢ Projective (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
    (M.localizedModule p.asIdeal.primeCompl)

Tactic:
rw [← IsProjective.iff_projective]

Premises used: IsProjective.iff_projective
-- 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)
h : Projective M
p : MaximalSpectrum R
this : Small.{v, u} (Localization (M := R) p.asIdeal.primeCompl) := ⋯
⊢ Module.Projective.{u, v} (Localization (M := R) p.asIdeal.primeCompl)
    (↑(M.localizedModule p.asIdeal.primeCompl) : Type v)

Tactic:
Module.projective_of_isLocalizedModule p.1.primeCompl
        (M.localizedModuleMkLinearMap p.1.primeCompl)

Premises used: MaximalSpectrum.asIdeal, Module.projective_of_isLocalizedModule, ModuleCat.localizedModuleMkLinearMap, 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)
h : Projective M
p : MaximalSpectrum R
this : Small.{v, u} (Localization (M := R) p.asIdeal.primeCompl) := ⋯
⊢ Module.Projective.{u, v} (Localization (M := R) p.asIdeal.primeCompl)
    (↑(M.localizedModule p.asIdeal.primeCompl) : Type v)

Tactic:
exact Module.projective_of_isLocalizedModule p.1.primeCompl
        (M.localizedModuleMkLinearMap p.1.primeCompl)

Premises used: MaximalSpectrum.asIdeal, Module.projective_of_isLocalizedModule, ModuleCat.localizedModuleMkLinearMap, 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
zero : Module.Projective.{u, v} R (↑M : Type v)
⊢ Projective M

Tactic:
rw [← IsProjective.iff_projective]

Premises used: IsProjective.iff_projective
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
⊢ Module.FinitePresentation.{u, v} R (↑M : Type v)

Tactic:
have : Module.FinitePresentation R M := Module.finitePresentation_of_finite R M
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
this : Module.FinitePresentation.{u, v} R (↑M : Type v)
apply :
  ∀ (p : Ideal R) (hp : p.IsMaximal),
    Module.Projective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
⊢ Module.Projective.{u, v} R (↑M : Type v)

Tactic:
apply Module.projective_of_localization_maximal (fun p hp ↦ ?_)

Premises used: Module.projective_of_localization_maximal
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
this_1 : Module.FinitePresentation.{u, v} R (↑M : Type v)
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := ⋯
⊢ Module.Projective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)

Tactic:
simpa [IsProjective.iff_projective] using h ⟨p, hp⟩

Premises used: MaximalSpectrum.mk, IsProjective.iff_projective
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
this : Module.FinitePresentation.{u, v} R (↑M : Type v)
p : Ideal R
hp : p.IsMaximal
⊢ Module.Projective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)

Tactic:
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⟩
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
this_1 : Module.FinitePresentation.{u, v} R (↑M : Type v)
p : Ideal R
hp : p.IsMaximal
this : Module.Projective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)
⊢ Module.Projective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
Module.Projective.of_equiv (LinearEquiv.extendScalarsOfIsLocalization p.primeCompl
        (Localization.AtPrime p) (IsLocalizedModule.linearEquiv p.primeCompl
        (M.localizedModuleMkLinearMap p.primeCompl)
        (LocalizedModule.mkLinearMap p.primeCompl M)))

Premises used: IsLocalizedModule.linearEquiv, Localization.AtPrime, ModuleCat.localizedModuleMkLinearMap, Module.Projective.of_equiv, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, LinearEquiv.extendScalarsOfIsLocalization
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
this_1 : Module.FinitePresentation.{u, v} R (↑M : Type v)
p : Ideal R
hp : p.IsMaximal
this : Module.Projective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)
⊢ Module.Projective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
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)))

Premises used: IsLocalizedModule.linearEquiv, Localization.AtPrime, ModuleCat.localizedModuleMkLinearMap, Module.Projective.of_equiv, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, LinearEquiv.extendScalarsOfIsLocalization
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R) [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
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
succ :
  ∀ (P : Type v) (w : AddCommGroup P) (w_1 : Module R P),
    Module.Free R P →
      Module.Finite R P →
        ∀ (f : P →ₗ[R] (↑M : Type v))
          (surjf : Function.Surjective (α := P) (β := (↑M : Type v)) (⇑f : (a : P) → (↑M : Type v))),
          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)
⊢ 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)

Tactic:
rcases Module.exists_finite_presentation R M with ⟨P, _, _, _, _, f, surjf⟩

Premises used: Module.exists_finite_presentation, ModuleCat.carrier
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R) [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
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
⊢ f.shortComplexKer.ShortExact

Tactic:
have S_exact := LinearMap.shortExact_shortComplexKer surjf
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R) [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
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
⊢ Projective S.X₂

Tactic:
have proj := ModuleCat.projective_of_categoryTheory_projective S.X₂
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R) [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
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)
⊢ ∀ (p : MaximalSpectrum R), (Sp p).ShortExact

Tactic:
have Sp_exact (p : MaximalSpectrum R) : (Sp p).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor p.asIdeal.primeCompl)
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R) [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
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
⊢ HasProjectiveDimensionLE (C := ModuleCat.{v, u} R) (of R ↥f.ker) n ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLE (localizedModule (of R ↥f.ker) m.asIdeal.primeCompl) n

Tactic:
specialize ih (ModuleCat.of R (LinearMap.ker f))

Premises used: LinearMap.ker, Membership.mem, Subtype, ModuleCat.of
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
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
⊢ ∀ (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
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
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₂
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)
⊢ 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)

Tactic:
rw [S_exact.hasProjectiveDimensionLT_X₃_iff n proj, ih]

Premises used: CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
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₂
⊢ (∀ (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:
(forall_congr' (fun p ↦ (Sp_exact p).hasProjectiveDimensionLT_X₃_iff n (projp p))).symm

Premises used: Set.Mem, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, forall_congr', ModuleCat.localizedModule, Iff.symm
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
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₂
⊢ (∀ (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:
exact (forall_congr' (fun p ↦ (Sp_exact p).hasProjectiveDimensionLT_X₃_iff n (projp p))).symm

Premises used: CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, forall_congr', Iff.symm
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
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 ↔
    ∀ (p : PrimeSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl) n

Tactic:
⟨fun _ p ↦ M.localizedModule_hasProjectiveDimensionLE n p.1.primeCompl,
    fun h ↦ (M.hasProjectiveDimensionLE_iff_forall_maximalSpectrum n).mpr
    fun m ↦ h ⟨m.1, Ideal.IsMaximal.isPrime' m.1⟩⟩

Premises used: MaximalSpectrum.asIdeal, Iff.mpr, PrimeSpectrum.mk, ModuleCat.localizedModule_hasProjectiveDimensionLE, ModuleCat.hasProjectiveDimensionLE_iff_forall_maximalSpectrum, Iff.intro, Ideal.primeCompl, PrimeSpectrum.asIdeal, 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)
n : ℕ
simp :
  HasProjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum 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 : PrimeSpectrum 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