awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (hypothesis)
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
⊢ False
have f_ne0 : f ≠ 0
Tactic: have f_ne0 : f ≠ 0 := by
      intro eq0
      absurd hg
      apply LinearMap.ext
      intro np'
      induction np' using Submodule.Quotient.induction_on with | _ np
      change to_res np = 0
      apply inj1
      change f np = _
      simp [eq0]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
f_ne0 : f ≠ 0
⊢ False
have inr : ¬Subsingleton (N →ₗ[R] M)
Tactic: absurd hom0
-- Lean 4 proof step from Mathlib.RingTheory.Regular.LinearMap (goal)
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
f_ne0 : f ≠ 0
h_3 : FinitePresentation R N := ⋯
⊢ ¬Subsingleton (N →ₗ[R] M)
have inr : ∀ (f_ne0 : Subsingleton (N →ₗ[R] M)), f = 0
Tactic: contrapose f_ne0
Cleared hypotheses: f_ne0
-- Lean 4 proof step from Mathlib.RingTheory.Regular.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 : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext M L 0)
⊢ HasProjectiveDimensionLT M 0
have this : Subsingleton.{v + 1} (M ⟶ M)
Tactic: have : Subsingleton (M ⟶ M) := Ext.homEquiv₀.subsingleton_congr.mp (h M ‹_›)
-- Lean 4 proof step from Mathlib.RingTheory.Regular.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 : ∀ (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)
⊢ HasProjectiveDimensionLT M 0
have this₁ : Limits.IsZero M
Tactic: have : Limits.IsZero M := (Limits.IsZero.iff_id_eq_zero M).mpr (Subsingleton.eq_zero (𝟙 M))
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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))
⊢ HasProjectiveDimensionLT M (n + 1)
have 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)
Tactic: rcases Module.exists_finite_presentation R M with ⟨_, _, _, _, _, f, surjf⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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
⊢ HasProjectiveDimensionLT M (n + 1)
have hS : S.ShortExact
Tactic: have hS : S.ShortExact := LinearMap.shortExact_shortComplexKer surjf
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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))
⊢ HasProjectiveDimensionLT M (HAdd.hAdd (α := ℕ) 0 1)
have simp : CategoryTheory.Projective M
Tactic: simp only [zero_add, ← projective_iff_hasProjectiveDimensionLT_one]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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))
⊢ CategoryTheory.Projective M
have this : Subsingleton.{v + 1} (Ext M S.X₁ 1)
Tactic: have : Subsingleton (Ext M S.X₁ 1) := h S.X₁ inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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)
⊢ CategoryTheory.Projective M
have rcases : ∀ (f' : Ext M S.X₂ 0) (hf' : f'.comp (Ext.mk₀ S.g) sorry = Ext.mk₀ (𝟙 M)), CategoryTheory.Projective M
Tactic: rcases Ext.covariant_sequence_exact₃ M hS (Ext.mk₀ (𝟙 M)) (zero_add 1)
        (Subsingleton.eq_zero _) with ⟨f', hf'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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)
⊢ CategoryTheory.Projective M
have rcases : ∀ (f : M ⟶ S.X₂) (hf : Ext.mk₀ f = f'), CategoryTheory.Projective M
Tactic: rcases (Ext.mk₀_bijective M S.X₂).2 f' with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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'
⊢ CategoryTheory.Projective M
have hf'₁ : f ≫ S.g = 𝟙 M
Tactic: rw [← hf, Ext.mk₀_comp_mk₀, (Ext.mk₀_bijective _ _).1.eq_iff] at hf'
Cleared hypotheses: hf', hf
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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))
⊢ HasProjectiveDimensionLT M (n + 1 + 1)
have rw : HasProjectiveDimensionLT S.X₁ (n + 1)
Tactic: rw [hS.hasProjectiveDimensionLT_X₃_iff n inferInstance]
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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
⊢ Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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))
⊢ Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))
have isi : IsIso (X := AddCommGrpCat.of (Ext S.X₁ L (n + 1))) (AddCommGrpCat.ofHom (Ext.precomp hS.extClass L sorry))
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 _)
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (hypothesis)
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))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)
have this : ∀ (L : ModuleCat.{v, u} R), Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))
Tactic: have (L : ModuleCat.{v} R) : Subsingleton (Ext S.X₁ L (n + 1)) ↔
        Subsingleton (Ext M L (n + 2)) := by
        have (m : ℕ) : Subsingleton (Ext S.X₂ L (m + 1)) := Ext.subsingleton_of_projective S.X₂ L m
        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 _)
        exact (asIso (AddCommGrpCat.ofHom (hS.extClass.precomp L
          (add_comm 1 _)))).addCommGroupIsoToAddEquiv.subsingleton_congr
-- Lean 4 proof step from Mathlib.RingTheory.Regular.ProjectiveDimension (goal)
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))
this : ∀ (L : ModuleCat.{v, u} R), Subsingleton.{v + 1} (Ext S.X₁ L (n + 1)) ↔ Subsingleton.{v + 1} (Ext M L (n + 2))
⊢ HasProjectiveDimensionLT S.X₁ (n + 1)
have apply : ∀ (L : ModuleCat.{v, u} R), Module.Finite.{u, v} R (↑L : Type v) → Subsingleton.{v + 1} (Ext S.X₁ L (n + 1))
Tactic: apply hn S.X₁