awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
inv :
  (Φ.colon Ψ).r.obj X ⟶
    Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯)
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
have mpr : NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ inv =
  𝟙 (Φ.obj (P := Over.isMono (𝟭 C)).left.obj X)
Tactic: refine ⟨inv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Colon (goal)
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
Φ Ψ : Preradical.{u_2, u_1} C
X : C
h : IsZero.{u_2, u_1} (Ψ.r.obj (Φ.quotient.obj X))
inv :
  (Φ.colon Ψ).r.obj X ⟶
    Cone.pt (F := parallelPair (Y := Φ.quotient.obj X) (NatTrans.app Φ.π X) 0) (KernelFork.ofι (Φ.ι.app X) ⋯)
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
mpr :
  NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X ≫ inv =
    𝟙 (Φ.obj (P := Over.isMono (𝟭 C)).left.obj X)
⊢ IsIso (Y := (Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
    (NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X)
have mpr₁ : inv ≫ NatTrans.app (Over.Hom.left (InducedCategory.Hom.hom (Φ.toColon Ψ))) X =
  𝟙 ((Φ.colon Ψ).obj (P := Over.isMono (𝟭 C)).left.obj X)
Tactic: refine ⟨inv, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Radical (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Preradical.{v_1, u_1} C
⊢ isRadical C Φ ↔ IsZero (Φ.quotient ⋙ Φ.r)
have rw : IsIso (Y := Φ.colon Φ) (Φ.toColon Φ) ↔ IsZero (Φ.quotient ⋙ Φ.r)
Tactic: rw [isRadical_iff_isIso, isIso_toColon_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Radical (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Preradical.{v_1, u_1} C
rw : IsIso (Y := Φ.colon Φ) (Φ.toColon Φ) ↔ IsZero (Φ.quotient ⋙ Φ.r)
⊢ isRadical C Φ ↔ IsZero (Φ.quotient ⋙ Φ.r)
have rw₁ : IsZero (Φ.quotient ⋙ Φ.r) ↔ IsZero (Φ.quotient ⋙ Φ.r)
Tactic: rw [isRadical_iff_isIso, isIso_toColon_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Preradical.Radical (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
Φ : Radical.{v_1, u_1} C
⊢ IsZero (Φ.obj (P := Preradical.isRadical C).quotient ⋙ Φ.obj (P := Preradical.isRadical C).r)
have rw : IsIso (Y := Φ.obj (P := Preradical.isRadical C).colon (Φ.obj (P := Preradical.isRadical C)))
  (Φ.obj (P := Preradical.isRadical C).toColon (Φ.obj (P := Preradical.isRadical C)))
Tactic: rw [← Preradical.isRadical_iff_isZero, Preradical.isRadical_iff_isIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : Projective.{v, u} P
⊢ Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
have this : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
Tactic: haveI := (projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj P).mp hP
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Projective.{v, u} P
have rw : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
Tactic: rw [projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
hP : PreservesFiniteColimits.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
have this : Functor.PreservesHomology.{v, u, v, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
Tactic: have := Functor.preservesHomologyOfExact (preadditiveCoyonedaObj P)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : HasProjectiveDimensionLT.{v, u} X n
i : ℕ
hi : n ≤ i
Y : C
this : HasExt C := ⋯
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)
have this₁ : ∀ ⦃Y : C⦄, Subsingleton (Ext X Y i)
Tactic: have := hX.subsingleton' i hi
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext.{w, v, u} X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext X Y i)
have this : Subsingleton.{w + 1} (Ext.{w, v, u} X Y i)
Tactic: have : Subsingleton (Ext X Y i) := ⟨fun e₁ e₂ ↦ by simp only [hX i hi]⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
⊢ HasProjectiveDimensionLT.{v, u} X 0
have rw : ∀ (i : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ e = 0
have rw : Ext.comp (Ext.mk₀ (𝟙 X)) e sorry = 0
Tactic: rw [← e.mk₀_id_comp, hX.eq_of_src (𝟙 X) 0, Ext.mk₀_zero, Ext.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
rw : Ext.comp (Ext.mk₀ (𝟙 X)) e ⋯ = 0
⊢ e = 0
have rw₁ : Eq (α := Ext X Y i) (Ext.comp (Ext.mk₀ 0) e sorry) 0
Tactic: rw [← e.mk₀_id_comp, hX.eq_of_src (𝟙 X) 0, Ext.mk₀_zero, Ext.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
rw : Ext.comp (Ext.mk₀ (𝟙 X)) e ⋯ = 0
rw₁ : Eq (α := Ext X Y i) (Ext.comp (Ext.mk₀ 0) e ⋯) 0
⊢ e = 0
have rw₂ : Eq (α := Ext X Y i) (Ext.comp 0 e sorry) 0
Tactic: rw [← e.mk₀_id_comp, hX.eq_of_src (𝟙 X) 0, Ext.mk₀_zero, Ext.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
hX : IsZero.{v, u} X
this : HasExt C := ⋯
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
rw : Ext.comp (Ext.mk₀ (𝟙 X)) e ⋯ = 0
rw₁ : Eq (α := Ext X Y i) (Ext.comp (Ext.mk₀ 0) e ⋯) 0
rw₂ : Eq (α := Ext X Y i) (Ext.comp 0 e ⋯) 0
⊢ e = 0
have rw₃ : Eq (α := Ext X Y i) 0 0
Tactic: rw [← e.mk₀_id_comp, hX.eq_of_src (𝟙 X) 0, Ext.mk₀_zero, Ext.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ IsZero.{v, u} X
have rw : Eq.{v + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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.{v + 1} (α := X ⟶ X) (𝟙 X) 0
have a : 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: apply Ext.homEquiv₀.symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ HasProjectiveDimensionLT.{v, u} X m
have rw : ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ HasProjectiveDimensionLT.{v, u} X 1
have rw : ∀ (i : ℕ), 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ e = 0
have zero : ∀ (hi : LE.le (α := ℕ) 1 0) (e : Ext X Y 0), e = 0
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi, e
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ e = 0
have succ : ∀ (i : ℕ) (hi : 1 ≤ i + 1) (e : Ext X Y (i + 1)), e = 0
Tactic: obtain _ | i := i
Cleared hypotheses: i, hi, e
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
inst_2 : HasExt.{w, v, u} C
⊢ Projective.{v, u} X ↔ ∀ ⦃Y : C⦄, Subsingleton.{w + 1} (Ext.{w, v, u} X Y 1)
have 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
Tactic: refine ⟨fun h ↦ HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl),
    fun h ↦ ⟨fun f g _ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ ∃ (f' : X ⟶ E), f' ≫ g = f
have obtain : ∀ (φ : Ext.{w, v, u} X (ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := sorry }) 0)
  (hφ :
    φ.comp
        (Ext.mk₀
          (ShortComplex.g
            { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := sorry : ShortComplex.{v, u} C }))
        sorry =
      Ext.mk₀ 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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ ∃ (f' : X ⟶ E), f' ≫ g = f
have obtain : ∀ (φ : X ⟶ ShortComplex.X₂ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := sorry })
  (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 := sorry }) 0)
      (Ext.comp
        ((Equiv.symm Ext.homEquiv₀ :
            (a : X ⟶ { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := sorry }.X₂) →
              Ext X { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := sorry }.X₂ 0)
          φ)
        (Ext.mk₀
          (ShortComplex.g
            { X₁ := kernel g, X₂ := E, X₃ := X_1, f := kernel.ι g, g := g, zero := sorry : ShortComplex.{v, u} C }))
        sorry)
      (Ext.mk₀ f)),
  ∃ (f' : X ⟶ E), f' ≫ g = f
Tactic: obtain ⟨φ, rfl⟩ := Ext.homEquiv₀.symm.surjective φ
Cleared hypotheses: φ, hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ HasProjectiveDimensionLT.{v, u} X n
have rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x = 0
have rw : Ext.comp (Ext.mk₀ (𝟙 X)) x sorry = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x = 0
have rw₁ : Ext.comp (Ext.mk₀ (h.i ≫ h.r)) x sorry = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x = 0
have rw₂ : Ext.comp (Ext.comp (Ext.mk₀ h.i) (Ext.mk₀ h.r) sorry) x sorry = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x = 0
have rw₃ : Ext.comp (Ext.mk₀ h.i) (Ext.comp (Ext.mk₀ h.r) x sorry) sorry = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x = 0
have rw₄ : Eq (α := Ext X T i) (Ext.comp (Ext.mk₀ h.i) 0 sorry) 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x = 0
have rw₅ : Eq (α := Ext X T i) 0 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ HasProjectiveDimensionLT.{v, u} S.X₂ n
have rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₂ Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x₂ = 0
have obtain : ∀ (x₃ : Ext S.X₃ Y i), Ext.comp (Ext.mk₀ S.g) x₃ sorry = 0
Tactic: obtain ⟨x₃, rfl⟩ := Ext.contravariant_sequence_exact₂ hS _ x₂
    (Ext.eq_zero_of_hasProjectiveDimensionLT _ n hi)
Cleared hypotheses: x₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ Ext.comp (Ext.mk₀ S.g) x₃ ⋯ = 0
have rw : Eq (α := Ext S.X₂ Y i) (Ext.comp (Ext.mk₀ S.g) 0 sorry) 0
Tactic: rw [x₃.eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ Ext.comp (Ext.mk₀ S.g) x₃ ⋯ = 0
have rw₁ : Eq (α := Ext S.X₂ Y i) 0 0
Tactic: rw [x₃.eq_zero_of_hasProjectiveDimensionLT n hi, Ext.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ HasProjectiveDimensionLT.{v, u} S.X₃ (n + 1)
have rw : ∀ (i : ℕ), n + 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₃ Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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)
⊢ x₃ = 0
have succ : ∀ (x₁ : Ext S.X₁ Y i), Ext.comp hS.extClass x₁ sorry = 0
Tactic: obtain ⟨x₁, rfl⟩ := Ext.contravariant_sequence_exact₃ hS _ x₃
      (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) hi) (add_comm _ _)
Cleared hypotheses: x₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ Ext.comp hS.extClass x₁ ⋯ = 0
have succ : Eq (α := Ext S.X₃ Y (i + 1)) (Ext.comp hS.extClass 0 sorry) 0
Tactic: rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ Ext.comp hS.extClass x₁ ⋯ = 0
have succ₁ : Eq (α := Ext S.X₃ Y (i + 1)) 0 0
Tactic: rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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 := ⋯
⊢ HasProjectiveDimensionLT.{v, u} S.X₁ n
have rw : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext S.X₁ Y i), e = 0
Tactic: rw [hasProjectiveDimensionLT_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ x₁ = 0
have obtain : ∀ (x₂ : Ext S.X₂ Y i), Ext.comp (Ext.mk₀ S.f) x₂ sorry = 0
Tactic: obtain ⟨x₂, rfl⟩ := Ext.contravariant_sequence_exact₁ hS _ x₁ (add_comm _ _)
    (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) (by lia))
Cleared hypotheses: x₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ Ext.comp (Ext.mk₀ S.f) x₂ ⋯ = 0
have rw : Eq (α := Ext S.X₁ Y i) (Ext.comp (Ext.mk₀ S.f) 0 sorry) 0
Tactic: rw [x₂.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ Ext.comp (Ext.mk₀ S.f) x₂ ⋯ = 0
have rw₁ : Eq (α := Ext S.X₁ Y i) 0 0
Tactic: rw [x₂.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Dimension (goal)
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
⊢ e = 0
have obtain : ∀ (k : ℕ) (hi : n ≤ n + k) (e : Ext.{w, v, u} X Y (n + k)), e = 0
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hi
Cleared hypotheses: i, hi, e