awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} X
⊢ Eq (α := ℤ) (↑0 : ℤ) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} X
dsimp :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0 ⟶ R.cochainComplex.X 0)
    (HomologicalComplex.Hom.f
        (Iso.inv (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1)) 0 ≫
      HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat) 0)
    (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv)
⊢ R.ι'.f 0 =
    Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv

Tactic:
dsimp [ι']

Premises used: CategoryTheory.InjectiveResolution.ι'
-- Module: Mathlib.CategoryTheory.Abelian.Injective.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 : InjectiveResolution.{v, u} X
rw :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0 ⟶ R.cochainComplex.X 0)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X.{v, u, 0}
        (HomologicalComplex.extend (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) X)
          ComplexShape.embeddingUpNat)
        0)
      (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
        Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℕ) 0 X) ≫
          Iso.inv
            (HomologicalComplex.extendXIso (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) X)
              ComplexShape.embeddingUpNat ι'._proof_1))
      (Iso.hom
          (HomologicalComplex.extendXIso (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) X)
            ComplexShape.embeddingUpNat ⋯) ≫
        R.ι.f 0 ≫ Iso.inv (HomologicalComplex.extendXIso R.cocomplex ComplexShape.embeddingUpNat ⋯)))
    (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv)
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.singleFunctor C 0) X) 0 ⟶ R.cochainComplex.X 0)
    (HomologicalComplex.Hom.f
        (Iso.inv (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1)) 0 ≫
      HomologicalComplex.Hom.f (HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat) 0)
    (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X) ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv)

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

