awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u_1, u_1, uM, u_5} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective.{u_4, u_5} (Rₚ I) (Mₚ I)
inst_11 : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : RingEquiv.{u_4, u_1} (Rₚ P) (Localization.AtPrime P) :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P))
r : Rₚ P
m : Mₚ P
H₁ :
  ∀ (r : R) (s : ↥P.primeCompl),
    AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        (HSMul.hSMul.{u_4, u_5, u_5} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m) =
      HSMul.hSMul (α := Localization.AtPrime P)
        ((((↑e : RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
              RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
            (a : Rₚ P) → Localization.AtPrime P)
          (IsLocalization.mk' (Rₚ P) r s))
        (AddHom.toFun
          (LinearMap.toAddHom
            (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
              Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
          m)
⊢ AddHom.toFun
      (LinearMap.toAddHom
        (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
          Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
      (r • m) =
    HSMul.hSMul (α := Localization.AtPrime P)
      ((((↑e : RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
              RingHom.{u_4, u_1} (Rₚ P) (Localization.AtPrime P)) :
            (a : Rₚ P) → Localization.AtPrime P)
          r :
        Localization.AtPrime P)
      (AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        m)

Tactic:
obtain ⟨r, s, rfl⟩ := IsLocalization.exists_mk'_eq P.primeCompl r

Premises used: Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.LocalProperties.Projective
Goal:
R : Type u_1
M : Type uM
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u_1, u_1, uM, u_5} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective.{u_4, u_5} (Rₚ I) (Mₚ I)
inst_11 : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : RingEquiv.{u_4, u_1} (Rₚ P) (Localization.AtPrime P) :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P))
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ HSMul.hSMul (β := LocalizedModule P.primeCompl M) (↑s : R)
      ((IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M) :
            (a : Mₚ P) → LocalizedModule P.primeCompl M)
          (HSMul.hSMul.{u_4, u_5, u_5} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m) :
        LocalizedModule P.primeCompl M) =
    (↑s : R) •
      HSMul.hSMul (α := Localization.AtPrime P) (β := LocalizedModule P.primeCompl M)
        ((IsLocalization.map (M := P.primeCompl) (T := P.primeCompl) (Localization.AtPrime P) (RingHom.id R) ⋯ :
            (a : Rₚ P) → Localization.AtPrime P)
          (IsLocalization.mk' (Rₚ P) r s))
        ((IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M) :
              (a : Mₚ P) → LocalizedModule P.primeCompl M)
            m :
          LocalizedModule P.primeCompl M)

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

Premises used: smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul, IsLocalization.map_id_mk', map_smul
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X : ModuleCat.{v, u} R
proj : Projective X
⊢ Small.{v, u} (Localization (M := R) S)

Tactic:
have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X : ModuleCat.{v, u} R
proj : Projective X
this : Small.{v, u} (Localization (M := R) S)
rw :
  ∀ (proj : Module.Projective.{u, v} R (↑X : Type v)) (this : Small.{v, u} (Localization (M := R) S)),
    Module.Projective.{u, v} (Localization (M := R) S) (↑((localizedModuleFunctor.{v, u} S).1 X) : Type v)
⊢ Projective ((localizedModuleFunctor S).obj X)

Tactic:
rw [← IsProjective.iff_projective] at proj ⊢

Premises used: IsProjective.iff_projective
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
X : ModuleCat.{v, u} R
proj : Module.Projective.{u, v} R (↑X : Type v)
this : Small.{v, u} (Localization (M := R) S)
⊢ Module.Projective.{u, v} (Localization (M := R) S) (↑((localizedModuleFunctor.{v, u} S).1 X) : Type v)

Tactic:
simpa [ModuleCat.localizedModuleFunctor] using
      Module.projective_of_isLocalizedModule S (X.localizedModuleMkLinearMap S)

Premises used: Module.projective_of_isLocalizedModule, ModuleCat.localizedModuleFunctor, ModuleCat.localizedModuleMkLinearMap
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
n : ℕ
S : Submonoid R
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M n
⊢ Small.{v, u} (Localization (M := R) S)

Tactic:
have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M 0
⊢ HasProjectiveDimensionLE M 0

Tactic:
have projle : HasProjectiveDimensionLE M 0 := ‹_›
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 projle : HasProjectiveDimensionLE M 0
⊢ HasProjectiveDimensionLT M 1

Tactic:
simp only [HasProjectiveDimensionLE, zero_add] at projle ⊢

Premises used: CategoryTheory.HasProjectiveDimensionLE, zero_add
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M 0
projle : HasProjectiveDimensionLT M 1
zero :
  ∀ (projle : Module.Projective.{u, v} R (↑M : Type v)),
    Module.Projective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)
⊢ HasProjectiveDimensionLT (M.localizedModule S) 1

Tactic:
rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at projle ⊢

Premises used: IsProjective.iff_projective, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M 0
projle : Module.Projective.{u, v} R (↑M : Type v)
⊢ Module.Projective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)

Tactic:
Module.projective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)

Premises used: Module.projective_of_isLocalizedModule, ModuleCat.localizedModuleMkLinearMap
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M 0
projle : Module.Projective.{u, v} R (↑M : Type v)
⊢ Module.Projective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)

Tactic:
exact Module.projective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)

Premises used: Module.projective_of_isLocalizedModule, ModuleCat.localizedModuleMkLinearMap
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
succ :
  ∀ (P : ModuleCat.{v, u} R) [Projective P] (f : P ⟶ M) [Epi f], HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
rcases ModuleCat.enoughProjectives.1 M with ⟨⟨P, f⟩⟩

Premises used: CategoryTheory.EnoughProjectives.presentation
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
⊢ T.ShortExact

Tactic:
have T_exact : T.ShortExact := { exact := ShortComplex.exact_kernel f }
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
⊢ TS.ShortExact

Tactic:
have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
⊢ Projective TS.X₂

Tactic:
have : Projective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).projective_obj _
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this_1 : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
this : Projective TS.X₂
⊢ HasProjectiveDimensionLT T.X₁ (n + 1)

