awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst_1 : Category.{v, u} C
X E X_1 : Type u
f : X ⟶ X_1
e : E ⟶ X_1
h : Epi e
he :
  Function.Surjective (α := (fun (X : Type u) ↦ X) E) (β := (fun (X : Type u) ↦ X) X_1)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) e) : (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
⊢ (↾fun (x : X) ↦
        Exists.choose (p := fun (a : E) ↦
          Eq (α := (fun (X : Type u) ↦ X) X_1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) e : (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
                a :
              (fun (X : Type u) ↦ X) X_1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X_1)
                x :
              (fun (X : Type u) ↦ X) X_1))
          ⋯) ≫
      e =
    f
have h : ∀ (x : X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X) ↦
            Exists.choose (p := fun (a : E) ↦
              Eq (α := (fun (X : Type u) ↦ X) X_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) e :
                      (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
                    a :
                  (fun (X : Type u) ↦ X) X_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X_1)
                    x :
                  (fun (X : Type u) ↦ X) X_1))
              sorry) ≫
          e))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h : Epi g
⊢ ∃ (f' : F.obj P ⟶ E), f' ≫ g = f
have rcases : ∀ (f' : P ⟶ G.obj E) (hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f), ∃ (f' : F.obj P ⟶ E), f' ≫ g = f
Tactic: rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h : Epi g
f' : P ⟶ G.obj E
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ (f' : F.obj P ⟶ E), f' ≫ g = f
have h : (F.map f' ≫ adj.counit.app E) ≫ g = f
Tactic: use F.map f' ≫ adj.counit.app _
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h : Epi g
f' : P ⟶ G.obj E
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E) ≫ g = f
have h : F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X = f
Tactic: rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
⊢ ∃ (f' : P ⟶ E), f' ≫ g = f
have this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
Tactic: haveI := Adjunction.leftAdjoint_preservesColimits.{0, 0} adj
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
⊢ ∃ (f' : P ⟶ E), f' ≫ g = f
have rcases : ∀ (f' : F.obj P ⟶ F.obj E) (hf' : f' ≫ F.map g = F.map f), ∃ (f' : P ⟶ E), f' ≫ g = f
Tactic: rcases (@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E
hf' : f' ≫ F.map g = F.map f
⊢ ∃ (f' : P ⟶ E), f' ≫ g = f
have h : (adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E)) ≫ g = f
Tactic: use adj.unit.app _ ≫ G.map f' ≫ (inv <| adj.unit.app _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesEpimorphisms
P : C
hP : Projective.{v_1, u_1} (F.obj P)
E X : C
g : P ⟶ X
f : E ⟶ X
h : Epi f
⊢ ∃ (f' : P ⟶ E), f' ≫ f = g
have obtain : ∀ (h : F.obj P ⟶ F.obj E) (fac : h ≫ F.map f = F.map g), ∃ (f' : P ⟶ E), f' ≫ f = g
Tactic: obtain ⟨h, fac⟩ := hP.factors (F.map g) (F.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
⊢ EnoughProjectives.{v, u} C ↔ EnoughProjectives.{v', u'} D
have mp : EnoughProjectives.{v, u} C → EnoughProjectives.{v', u'} D
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
mp : EnoughProjectives.{v, u} C → EnoughProjectives.{v', u'} D
⊢ EnoughProjectives.{v, u} C ↔ EnoughProjectives.{v', u'} D
have mpr : EnoughProjectives.{v', u'} D → EnoughProjectives.{v, u} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v, u} C
⊢ EnoughProjectives.{v', u'} D
have mp : ∀ (X : D), Nonempty (ProjectivePresentation.{v', u'} X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v, u} C
X : D
⊢ Nonempty (ProjectivePresentation.{v', u'} X)
have mp : ProjectivePresentation.{v', u'} X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v', u'} D
⊢ EnoughProjectives.{v, u} C
have mpr : ∀ (X : C), Nonempty (ProjectivePresentation.{v, u} X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v', u'} D
X : C
⊢ Nonempty (ProjectivePresentation.{v, u} X)
have mpr : ProjectivePresentation.{v, u} X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
⊢ Projective.{v, u} X
have refine : ∀ {A B : C} (f : X ⟶ B) (e : A ⟶ B), Epi e → ∃ (f' : X ⟶ A), f' ≫ e = f
Tactic: refine Projective.mk (fun {A B} f e _ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
A B : C
f : X ⟶ B
e : A ⟶ B
h_1 : Epi e
⊢ ∃ (f' : X ⟶ A), f' ≫ e = f
have rcases : ∀ (g : Y ⟶ A) (hg : g ≫ e = h.r ≫ f), ∃ (f' : X ⟶ A), f' ≫ e = f
Tactic: rcases p.factors (h.r ≫ f) e with ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
A B : C
f : X ⟶ B
e : A ⟶ B
h_1 : Epi e
g : Y ⟶ A
hg : g ≫ e = h.r ≫ f
⊢ ∃ (f' : X ⟶ A), f' ≫ e = f
have h₁ : (h.i ≫ g) ≫ e = f
Tactic: use h.i ≫ g
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
i : Z ⟶ P
hZ : IsZero.{v, u} Z
⊢ Projective.{v, u} P ↔ MorphismProperty.llp (MorphismProperty.epimorphisms C) i
have obtain : Projective.{v, u} P ↔ MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
Tactic: obtain rfl := hZ.eq_of_src i 0
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
⊢ Projective.{v, u} P ↔ MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
have mp : Projective.{v, u} P → MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
mp : Projective.{v, u} P → MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
⊢ Projective.{v, u} P ↔ MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
have mpr : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0 → Projective.{v, u} P
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : Projective.{v, u} P
X Y : C
p : X ⟶ Y
⊢ MorphismProperty.epimorphisms C p → HasLiftingProperty (A := Z) (B := P) 0 p
have mp : Epi p → HasLiftingProperty (A := Z) (B := P) 0 p
Tactic: (_ : Epi p)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
⊢ Projective.{v, u} P
have mpr : ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [Epi e], ∃ (f' : P ⟶ E), f' ≫ e = f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
⊢ ∃ (f' : P ⟶ X), f' ≫ p = f
have this : HasLiftingProperty (A := Z) (B := P) 0 p
Tactic: have := h _ hp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
hZ : IsZero.{v, u} Z
h : MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty (A := Z) (B := P) 0 p
⊢ ∃ (f' : P ⟶ X), f' ≫ p = f
have sq : CommSq (W := Z) 0 0 p f
Tactic: have sq : CommSq 0 (0 : Z ⟶ P) p f := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Preserves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
⊢ Epi (G.map f)
have suffices : ∃ (h : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj X), h ≫ G.map f = Projective.π (G.obj Y)
Tactic: suffices ∃ h, h ≫ G.map f = Projective.π (G.obj Y) from epi_of_epi_fac this.choose_spec
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Preserves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
⊢ ∃ (h : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj X), h ≫ G.map f = Projective.π (G.obj Y)
have refine : Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
  ((adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
        G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f)) ≫
      G.map f :
    Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
  (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
Tactic: refine ⟨adj.unit.app (Projective.over (G.obj Y)) ≫
      G.map (Projective.factorThru (F.map (Projective.π _) ≫ adj.counit.app Y) f), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Preserves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : EnoughProjectives.{v₁, u₁} C
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_3 : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
h : Epi f
⊢ Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    ((adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
          G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f)) ≫
        G.map f :
      Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
    (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
have rw : Eq (α := Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
  (adj.unit.app (Projective.over.{v₁, u₁} (G.obj Y)) ≫
      G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f ≫ f) :
    Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
  (Projective.π (G.obj Y) : Projective.over.{v₁, u₁} (G.obj Y) ⟶ G.obj Y)
Tactic: rw [Category.assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ ExactAt P.complex (n + 1)
have rw : QuasiIsoAt P.π (n + 1)
Tactic: rw [← quasiIsoAt_iff_exactAt' P.π (n + 1) (exactAt_succ_single_obj _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ (ComplexShape.down ℕ).prev (n + 1) = n + 2
have simp : n + 1 + 1 = n + 2
Tactic: simp only [prev]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.complex.d 1 0 ≫ P.π.f 0) 0
have rw : Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
  (P.π.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ C) Z) 1 0) 0
Tactic: rw [← P.π.comm 1 0, single_obj_d, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
rw :
  Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
    (P.π.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ C) Z) 1 0) 0
⊢ Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.complex.d 1 0 ≫ P.π.f 0) 0
have rw₁ : Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.π.f 1 ≫ 0) 0
Tactic: rw [← P.π.comm 1 0, single_obj_d, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
rw :
  Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
    (P.π.f 1 ≫ HomologicalComplex.d (Functor.obj (single₀ C) Z) 1 0) 0
rw₁ : Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.π.f 1 ≫ 0) 0
⊢ Eq (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) (P.complex.d 1 0 ≫ P.π.f 0) 0
have rw₂ : Eq.{v + 1} (α := P.complex.X 1 ⟶ X.{v, u, 0} (Functor.obj (single₀ C) Z) 0) 0 0
Tactic: rw [← P.π.comm 1 0, single_obj_d, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ IsColimit P.cokernelCofork
have refine : CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) sorry ≅ P.cokernelCofork
Tactic: refine IsColimit.ofIsoColimit (P.complex.opcyclesIsCokernel 1 0 (by simp)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯ ≅ P.cokernelCofork
have refine : CategoryStruct.comp (Y :=
    Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
      (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) sorry))
    (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) sorry))
    (Iso.hom
      (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
        (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) =
  Cofork.π P.cokernelCofork
Tactic: refine Cofork.ext (P.complex.isoHomologyι₀.symm ≪≫ isoOfQuasiIsoAt P.π 0 ≪≫
    singleObjHomologySelfIso _ _ _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
        (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
      (Iso.hom
        (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
          (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) =
    Cofork.π P.cokernelCofork
have rw : Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt) 0)
  ((CategoryStruct.comp (Y :=
        Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
          (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) sorry))
        (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) sorry))
        (Iso.hom
          (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
            (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
    Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
  ((Cofork.π P.cokernelCofork ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
    Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
Tactic: rw [← cancel_mono (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 _).inv,
    ← cancel_mono (isoHomologyι₀ _).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
⊢ Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt) 0)
    ((CategoryStruct.comp (Y :=
          Cocone.pt (F := parallelPair (X := P.complex.X 1) (Y := P.complex.X 0) (P.complex.d 1 0) 0)
            (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
          (Cofork.π (CokernelCofork.ofπ (Z := opcycles P.complex 0) (pOpcycles P.complex 0) ⋯))
          (Iso.hom
            (Iso.trans (Y := homology P.complex 0) (Iso.symm P.complex.isoHomologyι₀)
              (isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z))) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
      Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
    ((Cofork.π P.cokernelCofork ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt)) ≫
      Iso.hom (isoHomologyι₀ (Functor.obj (single C (ComplexShape.down ℕ) 0) P.cokernelCofork.pt)))
have dsimp : Eq (α := P.complex.X 0 ⟶ opcycles.{v, u, 0} (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
  ((CategoryStruct.comp (Y := opcycles P.complex 0) (pOpcycles P.complex 0)
        (Iso.inv P.complex.isoHomologyι₀ ≫
          homologyMap P.π 0 ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
      Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
    homologyι (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
  ((P.π.f 0 ≫ Iso.inv (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z)) ≫
    homologyι (Functor.obj (single C (ComplexShape.down ℕ) 0) Z) 0)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ Epi (P.π.f n)
have zero : Epi (X := P.complex.X 0) (P.π.f 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
zero : Epi (X := P.complex.X 0) (P.π.f 0)
⊢ Epi (P.π.f n)
have succ : ∀ (n : ℕ), Epi (X := P.complex.X (n + 1)) (P.π.f (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
n : ℕ
⊢ Epi (X := P.complex.X (n + 1)) (P.π.f (n + 1))
have succ : Epi.{v, u} (C := C) (X := P.complex.X (n + 1)) (Y := X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1)) 0
Tactic: rw [π_f_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
inst_3 : Projective.{v, u} Z
n : ℕ
⊢ Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) n)
have zero : Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
Tactic: cases n
Cleared hypotheses: n