awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
h_3 : FinitePresentation R N := ⋯
f_ne0 : Subsingleton (N →ₗ[R] M)
⊢ f = 0

Tactic:
(Module.FinitePresentation.linearEquivMapExtendScalars
      p'.asIdeal.primeCompl).symm.map_eq_zero_iff.mp (Subsingleton.eq_zero _)

Premises used: LinearEquiv.symm, Module.FinitePresentation.linearEquivMapExtendScalars, LinearEquiv.map_eq_zero_iff, Iff.mp, Ideal.primeCompl, Subsingleton.eq_zero, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Regular.LinearMap
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R M
inst_7 : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h_1 : Nontrivial M
h : ∀ (r : R) (_ : Membership.mem (γ := Ideal R) (annihilator R N) r), ¬IsSMulRegular M r
p : Ideal R
pass : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R M) p
hp : annihilator R N ≤ p
h_2 : p.IsPrime := ⋯
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
loc_ne_zero : Nontrivial (LocalizedModule p'.asIdeal.primeCompl N)
Rₚ : Type u_1 := Localization.AtPrime p
Nₚ : Type (max u_1 u_3) := LocalizedModule.AtPrime p'.asIdeal N
Mₚ : Type (max u_1 u_2) := LocalizedModule.AtPrime p'.asIdeal M
Nₚ' : Type (max u_1 u_3) :=
  Nₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
ntr : Nontrivial Nₚ'
Mₚ' : Type (max u_1 u_2) :=
  Mₚ ⧸
    HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Mₚ) (maximalIdeal (Localization.AtPrime p)) ⊤
x_1 : Module p.ResidueField Nₚ' := instQuotientIdealSubmoduleHSMulTop Nₚ (maximalIdeal (Localization.AtPrime p))
this_1 :
  Ideal.IsPrime.{u_1} (α := Localization.AtPrime p) (maximalIdeal (Localization.AtPrime p)) ∧
    ∃ (x : LocalizedModule.AtPrime p M),
      Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
        (Submodule.colon (M := LocalizedModule.AtPrime p M) ⊥ {x})
x : LocalizedModule.AtPrime p M
this : Nontrivial (Dual p.ResidueField Nₚ')
g : Dual p.ResidueField Nₚ'
hg : g ≠ 0
to_res' : Nₚ' →ₗ[Rₚ] p.ResidueField :=
  let __spread.0 := g;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
to_res : Nₚ →ₗ[Rₚ] p.ResidueField :=
  to_res' ∘ₗ
    (HSMul.hSMul (α := Ideal (Localization.AtPrime p)) (β := Submodule Rₚ Nₚ) (maximalIdeal (Localization.AtPrime p))
        ⊤).mkQ
hx :
  Eq.{u_1 + 1} (α := Ideal (Localization.AtPrime p)) (maximalIdeal (Localization.AtPrime p))
    (ker (toSpanSingleton (Localization.AtPrime p) (LocalizedModule.AtPrime p M) x))
i : p.ResidueField →ₗ[Rₚ] Mₚ := Submodule.liftQ (maximalIdeal (Localization.AtPrime p)) (toSpanSingleton Rₚ Mₚ x) ⋯
inj1 : Function.Injective (α := p.ResidueField) (β := Mₚ) (⇑i : (a : p.ResidueField) → Mₚ)
f : Nₚ →ₗ[Rₚ] Mₚ := i ∘ₗ to_res
h_3 : FinitePresentation R N := ⋯
f_ne0 : Subsingleton (N →ₗ[R] M)
⊢ f = 0

Tactic:
exact (Module.FinitePresentation.linearEquivMapExtendScalars
      p'.asIdeal.primeCompl).symm.map_eq_zero_iff.mp (Subsingleton.eq_zero _)

Premises used: LinearEquiv.symm, Module.FinitePresentation.linearEquivMapExtendScalars, LinearEquiv.map_eq_zero_iff, Iff.mp, Ideal.primeCompl, Subsingleton.eq_zero, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Regular.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 : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)
⊢ Subsingleton.{v + 1} (M ⟶ M)

Tactic:
have : Subsingleton (M ⟶ M) := Ext.homEquiv₀.subsingleton_congr.mp (h M ‹_›)
-- Module: Mathlib.RingTheory.Regular.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 : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)
this : Subsingleton.{v + 1} (M ⟶ M)
⊢ Limits.IsZero M

Tactic:
have : Limits.IsZero M := (Limits.IsZero.iff_id_eq_zero M).mpr (Subsingleton.eq_zero (𝟙 M))
-- Module: Mathlib.RingTheory.Regular.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 : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)
this_1 : Subsingleton.{v + 1} (M ⟶ M)
this : Limits.IsZero M
⊢ HasProjectiveDimensionLT M 0

Tactic:
this.hasProjectiveDimensionLT_zero

Premises used: CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero
-- Module: Mathlib.RingTheory.Regular.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 : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)
this_1 : Subsingleton.{v + 1} (M ⟶ M)
this : Limits.IsZero M
⊢ HasProjectiveDimensionLT M 0

Tactic:
exact this.hasProjectiveDimensionLT_zero

Premises used: CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L n)),
    HasProjectiveDimensionLT M n
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))
succ :
  ∀ (w : Type v) (w_1 : AddCommGroup w) (w_2 : Module R w),
    Free R w →
      Module.Finite R w →
        ∀ (f : w →ₗ[R] (↑M : Type v))
          (surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))),
          HasProjectiveDimensionLT M (n + 1)
⊢ HasProjectiveDimensionLT M (n + 1)

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

Premises used: Module.exists_finite_presentation, ModuleCat.carrier
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L n)),
    HasProjectiveDimensionLT M n
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
⊢ S.ShortExact