Premises used: HomologicalComplex.extendSingleIso_inv_f, HomologicalComplex.extendMap_f
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
⊢ QuasiIso (K := Functor.obj (CochainComplex.singleFunctor C 0) X)
    (Iso.inv (HomologicalComplex.extendSingleIso ComplexShape.embeddingUpNat X 0 0 ι'._proof_1) ≫
      HomologicalComplex.extendMap R.ι ComplexShape.embeddingUpNat)

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

Tactic:
simp only [← HomologicalComplex.isSupported_iff_of_quasiIso R.ι']

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

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
X' : C
R' : InjectiveResolution.{v, u} X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : (↑m : ℤ) = n
⊢ ComplexShape.embeddingUpNat.f m = n

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
X' : C
R' : InjectiveResolution.{v, u} X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : (↑m : ℤ) = n
⊢ φ.hom'.f n = (R.cochainComplexXIso n m h).hom ≫ φ.hom.f m ≫ (R'.cochainComplexXIso n m h).inv

Tactic:
simp [hom',
    HomologicalComplex.extendMap_f _ ComplexShape.embeddingUpNat (i := m) (i' := n) (by simpa),
    cochainComplexXIso]

Premises used: HomologicalComplex.extendMap_f, CategoryTheory.InjectiveResolution.Hom.hom', ComplexShape.embeddingUpNat, CategoryTheory.InjectiveResolution.cochainComplexXIso
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Extend
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
R : InjectiveResolution.{v, u} X
X' : C
R' : InjectiveResolution.{v, u} X'
f : X ⟶ X'
φ : R.Hom R' f
⊢ Eq (α :=
    HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) X) 0 ⟶
      R'.cochainComplex.X 0)
    ((R.ι' ≫ φ.hom').f 0) ((Functor.map (CochainComplex.singleFunctor C 0) f ≫ R'.ι').f 0)

Tactic:
simp [hom'_f _ 0 0 rfl, ι'_f_zero, CochainComplex.singleFunctor,
      CochainComplex.singleFunctors,
      HomologicalComplex.single, HomologicalComplex.singleObjXSelf,
      HomologicalComplex.singleObjXIsoOfEq]

Premises used: CategoryTheory.InjectiveResolution.Hom.hom'_f, CategoryTheory.InjectiveResolution.ι'_f_zero, CochainComplex.singleFunctor, HomologicalComplex.singleObjXIsoOfEq, CochainComplex.singleFunctors, HomologicalComplex.singleObjXSelf, OfNat.ofNat, rfl, HomologicalComplex.single
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
⊢ { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := I.cocomplex.X 0, X₃ := I.cocomplex.X 1, f := I.ι.f 0,
      g := I.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
ShortComplex.exact_of_f_is_kernel _ I.isLimitKernelFork

Premises used: CategoryTheory.InjectiveResolution.isLimitKernelFork, CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
dsimp : Eq (α := Z ⟶ I.cocomplex.X 1) (J.ι.f 0 ≫ descFZero f I J ≫ I.cocomplex.d 0 1) 0
⊢ Eq (α :=
    { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
          g := J.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.X₁ ⟶
      I.cocomplex.X 1)
    ({ X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
          g := J.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.f ≫
      descFZero f I J ≫ I.cocomplex.d 0 1)
    0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
simp :
  Eq (α := Z ⟶ I.cocomplex.X 1)
    (CategoryStruct.comp (Y := I.cocomplex.X 0)
        (CategoryStruct.comp (Y := J.cocomplex.X 0) (J.ι.f 0) (factorThru (f ≫ I.ι.f 0) (J.ι.f 0)))
        (I.cocomplex.d 0 1) :
      Z ⟶ I.cocomplex.X 1)
    (0 :
      { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
            g := J.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.X₁ ⟶
        I.cocomplex.X 1)
⊢ Eq (α := Z ⟶ I.cocomplex.X 1) (J.ι.f 0 ≫ descFZero f I J ≫ I.cocomplex.d 0 1) 0

Tactic:
simp only [← assoc, descFZero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.InjectiveResolution.descFZero
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ Eq (α := Z ⟶ I.cocomplex.X 1)
    (CategoryStruct.comp (Y := I.cocomplex.X 0)
        (CategoryStruct.comp (Y := J.cocomplex.X 0) (J.ι.f 0) (factorThru (f ≫ I.ι.f 0) (J.ι.f 0)))
        (I.cocomplex.d 0 1) :
      Z ⟶ I.cocomplex.X 1)
    (0 :
      { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
            g := J.cocomplex.d 0 1, zero := ⋯ : ShortComplex.{v, u} C }.X₁ ⟶
        I.cocomplex.X 1)

Tactic:
simp [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ J.cocomplex.d 0 1 ≫ descFOne f I J = descFZero f I J ≫ I.cocomplex.d 0 1

Tactic:
apply J.exact₀.comp_descToInjective

Premises used: CategoryTheory.ShortComplex.Exact.comp_descToInjective, CategoryTheory.InjectiveResolution.exact₀
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
n : ℕ
g : J.cocomplex.X n ⟶ I.cocomplex.X n
g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1)
w : J.cocomplex.d n (n + 1) ≫ g' = g ≫ I.cocomplex.d n (n + 1)
⊢ Eq (α :=
    (ShortComplex.mk (X₂ := J.cocomplex.X (n + 1)) (X₃ := J.cocomplex.X (n + 2)) (J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 2)) ⋯).X₁ ⟶
      I.cocomplex.X (n + 2))
    ((ShortComplex.mk (X₂ := J.cocomplex.X (n + 1)) (X₃ := J.cocomplex.X (n + 2)) (J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 2)) ⋯).f ≫
      g' ≫ I.cocomplex.d (n + 1) (n + 2))
    0

Tactic:
simp [reassoc_of% w]
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
hfg :
  Eq (α :=
    HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) Z) 0 ⟶
      I.cocomplex.X 0)
    ((J.ι ≫ desc f I J).f 0) ((Functor.map (CochainComplex.single₀ C) f ≫ I.ι).f 0)
⊢ J.ι ≫ desc f I J = Functor.map (CochainComplex.single₀ C) f ≫ I.ι

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ Eq (α :=
    HomologicalComplex.X.{v, u, 0} (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℕ) 0) Z) 0 ⟶
      I.cocomplex.X 0)
    ((J.ι ≫ desc f I J).f 0) ((Functor.map (CochainComplex.single₀ C) f ≫ I.ι).f 0)

Tactic:
simp [desc, descFOne, descFZero]

Premises used: CategoryTheory.InjectiveResolution.descFOne, CategoryTheory.InjectiveResolution.descFZero, CategoryTheory.InjectiveResolution.desc
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
⊢ Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) Z) 0 ⟶ I.cocomplex.X 0)
    ((Functor.map (CochainComplex.single₀ C) f ≫ I.ι).f 0) (f ≫ I.ι.f 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ I.cocomplex.d 0 1 ≫ descHomotopyZeroZero f comm = f.f 0

Tactic:
I.exact₀.comp_descToInjective _ _

Premises used: CategoryTheory.ShortComplex.Exact.comp_descToInjective, CategoryTheory.InjectiveResolution.descHomotopyZeroZero, CategoryTheory.InjectiveResolution.exact₀
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
rw :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
    0
rw₁ :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      f.f 0 ≫ J.cocomplex.d 0 1 =
    0
rw₂ :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      I.cocomplex.d 0 1 ≫ f.f 1 =
    0
rw₃ rw₄ :
  Eq.{v + 1} (α :=
    (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).X₁ ⟶
      J.cocomplex.X 1)
    0 0
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0

Tactic:
rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm,
          HomologicalComplex.Hom.comm, sub_self]