Tactic:
have := (T_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mp ‹_›
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this_1 : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
this_2 : Projective TS.X₂
this : HasProjectiveDimensionLT T.X₁ (n + 1)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
(TS_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mpr (ih (kernel f))

Premises used: Iff.mpr, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, CategoryTheory.Limits.kernel, ModuleCat.localizedModule
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
this_1 : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M (n + 1)
P : ModuleCat.{v, u} R
projective : Projective P
f : P ⟶ M
epi : Epi f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₁ := kernel f) (kernel.ι f) f ⋯
T_exact : T.ShortExact
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
this_2 : Projective TS.X₂
this : HasProjectiveDimensionLT T.X₁ (n + 1)
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
exact (TS_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mpr (ih (kernel f))

Premises used: Iff.mpr, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, CategoryTheory.Limits.kernel
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
n : ℕ
S : Submonoid R
M : ModuleCat.{v, u} R
inst_2 : HasProjectiveDimensionLE M n
this : Small.{v, u} (Localization (M := R) S)
zero : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M 0], HasProjectiveDimensionLE (M.localizedModule S) 0
succ :
  ∀ (n : ℕ)
    (ih : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M n], HasProjectiveDimensionLE (M.localizedModule S) n)
    (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M (n + 1)],
    HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
⊢ HasProjectiveDimensionLE (M.localizedModule S) n

Tactic:
induction n generalizing M with
  | zero =>
    have projle : HasProjectiveDimensionLE M 0 := ‹_›
    simp only [HasProjectiveDimensionLE, zero_add] at projle ⊢
    rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at projle ⊢
    exact Module.projective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)
  | succ n ih =>
    rcases ModuleCat.enoughProjectives.1 M with ⟨⟨P, f⟩⟩
    let T := ShortComplex.mk (kernel.ι f) f (kernel.condition f)
    have T_exact : T.ShortExact := { exact := ShortComplex.exact_kernel f }
    let TS := T.map (ModuleCat.localizedModuleFunctor S)
    have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
    have : Projective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).projective_obj _
    have := (T_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mp ‹_›
    exact (TS_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mpr (ih (kernel f))

Premises used: CategoryTheory.EnoughProjectives.presentation, IsProjective.iff_projective, 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
S : Submonoid R
M : ModuleCat.{v, u} R
n : ℕ
simp : HasProjectiveDimensionLE M n → HasProjectiveDimensionLE (M.localizedModule S) n
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)

Tactic:
simp only [projectiveDimension_le_iff]

Premises used: CategoryTheory.projectiveDimension_le_iff
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
n : ℕ
h : HasProjectiveDimensionLE M n
⊢ HasProjectiveDimensionLE (M.localizedModule S) n

Tactic:
ModuleCat.localizedModule_hasProjectiveDimensionLE n S M

Premises used: ModuleCat.localizedModule_hasProjectiveDimensionLE
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
n : ℕ
h : HasProjectiveDimensionLE M n
⊢ HasProjectiveDimensionLE (M.localizedModule S) n

Tactic:
exact ModuleCat.localizedModule_hasProjectiveDimensionLE n S M

Premises used: ModuleCat.localizedModule_hasProjectiveDimensionLE
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
⊢ ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)

Tactic:
have aux (n : ℕ) : projectiveDimension M ≤ n → projectiveDimension (M.localizedModule S) ≤ n := by
    simp only [projectiveDimension_le_iff]
    intro h
    exact ModuleCat.localizedModule_hasProjectiveDimensionLE n S M
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ projectiveDimension (M.localizedModule S) ≤ projectiveDimension M

Tactic:
le_of_forall_ge (fun N ↦ ?_)

Premises used: le_of_forall_ge
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
refine : ∀ (N : WithBot ℕ∞), projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N
⊢ projectiveDimension (M.localizedModule S) ≤ projectiveDimension M

Tactic:
refine le_of_forall_ge (fun N ↦ ?_)

Premises used: le_of_forall_ge
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
bot : Subsingleton.{v + 1} (↑M : Type v) → Subsingleton (LocalizedModule.{u, v} S (↑M : Type v))
⊢ projectiveDimension M ≤ ⊥ → projectiveDimension (M.localizedModule S) ≤ ⊥

Tactic:
simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      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
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
h : Subsingleton.{v + 1} (↑M : Type v)
⊢ Subsingleton (LocalizedModule.{u, v} S (↑M : Type v))

Tactic:
apply LocalizedModule.instSubsingleton _

Premises used: LocalizedModule.instSubsingleton
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑⊤ : WithBot ℕ∞)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
n : ℕ
⊢ projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) →
    projectiveDimension (M.localizedModule S) ≤ (↑(↑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
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
N : ℕ∞
coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑⊤ : WithBot ℕ∞)
coe₁ :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) →
      projectiveDimension (M.localizedModule S) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑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
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot : projectiveDimension M ≤ ⊥ → projectiveDimension (M.localizedModule S) ≤ ⊥
coe :
  ∀ (N : ℕ∞), projectiveDimension M ≤ (↑N : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)
⊢ projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N

Tactic:
induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    intro _
    apply LocalizedModule.instSubsingleton _
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, LocalizedModule.instSubsingleton, Equiv.subsingleton_congr, CategoryTheory.projectiveDimension_eq_bot_iff, ModuleCat.localizedModule, equivShrink