awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasProjectiveDimensionLT.{v, u} X 0
this : HasExt C := ⋯
⊢ LE.le (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasProjectiveDimensionLT.{v, u} X 0
this : HasExt C := ⋯
⊢ Eq (α := Ext X X 0) ((Equiv.symm Ext.homEquiv₀ : (a : X ⟶ X) → Ext X X 0) (𝟙 X) : Ext X X 0)
    ((Equiv.symm Ext.homEquiv₀ : (a : X ⟶ X) → Ext X X 0) 0 : Ext X X 0)

Tactic:
simpa only [Ext.homEquiv₀_symm_apply, Ext.mk₀_zero]
    using Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT _ 0 (by rfl)

Premises used: CategoryTheory.Abelian.Ext.mk₀_zero, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT, OfNat.ofNat, CategoryTheory.Abelian.Ext.homEquiv₀_symm_apply
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ HasProjectiveDimensionLT.{v, u} X 0 ↔ IsZero.{v, u} X

Tactic:
⟨fun _ ↦ isZero_of_hasProjectiveDimensionLT_zero X, fun h ↦ h.hasProjectiveDimensionLT_zero⟩

Premises used: CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero, CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero, Iff.intro
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n m : ℕ
h : n ≤ m
inst_2 : HasProjectiveDimensionLT.{v, u} X n
this : HasExt C := ⋯
rw : ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} X m

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n m : ℕ
h : n ≤ m
inst_2 : HasProjectiveDimensionLT.{v, u} X n
this : HasExt C := ⋯
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ n ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n m : ℕ
h : n ≤ m
inst_2 : HasProjectiveDimensionLT.{v, u} X n
this : HasExt C := ⋯
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Tactic:
exact e.eq_zero_of_hasProjectiveDimensionLT n (by lia)

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} X n
k : ℕ
⊢ n ≤ n + k

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} X n
k : ℕ
⊢ n ≤ k + n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} X n
⊢ HasProjectiveDimensionLT.{v, u} X n.succ

Tactic:
inferInstanceAs (HasProjectiveDimensionLT X (n + 1))

Premises used: _private.0.CategoryTheory.instHasProjectiveDimensionLTSucc._proof_1
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Projective.{v, u} X
this : HasExt C := ⋯
rw : ∀ (i : ℕ), 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} X 1

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Projective.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 1 ≤ i
Y : C
e : Ext X Y i
zero : ∀ (hi : LE.le (α := ℕ) 1 0) (e : Ext X Y 0), e = 0
succ : ∀ (i : ℕ) (hi : 1 ≤ i + 1) (e : Ext X Y (i + 1)), e = 0
⊢ e = 0

Tactic:
obtain _ | i := i
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Projective.{v, u} X
this : HasExt C := ⋯
Y : C
hi : LE.le (α := ℕ) 1 0
e : Ext X Y 0
⊢ e = 0

Tactic:
simp at hi
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Projective.{v, u} X
this : HasExt C := ⋯
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext X Y (i + 1)
⊢ e = 0

Tactic:
e.eq_zero_of_projective

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_projective
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : Projective.{v, u} X
this : HasExt C := ⋯
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext X Y (i + 1)
⊢ e = 0

Tactic:
exact e.eq_zero_of_projective

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_projective
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : Projective.{v, u} X
⊢ LE.le (α := ℕ) 1 1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
refine :
  ∀ (h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)) {E X_1 : C} (f : X ⟶ X_1) (g : E ⟶ X_1),
    Epi g → ∃ (f' : X ⟶ E), f' ≫ g = f
⊢ Projective.{v, u} X ↔ ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)

Tactic:
refine ⟨fun h ↦ HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl),
    fun h ↦ ⟨fun f g _ ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)
