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
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
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
have this₁ : Projective TS.X₂
Tactic: have : Projective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).projective_obj _
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (hypothesis)
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₂
⊢ HasProjectiveDimensionLE (M.localizedModule S) (n + 1)
have this₁ : HasProjectiveDimensionLT T.X₁ (n + 1)
Tactic: have := (T_exact.hasProjectiveDimensionLT_X₃_iff n ‹_›).mp ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
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)
⊢ HasProjectiveDimensionLE (M.localizedModule S) n
have zero : ∀ (M : ModuleCat.{v, u} R) [HasProjectiveDimensionLE M 0], HasProjectiveDimensionLE (M.localizedModule S) 0
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))
Cleared hypotheses: n, M, inst_2
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
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
⊢ HasProjectiveDimensionLE (M.localizedModule S) n
have 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)
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))
Cleared hypotheses: n, M, inst_2
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
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 ℕ∞)
have simp : HasProjectiveDimensionLE M n → HasProjectiveDimensionLE (M.localizedModule S) n
Tactic: simp only [projectiveDimension_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
S : Submonoid R
M : ModuleCat.{v, u} R
⊢ projectiveDimension (M.localizedModule S) ≤ projectiveDimension M
have aux : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
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
have refine : ∀ (N : WithBot ℕ∞), projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N
Tactic: refine le_of_forall_ge (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
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ projectiveDimension M ≤ ⊥ → projectiveDimension (M.localizedModule S) ≤ ⊥
have bot : Subsingleton.{v + 1} (↑M : Type v) → Subsingleton (LocalizedModule.{u, v} S (↑M : Type v))
Tactic: simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      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
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 ℕ∞)
have coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑⊤ : 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
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 ℕ∞)
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)
have coe₁ : ∀ (n : ℕ),
  projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) →
    projectiveDimension (M.localizedModule S) ≤ (↑(↑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
S : Submonoid R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ), projectiveDimension M ≤ (↑n : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
⊢ projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N
have bot : projectiveDimension M ≤ ⊥ → projectiveDimension (M.localizedModule S) ≤ ⊥
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
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
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) ≤ ⊥
⊢ projectiveDimension M ≤ N → projectiveDimension (M.localizedModule S) ≤ N
have coe : ∀ (N : ℕ∞), projectiveDimension M ≤ (↑N : WithBot ℕ∞) → projectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)
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
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)
⊢ HasProjectiveDimensionLE M 0 ↔
    ∀ (m : MaximalSpectrum R),
      HasProjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) 0
have zero : Projective M ↔
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
Tactic: simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
-- 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)
⊢ Projective M ↔
    ∀ (m : MaximalSpectrum R),
      Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)
have zero : ∀ (h : Projective M) (p : MaximalSpectrum R),
  Projective (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
    (M.localizedModule p.asIdeal.primeCompl)
Tactic: refine ⟨fun h p ↦ ?_, 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)
zero :
  ∀ (h : Projective M) (p : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
      (M.localizedModule p.asIdeal.primeCompl)
⊢ Projective M ↔
    ∀ (m : MaximalSpectrum R),
      Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)
have zero₁ : ∀
  (h :
    ∀ (m : MaximalSpectrum R),
      Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)),
  Projective M
Tactic: refine ⟨fun h p ↦ ?_, 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)
h : Projective M
p : MaximalSpectrum R
this : Small.{v, u} (Localization (M := R) p.asIdeal.primeCompl) := ⋯
⊢ Projective (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
    (M.localizedModule p.asIdeal.primeCompl)
have zero : Module.Projective.{u, v} (Localization (M := R) p.asIdeal.primeCompl)
  (↑(M.localizedModule p.asIdeal.primeCompl) : Type v)
Tactic: rw [← IsProjective.iff_projective]
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
⊢ Projective M
have zero : Module.Projective.{u, v} R (↑M : Type v)
Tactic: rw [← IsProjective.iff_projective]
-- 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)
h :
  ∀ (m : MaximalSpectrum R),
    Projective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
⊢ Module.Projective.{u, v} R (↑M : Type v)
have this : Module.FinitePresentation.{u, v} R (↑M : Type v)
Tactic: have : Module.FinitePresentation R M := Module.finitePresentation_of_finite R 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)
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)
⊢ Module.Projective.{u, v} R (↑M : Type v)
have apply : ∀ (p : Ideal R) (hp : p.IsMaximal),
  Module.Projective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
Tactic: apply Module.projective_of_localization_maximal (fun p hp ↦ ?_)
-- 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)
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 (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
have this₁ : 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⟩
-- 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 : ℕ
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)
⊢ 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 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)
Tactic: rcases Module.exists_finite_presentation R M with ⟨P, _, _, _, _, f, surjf⟩
-- 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 : ℕ
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
⊢ 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 S_exact : f.shortComplexKer.ShortExact
Tactic: have S_exact := LinearMap.shortExact_shortComplexKer surjf
-- 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 : ℕ
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
⊢ 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 proj : Projective S.X₂
Tactic: have proj := ModuleCat.projective_of_categoryTheory_projective S.X₂
-- 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 : ℕ
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)
⊢ 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 Sp_exact : ∀ (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)
-- 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 : ℕ
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 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 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
Tactic: specialize ih (ModuleCat.of R (LinearMap.ker f))
Cleared hypotheses: ih