awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
Y' : C
g : Y ⟶ Y'
this : HasDerivedCategory C
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y') (↑n : ℤ))
    (ShiftedHom.comp (b := (↑n : ℤ))
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp (b := 0)
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (Functor.map (singleFunctor C 0 ⋙ DerivedCategory.Q) g ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
          inv (Functor.map DerivedCategory.Q R.π')))
      (ShiftedHom.comp (b := 0)
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯
          (Functor.map DerivedCategory.Q (Functor.map (singleFunctor C 0) g) ≫
            NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y'))
        ⋯)
      ⋯)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n_1 n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
⊢ R'.complex.d m n ≫ φ.hom.f n ≫ f = 0

Tactic:
simp [← φ.hom.comm_assoc, hf]

Premises used: CategoryTheory.ProjectiveResolution.Hom.hom, HomologicalComplex.Hom.comm_assoc
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
have :
  ∀ (this : HasDerivedCategory C),
    Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)
      (R'.extMk (φ.hom.f n ≫ f) m hm ⋯)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R'.extMk (φ.hom.f n ≫ f) m hm ⋯)

Tactic:
have := HasDerivedCategory.standard C
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)) (Ext.hom (R'.extMk (φ.hom.f n ≫ f) m hm ⋯))
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X' Y n) (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯) (R'.extMk (φ.hom.f n ≫ f) m hm ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ Eq (α := ℤ) (-(↑n : ℤ)) (-(↑n : ℤ))

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom

Tactic:
simp [φ.hom'_f _ _ rfl]

Premises used: CategoryTheory.ProjectiveResolution.Hom.hom'_f, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this : HasDerivedCategory C
⊢ (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom

Tactic:
have : (R'.cochainComplexXIso (-n) n (by lia)).hom ≫ φ.hom.f n =
      φ.hom'.f (-n) ≫ (R.cochainComplexXIso (-n) n (by lia)).hom := by
    simp [φ.hom'_f _ _ rfl]
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
h :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (ShiftedHom.mk₀ (↑0 : ℤ) Ext.mk₀._proof_1 (Functor.map (DerivedCategory.singleFunctor C 0) g))
      (ShiftedHom.comp
        (ShiftedHom.mk₀ 0 ⋯
          (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
            inv (Functor.map DerivedCategory.Q R.π')))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                  R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
              (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
            DerivedCategory.Q)
          (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
        ⋯)
      ⋯)
    (ShiftedHom.comp
      (ShiftedHom.mk₀ 0 ⋯
        (NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
          inv (Functor.map DerivedCategory.Q R'.π')))
      (ShiftedHom.comp
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R'.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R'.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk (φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯
              ⋯))
          DerivedCategory.Q)
        (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
      ⋯)
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (Ext.hom (Ext.comp (Ext.mk₀ g) (R.extMk f m hm hf) ⋯)) (Ext.hom (R'.extMk (φ.hom.f n ≫ f) m hm ⋯))

Tactic:
simp only [Ext.comp_hom, extMk_hom, Ext.mk₀_hom, reassoc_of% this]

Premises used: CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.comp_hom
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 = -(↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ Eq (α := R.cochainComplex.X (-(↑m : ℤ)) ⟶ Y)
    (R.cochainComplex.d (-(↑m : ℤ)) (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) 0

Tactic:
simpa [R.cochainComplex_d _ _ _ _ rfl rfl]

Premises used: CategoryTheory.ProjectiveResolution.cochainComplex_d, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 0 + (↑0 : ℤ) = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ HAdd.hAdd (α := ℤ) 0 (↑n : ℤ) + (↑0 : ℤ) = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ HAdd.hAdd (α := ℤ) 0 (↑n : ℤ) + 0 = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 0 + 0 = (↑n : ℤ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
h :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj DerivedCategory.Q R.cochainComplex))
    (Functor.map (DerivedCategory.singleFunctor C 0) g ≫
      NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫ inv (Functor.map DerivedCategory.Q R.π'))
    ((NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
        inv (Functor.map DerivedCategory.Q R'.π')) ≫
      Functor.map DerivedCategory.Q φ.hom')
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    (ShiftedHom.comp (a := (↑n : ℤ))
      (ShiftedHom.comp
        (ShiftedHom.mk₀ (↑0 : ℤ) ⋯
          (Functor.map (DerivedCategory.singleFunctor C 0) g ≫
            NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫
              inv (Functor.map DerivedCategory.Q R.π')))
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        ⋯)
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)
    (ShiftedHom.comp (a := (↑n : ℤ))
      (ShiftedHom.comp (a := 0) (b := (↑n : ℤ))
        (ShiftedHom.mk₀ 0 ⋯
          ((NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
              inv (Functor.map DerivedCategory.Q R'.π')) ≫
            Functor.map DerivedCategory.Q φ.hom'))
        (ShiftedHom.map
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle R.cochainComplex ((singleFunctor C 0).obj Y) (↑n : ℤ)) →
                R.cochainComplex ⟶ (shiftFunctor (CochainComplex C ℤ) (↑n : ℤ)).obj ((singleFunctor C 0).obj Y))
            (Cocycle.toSingleMk ((R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ f) ⋯ (-(↑m : ℤ)) ⋯ ⋯))
          DerivedCategory.Q)
        ⋯)
      (ShiftedHom.mk₀ 0 ⋯ (NatTrans.app (Iso.inv (DerivedCategory.singleFunctorIsoCompQ C 0)) Y)) ⋯)

Tactic:
congr 3
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Ext
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
R : ProjectiveResolution.{v, u} X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution.{v, u} X'
g : X' ⟶ X
φ : R'.Hom R g
this_1 : HasDerivedCategory C
this :
  (R'.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom ≫ φ.hom.f n =
    φ.hom'.f (-(↑n : ℤ)) ≫ (R.cochainComplexXIso (-(↑n : ℤ)) n ⋯).hom
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (DerivedCategory.singleFunctor C 0) X')
      (Functor.obj DerivedCategory.Q R.cochainComplex))
    (Functor.map (DerivedCategory.singleFunctor C 0) g ≫
      NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X ≫ inv (Functor.map DerivedCategory.Q R.π'))
    ((NatTrans.app (Iso.hom (DerivedCategory.singleFunctorIsoCompQ C 0)) X' ≫
        inv (Functor.map DerivedCategory.Q R'.π')) ≫
      Functor.map DerivedCategory.Q φ.hom')

Tactic:
simp [← Functor.map_comp_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n₁ n₂ : ℤ
k₁ k₂ : ℕ
h₁ : -(↑k₁ : ℤ) = n₁
h₂ : -(↑k₂ : ℤ) = n₂
⊢ R.cochainComplex.d n₁ n₂ = (R.cochainComplexXIso n₁ k₁ ⋯).hom ≫ R.complex.d k₁ k₂ ≫ (R.cochainComplexXIso n₂ k₂ ⋯).inv

Tactic:
HomologicalComplex.extend_d_eq _ _ h₁ h₂

Premises used: HomologicalComplex.extend_d_eq
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ CochainComplex.IsStrictlyLE (HomologicalComplex.extend R.complex ComplexShape.embeddingDownNat) 0

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
pos : ∀ (hn : n ≤ 0), Projective.{v, u} (R.cochainComplex.X n)
neg : ∀ (hn : ¬n ≤ 0), Projective.{v, u} (R.cochainComplex.X n)
⊢ Projective.{v, u} (R.cochainComplex.X n)

Tactic:
by_cases hn : n ≤ 0
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
hn : n ≤ 0
pos : ∀ (k : ℕ) (hn : LE.le (α := ℤ) (-(↑k : ℤ)) 0), Projective.{v, u} (R.cochainComplex.X (-(↑k : ℤ)))
⊢ Projective.{v, u} (R.cochainComplex.X n)

Tactic:
obtain ⟨k, rfl⟩ := Int.exists_eq_neg_ofNat hn

Premises used: Int.exists_eq_neg_ofNat, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
k : ℕ
hn : LE.le (α := ℤ) (-(↑k : ℤ)) 0
⊢ Projective.{v, u} (R.cochainComplex.X (-(↑k : ℤ)))

Tactic:
Projective.of_iso (R.cochainComplexXIso (-k) k).symm inferInstance

Premises used: inferInstance, Nat.cast, CategoryTheory.ProjectiveResolution.cochainComplexXIso, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, Neg.neg
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
k : ℕ
hn : LE.le (α := ℤ) (-(↑k : ℤ)) 0
⊢ Projective.{v, u} (R.cochainComplex.X (-(↑k : ℤ)))

Tactic:
exact Projective.of_iso (R.cochainComplexXIso (-k) k).symm inferInstance

Premises used: inferInstance, Nat.cast, CategoryTheory.ProjectiveResolution.cochainComplexXIso, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, Neg.neg
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
hn : ¬n ≤ 0
⊢ Projective.{v, u} (R.cochainComplex.X n)

Tactic:
IsZero.projective (CochainComplex.isZero_of_isStrictlyLE _ 0 _)

Premises used: CochainComplex.isZero_of_isStrictlyLE, CategoryTheory.Limits.IsZero.projective, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
n : ℤ
hn : ¬n ≤ 0
⊢ Projective.{v, u} (R.cochainComplex.X n)

Tactic:
exact IsZero.projective (CochainComplex.isZero_of_isStrictlyLE _ 0 _)

Premises used: CochainComplex.isZero_of_isStrictlyLE, CategoryTheory.Limits.IsZero.projective, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ ComplexShape.embeddingDownNat.f 0 = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
dsimp :
  Eq (α := R.cochainComplex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0)
    (HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat) 0 ≫
      HomologicalComplex.Hom.f
        (Iso.hom (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1)) 0)
    ((R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X))
⊢ R.π'.f 0 =
    (R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X)

Tactic:
dsimp [π']

Premises used: CategoryTheory.ProjectiveResolution.π'
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : Preadditive.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
rw :
  Eq (α := R.cochainComplex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X.{v, u, 0}
        (HomologicalComplex.extend (Functor.obj (ChainComplex.single₀ C) X) ComplexShape.embeddingDownNat) 0)
      (Iso.hom (HomologicalComplex.extendXIso R.complex ComplexShape.embeddingDownNat ⋯) ≫
        R.π.f 0 ≫
          Iso.inv
            (HomologicalComplex.extendXIso (Functor.obj (ChainComplex.single₀ C) X) ComplexShape.embeddingDownNat ⋯))
      (Iso.hom
          (HomologicalComplex.extendXIso (Functor.obj (HomologicalComplex.single C (ComplexShape.down ℕ) 0) X)
            ComplexShape.embeddingDownNat π'._proof_1) ≫
        Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 X) ≫
          Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X)))
    ((R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X))
⊢ Eq (α := R.cochainComplex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0)
    (HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat) 0 ≫
      HomologicalComplex.Hom.f
        (Iso.hom (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1)) 0)
    ((R.cochainComplexXIso 0 0 π'_f_zero._proof_2).hom ≫
      R.π.f 0 ≫ Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X))

Tactic:
rw [HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),
    HomologicalComplex.extendSingleIso_hom_f]

Premises used: HomologicalComplex.extendMap_f, HomologicalComplex.extendSingleIso_hom_f
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ QuasiIso (L := Functor.obj (CochainComplex.singleFunctor C 0) X)
    (HomologicalComplex.extendMap R.π ComplexShape.embeddingDownNat ≫
      Iso.hom (HomologicalComplex.extendSingleIso ComplexShape.embeddingDownNat X 0 0 π'._proof_1))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
simp :
  HomologicalComplex.IsSupported.{0, 0, v, u} (Functor.obj (CochainComplex.singleFunctor C 0) X)
    (ComplexShape.embeddingUpIntGE 0)
⊢ R.cochainComplex.IsGE 0

Tactic:
simp only [HomologicalComplex.isSupported_iff_of_quasiIso R.π']

Premises used: CategoryTheory.ProjectiveResolution.π', HomologicalComplex.isSupported_iff_of_quasiIso
-- Module: Mathlib.CategoryTheory.Abelian.Projective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : ProjectiveResolution.{v, u} X
⊢ HomologicalComplex.IsSupported.{0, 0, v, u} (Functor.obj (CochainComplex.singleFunctor C 0) X)
    (ComplexShape.embeddingUpIntGE 0)

Tactic:
infer_instance