E X_1 : C
f : X ⟶ X_1
g : E ⟶ X_1
h_1 : Epi g
⊢ Eq.{w + 1} (α :=
    Ext.{w, v, u} X (ShortComplex.X₁ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }) 1)
    (Ext.comp (Ext.mk₀ f) (ShortComplex.ShortExact.extClass ⋯) ⋯) 0

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)
E X_1 : C
f : X ⟶ X_1
g : E ⟶ X_1
h_1 : Epi g
obtain :
  ∀ (φ : Ext.{w, v, u} X (ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }) 0)
    (hφ :
      φ.comp
          (Ext.mk₀
            (ShortComplex.g
              { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ : ShortComplex.{v, u} C }))
          ⋯ =
        Ext.mk₀ f),
    ∃ (f' : X ⟶ E), f' ≫ g = f
⊢ ∃ (f' : X ⟶ E), f' ≫ g = f

Tactic:
obtain ⟨φ, hφ⟩ :=
    Ext.covariant_sequence_exact₃ _ { exact := ShortComplex.exact_kernel g }
      (Ext.mk₀ f) (zero_add 1) (by subsingleton)

Premises used: CategoryTheory.ShortComplex.exact_kernel, zero_add, CategoryTheory.Abelian.Ext.covariant_sequence_exact₃, CategoryTheory.ShortComplex.ShortExact.mk, OfNat.ofNat, CategoryTheory.Abelian.Ext.mk₀
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)
E X_1 : C
f : X ⟶ X_1
g : E ⟶ X_1
h_1 : Epi g
φ : Ext.{w, v, u} X (ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }) 0
hφ :
  φ.comp
      (Ext.mk₀
        (ShortComplex.g
          { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ : ShortComplex.{v, u} C }))
      ⋯ =
    Ext.mk₀ f
obtain :
  ∀ (φ : X ⟶ ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ })
    (hφ :
      Eq.{w + 1} (α :=
        Ext.{w, v, u} X (ShortComplex.X₃ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }) 0)
        (Ext.comp
          ((Equiv.symm Ext.homEquiv₀ :
              (a : X ⟶ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }.X₂) →
                Ext X { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }.X₂ 0)
            φ)
          (Ext.mk₀
            (ShortComplex.g
              { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ : ShortComplex.{v, u} C }))
          ⋯)
        (Ext.mk₀ f)),
    ∃ (f' : X ⟶ E), f' ≫ g = f
⊢ ∃ (f' : X ⟶ E), f' ≫ g = f

Tactic:
obtain ⟨φ, rfl⟩ := Ext.homEquiv₀.symm.surjective φ

Premises used: Equiv.surjective, Equiv.symm, CategoryTheory.Abelian.Ext.homEquiv₀, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)
E X_1 : C
f : X ⟶ X_1
g : E ⟶ X_1
h_1 : Epi g
φ : X ⟶ ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }
hφ :
  Eq.{w + 1} (α :=
    Ext.{w, v, u} X (ShortComplex.X₃ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }) 0)
    (Ext.comp
      ((Equiv.symm Ext.homEquiv₀ :
          (a : X ⟶ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }.X₂) →
            Ext X { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }.X₂ 0)
        φ)
      (Ext.mk₀
        (ShortComplex.g
          { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ : ShortComplex.{v, u} C }))
      ⋯)
    (Ext.mk₀ f)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X X_1 0)
    ((Equiv.symm Ext.homEquiv₀ : (a : X ⟶ X_1) → Ext X X_1 0) (φ ≫ g) : Ext.{w, v, u} X X_1 0)
    ((Equiv.symm Ext.homEquiv₀ : (a : X ⟶ X_1) → Ext X X_1 0) f : Ext.{w, v, u} X X_1 0)

Tactic:
simpa using hφ
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
h : ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)
E X_1 : C
f : X ⟶ X_1
g : E ⟶ X_1
h_1 : Epi g
φ : X ⟶ ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }
hφ :
  Eq.{w + 1} (α :=
    Ext.{w, v, u} X (ShortComplex.X₃ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }) 0)
    (Ext.comp
      ((Equiv.symm Ext.homEquiv₀ :
          (a : X ⟶ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }.X₂) →
            Ext X { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ }.X₂ 0)
        φ)
      (Ext.mk₀
        (ShortComplex.g
          { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := ⋯ : ShortComplex.{v, u} C }))
      ⋯)
    (Ext.mk₀ f)