Premises used: sub_self, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.Hom.comm
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm = f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1

Tactic:
(I.exact_succ 0).comp_descToInjective _ _

Premises used: CategoryTheory.ShortComplex.Exact.comp_descToInjective, CategoryTheory.InjectiveResolution.exact_succ, OfNat.ofNat, CategoryTheory.InjectiveResolution.descHomotopyZeroOne
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
dsimp :
  Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X (n + 1)) (X₂ := I.cocomplex.X (n + 1 + 1)) (X₃ := I.cocomplex.X (n + 1 + 2))
          (I.cocomplex.d (n + 1) (n + 1 + 1)) (I.cocomplex.d (n + 1 + 1) (n + 1 + 2)) ⋯).f ≫
      (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ I.cocomplex.d (n + 2) (n + 3) ≫ descHomotopyZeroSucc f n g g' w = f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)

Tactic:
(I.exact_succ (n + 1)).comp_descToInjective _ _

Premises used: CategoryTheory.ShortComplex.Exact.comp_descToInjective, HAdd.hAdd, CategoryTheory.InjectiveResolution.exact_succ, OfNat.ofNat, CategoryTheory.InjectiveResolution.descHomotopyZeroSucc
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ f.f 0 = I.cocomplex.d 0 1 ≫ descHomotopyZeroZero f comm

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ f.f 1 = descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 + I.cocomplex.d 1 2 ≫ descHomotopyZeroOne f comm

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x :
  (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ×'
    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ g'
⊢ f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)

Tactic:
simp only [w, add_comm]

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
n : ℕ
x :
  (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ×'
    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f'
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ g'
⊢ f.f (n + 2) =
    HAdd.hAdd (α := I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 2))
      (CategoryStruct.comp (Y := J.cocomplex.X (n + 1))
        (PSigma.fst (β := fun (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ↦
          f.f (n + 1) =
            PSigma.fst (β := fun (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ↦
                  (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
                    f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f')
                  (PSigma.mk (β := fun (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ↦
                    (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
                      f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f')
                    g
                    (PSigma.mk (β := fun (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ↦
                      f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f') g' w)) ≫
                J.cocomplex.d n (n + 1) +
              I.cocomplex.d (n + 1) (n + 2) ≫ f')
          (PSigma.snd (β := fun (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ↦
            (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
              f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f')
            (PSigma.mk (β := fun (f_1 : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n) ↦
              (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ×'
                f.f (n + 1) = f_1 ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f')
              g
              (PSigma.mk (β := fun (f' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)) ↦
                f.f (n + 1) = g ≫ J.cocomplex.d n (n + 1) + I.cocomplex.d (n + 1) (n + 2) ≫ f') g' w))))
        (J.cocomplex.d (n + 1) (n + 2)))
      (I.cocomplex.d (n + 2) (n + 3) ≫ descHomotopyZeroSucc f n g g' ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
f : Y ⟶ Z
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
g h : I.cocomplex ⟶ J.cocomplex
g_comm : I.ι ≫ g = Functor.map (CochainComplex.single₀ C) f ≫ J.ι
h_comm : I.ι ≫ h = Functor.map (CochainComplex.single₀ C) f ≫ J.ι
⊢ I.ι ≫ (g - h) = 0

Tactic:
simp [g_comm, h_comm]
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I : InjectiveResolution.{v, u} X
g_comm : I.ι ≫ desc (𝟙 X) I I = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι
h_comm : I.ι ≫ 𝟙 I.cocomplex = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι
⊢ Homotopy (desc (𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
apply descHomotopy (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.InjectiveResolution.descHomotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I : InjectiveResolution.{v, u} X
⊢ I.ι ≫ desc (𝟙 X) I I = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I : InjectiveResolution.{v, u} X
⊢ I.ι ≫ 𝟙 I.cocomplex = Functor.map (CochainComplex.single₀ C) (𝟙 X) ≫ I.ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
K : InjectiveResolution.{v, u} Z
g_comm : I.ι ≫ desc (f ≫ g) K I = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι
h_comm : I.ι ≫ desc f J I ≫ desc g K J = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι
⊢ Homotopy (desc (f ≫ g) K I) (desc f J I ≫ desc g K J)

Tactic:
apply descHomotopy (f ≫ g)

Premises used: CategoryTheory.InjectiveResolution.descHomotopy, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
K : InjectiveResolution.{v, u} Z
⊢ I.ι ≫ desc (f ≫ g) K I = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
K : InjectiveResolution.{v, u} Z
⊢ I.ι ≫ desc f J I ≫ desc g K J = Functor.map (CochainComplex.single₀ C) (f ≫ g) ≫ K.ι

Tactic:
simp