Tactic:
have hS : S.ShortExact := LinearMap.shortExact_shortComplexKer surjf
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
simp : CategoryTheory.Projective M
⊢ HasProjectiveDimensionLT M (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]

Premises used: zero_add, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
⊢ Subsingleton.{v + 1} (Ext M S.X₁ 1)

Tactic:
have : Subsingleton (Ext M S.X₁ 1) := h S.X₁ inferInstance
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
rcases : ∀ (f' : Ext M S.X₂ 0) (hf' : f'.comp (Ext.mk₀ S.g) ⋯ = Ext.mk₀ (𝟙 M)), CategoryTheory.Projective M
⊢ CategoryTheory.Projective M

Tactic:
rcases Ext.covariant_sequence_exact₃ M hS (Ext.mk₀ (𝟙 M)) (zero_add 1)
        (Subsingleton.eq_zero _) with ⟨f', hf'⟩

Premises used: CategoryTheory.CategoryStruct.id, zero_add, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃, Subsingleton.eq_zero, OfNat.ofNat, CategoryTheory.Abelian.Ext.mk₀
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
hf' : f'.comp (Ext.mk₀ S.g) ⋯ = Ext.mk₀ (𝟙 M)
rcases : ∀ (f : M ⟶ S.X₂) (hf : Ext.mk₀ f = f'), CategoryTheory.Projective M
⊢ CategoryTheory.Projective M

Tactic:
rcases (Ext.mk₀_bijective M S.X₂).2 f' with ⟨f, hf⟩

Premises used: And.right, CategoryTheory.Abelian.Ext.mk₀_bijective, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f_1 : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f_1 : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f_1.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
hf' : f'.comp (Ext.mk₀ S.g) ⋯ = Ext.mk₀ (𝟙 M)
f : M ⟶ S.X₂
hf : Ext.mk₀ f = f'
⊢ f ≫ S.g = 𝟙 M

Tactic:
rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'

Premises used: Function.Injective.eq_iff, And.left, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀, CategoryTheory.Abelian.Ext.mk₀_bijective
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f_1 : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f_1 : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f_1.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
hf' : f'.comp (Ext.mk₀ S.g) ⋯ = Ext.mk₀ (𝟙 M)
f : M ⟶ S.X₂
hf : Ext.mk₀ f = f'
hf'₁ : f ≫ S.g = 𝟙 M
⊢ Ext.mk₀ f = f'

Tactic:
rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'

Premises used: Function.Injective.eq_iff, And.left, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀, CategoryTheory.Abelian.Ext.mk₀_bijective
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f_1 : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f_1 : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f_1.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
f : M ⟶ S.X₂
hf' : f ≫ S.g = 𝟙 M
hf : Ext.mk₀ f = f'
⊢ CategoryTheory.Projective M

Tactic:
(Retract.mk f S.g hf').projective

Premises used: CategoryTheory.Retract.projective, CategoryTheory.Retract.mk, CategoryTheory.ShortComplex.g
-- Module: Mathlib.RingTheory.Regular.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)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f_1 : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f_1 : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f_1.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)),
    HasProjectiveDimensionLT M 0
h :
  ∀ (L : ModuleCat.{v, u} R),
    Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (HAdd.hAdd (α := ℕ) 0 1))
this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
f : M ⟶ S.X₂
hf' : f ≫ S.g = 𝟙 M
hf : Ext.mk₀ f = f'
⊢ CategoryTheory.Projective M

Tactic:
exact (Retract.mk f S.g hf').projective

Premises used: CategoryTheory.Retract.projective, CategoryTheory.Retract.mk, CategoryTheory.ShortComplex.g
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
rw : HasProjectiveDimensionLT S.X₁ (n + 1)
⊢ HasProjectiveDimensionLT M (n + 1 + 1)

Tactic:
rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]

Premises used: CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, inferInstance
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
L : ModuleCat.{v, u} R
⊢ ∀ (m : ℕ), Subsingleton.{v + 1} (Ext S.X₂ L (m + 1))

Tactic:
have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
L : ModuleCat.{v, u} R
this : ∀ (m : ℕ), Subsingleton.{v + 1} (Ext S.X₂ L (m + 1))
⊢ HAdd.hAdd (α := ℕ) 1 3 ≤ 5

Tactic:
decide
-- Module: Mathlib.RingTheory.Regular.ProjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n_1 : ℕ
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
w : Type v
w_1 : AddCommGroup w
w_2 : Module R w
w_3 : Free R w
w_4 : Module.Finite R w
f : w →ₗ[R] (↑M : Type v)
surjf : Function.Surjective (α := w) (β := (↑M : Type v)) (⇑f : (a : w) → (↑M : Type v))
S : ShortComplex (ModuleCat.{v, u} R) := f.shortComplexKer
hS : S.ShortExact
n : ℕ
hn :
  ∀ (M : ModuleCat.{v, u} R) [Module.Finite.{u, v} R (↑M : Type v)]
    (h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1))),
    HasProjectiveDimensionLT M (n + 1)
h : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L (n + 1 + 1))
L : ModuleCat.{v, u} R
this : ∀ (m : ℕ), Subsingleton.{v + 1} (Ext S.X₂ L (m + 1))
⊢ IsIso (X := AddCommGrpCat.of (Ext S.X₁ L (n + 1))) (AddCommGrpCat.ofHom (Ext.precomp hS.extClass L ⋯))

Tactic:
have isi : IsIso (AddCommGrpCat.ofHom (hS.extClass.precomp L (add_comm 1 _))) :=
          (Ext.contravariantSequence_exact hS L (n + 1) (n + 2)
            (add_comm 1 _)).isIso_map' 1 (by decide)
              ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_src _)
                ((AddCommGrpCat.of _).isZero_of_subsingleton.eq_zero_of_tgt _)