⊢ ∃ (f' : X ⟶ E), f' ≫ g = f

Tactic:
exact ⟨φ, Ext.homEquiv₀.symm.injective (by simpa using hφ)⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
this : HasExt C := ⋯
h : HasProjectiveDimensionLT.{v, u} X 1
⊢ LE.le (α := ℕ) 1 1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
this : HasExt C := ⋯
⊢ Projective.{v, u} X ↔ HasProjectiveDimensionLT.{v, u} X 1

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ projective_iff_subsingleton_ext_one.2
    (HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ Projective.{v, u} X ↔ HasProjectiveDimensionLE.{v, u} X 0

Tactic:
projective_iff_hasProjectiveDimensionLT_one

Premises used: CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} X 1
⊢ Projective.{v, u} X

Tactic:
projective_iff_hasProjectiveDimensionLT_one.mpr ‹_›

Premises used: Iff.mpr, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} Y n
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} X n

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
h : Retract X Y
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} Y n
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
rw : Ext.comp (Ext.mk₀ (𝟙 X)) x ⋯ = 0
rw₁ : Ext.comp (Ext.mk₀ (h.i ≫ h.r)) x ⋯ = 0
rw₂ : Ext.comp (Ext.comp (Ext.mk₀ h.i) (Ext.mk₀ h.r) ⋯) x ⋯ = 0
rw₃ : Ext.comp (Ext.mk₀ h.i) (Ext.comp (Ext.mk₀ h.r) x ⋯) ⋯ = 0
rw₄ : Eq (α := Ext X T i) (Ext.comp (Ext.mk₀ h.i) 0 ⋯) 0
rw₅ rw₆ : Eq (α := Ext X T i) 0 0
⊢ x = 0

Tactic:
rw [← x.mk₀_id_comp, ← h.retract, ← Ext.mk₀_comp_mk₀,
    Ext.comp_assoc_of_second_deg_zero,
    ((Ext.mk₀ h.r).comp x (zero_add i)).eq_zero_of_hasProjectiveDimensionLT n hi,
    Ext.comp_zero]

Premises used: CategoryTheory.Abelian.Ext.mk₀_id_comp, CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.Retract.retract, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, zero_add, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Retract.r, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT, CategoryTheory.Abelian.Ext.mk₀
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X X' : C
e : X ≅ X'
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} X n
⊢ HasProjectiveDimensionLT.{v, u} X' n

Tactic:
e.symm.retract.hasProjectiveDimensionLT n

Premises used: CategoryTheory.Iso.retract, CategoryTheory.Iso.symm, CategoryTheory.Retract.hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ n
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₂ Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} S.X₂ n

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ n
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
obtain : ∀ (x₃ : Ext S.X₃ Y i), Ext.comp (Ext.mk₀ S.g) x₃ ⋯ = 0
⊢ x₂ = 0

Tactic:
obtain ⟨x₃, rfl⟩ := Ext.contravariant_sequence_exact₂ hS _ x₂
    (Ext.eq_zero_of_hasProjectiveDimensionLT _ n hi)

Premises used: CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ n
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext S.X₃ Y i
rw : Eq (α := Ext S.X₂ Y i) (Ext.comp (Ext.mk₀ S.g) 0 ⋯) 0
rw₁ rw₂ : Eq (α := Ext S.X₂ Y i) 0 0
⊢ Ext.comp (Ext.mk₀ S.g) x₃ ⋯ = 0

Tactic:
rw [x₃.eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n + 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₃ Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
hi : n + 1 ≤ 0
Y : C
x₃ : Ext S.X₃ Y 0
⊢ x₃ = 0

Tactic:
simp at hi
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext S.X₃ Y (i + 1)
succ : ∀ (x₁ : Ext S.X₁ Y i), Ext.comp hS.extClass x₁ ⋯ = 0
⊢ x₃ = 0

Tactic:
obtain ⟨x₁, rfl⟩ := Ext.contravariant_sequence_exact₃ hS _ x₃
      (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) hi) (add_comm _ _)

Premises used: add_comm, HAdd.hAdd, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT, OfNat.ofNat, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext S.X₁ Y i
⊢ n ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT.{v, u} S.X₁ n
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext S.X₁ Y i
succ : Eq (α := Ext S.X₃ Y (i + 1)) (Ext.comp hS.extClass 0 ⋯) 0
succ₁ succ₂ : Eq (α := Ext S.X₃ Y (i + 1)) 0 0
⊢ Ext.comp hS.extClass x₁ ⋯ = 0

Tactic:
rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)
this : HasExt C := ⋯
rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₁ Y i), e = 0
⊢ HasProjectiveDimensionLT.{v, u} S.X₁ n

Tactic:
rw [hasProjectiveDimensionLT_iff]

Premises used: CategoryTheory.hasProjectiveDimensionLT_iff
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext S.X₁ Y i
⊢ n + 1 ≤ i + 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext S.X₁ Y i
obtain : ∀ (x₂ : Ext S.X₂ Y i), Ext.comp (Ext.mk₀ S.f) x₂ ⋯ = 0
⊢ x₁ = 0

Tactic:
obtain ⟨x₂, rfl⟩ := Ext.contravariant_sequence_exact₁ hS _ x₁ (add_comm _ _)
    (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) (by lia))

Premises used: add_comm, HAdd.hAdd, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT, CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁, OfNat.ofNat, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ n ≤ i

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT.{v, u} S.X₂ n
h₃ : HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)
this : HasExt C := ⋯
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
rw : Eq (α := Ext S.X₁ Y i) (Ext.comp (Ext.mk₀ S.f) 0 ⋯) 0
rw₁ rw₂ : Eq (α := Ext S.X₁ Y i) 0 0
⊢ Ext.comp (Ext.mk₀ S.f) x₂ ⋯ = 0

Tactic:
rw [x₂.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]

Premises used: CategoryTheory.Abelian.Ext.comp_zero, CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
n : ℕ
h₂ : Projective.{v, u} S.X₂
⊢ HasProjectiveDimensionLT.{v, u} S.X₃ (n + 2) ↔ HasProjectiveDimensionLT.{v, u} S.X₁ (n + 1)

Tactic:
⟨fun _ ↦ hS.hasProjectiveDimensionLT_X₁ (n + 1) inferInstance inferInstance,
    fun _ ↦ hS.hasProjectiveDimensionLT_X₃ (n + 1) inferInstance inferInstance⟩

Premises used: CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁, inferInstance, HAdd.hAdd, Iff.intro, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
n : ℕ
inst_2 : HasProjectiveDimensionLT.{v, u} X n
inst_3 : HasProjectiveDimensionLT.{v, u} Y n
⊢ HasProjectiveDimensionLT.{v, u} (biprod.{v, u} X Y) n

Tactic:
(ShortComplex.Splitting.ofHasBinaryBiproduct X Y).shortExact.hasProjectiveDimensionLT_X₂ n ‹_› ‹_›

Premises used: CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct, CategoryTheory.ShortComplex.Splitting.shortExact, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (k : ℕ), d = n + k → e = 0
i : ℕ
hi : n ≤ i
Y : C
e : Ext.{w, v, u} X Y i
obtain : ∀ (k : ℕ) (hi : n ≤ n + k) (e : Ext.{w, v, u} X Y (n + k)), e = 0
⊢ e = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext.{w, v, u} X Y (n + k)
⊢ e = 0

Tactic:
this e k rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton.{w + 1} (Ext.{w, v, u} X Y n)
this : ∀ ⦃d : ℕ⦄ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y d) (k : ℕ), d = n + k → e = 0
Y : C
k : ℕ
hi : n ≤ n + k
e : Ext.{w, v, u} X Y (n + k)
⊢ e = 0

Tactic:
exact this e k rfl

Premises used: rfl