awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I J : InjectiveResolution.{v, u} X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) I I) (𝟙 I.cocomplex)

Tactic:
simpa [id_comp] using descIdHomotopy _ _

Premises used: CategoryTheory.InjectiveResolution.descIdHomotopy, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I J : InjectiveResolution.{v, u} X
⊢ Homotopy (desc (𝟙 X ≫ 𝟙 X) J J) (𝟙 J.cocomplex)

Tactic:
simpa [id_comp] using descIdHomotopy _ _

Premises used: CategoryTheory.InjectiveResolution.descIdHomotopy, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I J : InjectiveResolution.{v, u} X
⊢ I.ι ≫ (I.homotopyEquiv J).hom = J.ι

Tactic:
simp [homotopyEquiv]

Premises used: CategoryTheory.InjectiveResolution.homotopyEquiv
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
I J : InjectiveResolution.{v, u} X
⊢ J.ι ≫ (I.homotopyEquiv J).inv = I.ι

Tactic:
simp [homotopyEquiv]

Premises used: CategoryTheory.InjectiveResolution.homotopyEquiv
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X : C
h :
  Homotopy (C := InjectiveResolution.cocomplex (injectiveResolution X))
    (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X))
    (𝟙 (InjectiveResolution.cocomplex (injectiveResolution X)))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution X)))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution X))))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (𝟙 (InjectiveResolution.cocomplex (injectiveResolution X))))

Tactic:
apply HomotopyCategory.eq_of_homotopy

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X : C
⊢ Homotopy (C := InjectiveResolution.cocomplex (injectiveResolution X))
    (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X))
    (𝟙 (InjectiveResolution.cocomplex (injectiveResolution X)))

Tactic:
apply InjectiveResolution.descIdHomotopy

Premises used: CategoryTheory.InjectiveResolution.descIdHomotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h :
  Homotopy (C := InjectiveResolution.cocomplex (injectiveResolution X)) (D :=
    InjectiveResolution.cocomplex (injectiveResolution Z))
    (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z) (injectiveResolution X))
    (CategoryStruct.comp (Y := InjectiveResolution.cocomplex (injectiveResolution Y))
      (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X))
      (InjectiveResolution.desc g (injectiveResolution Z) (injectiveResolution Y)))
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℕ))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution X)))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ))
        (InjectiveResolution.cocomplex (injectiveResolution Z))))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z) (injectiveResolution X)))
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ))
      (CategoryStruct.comp (Y := InjectiveResolution.cocomplex (injectiveResolution Y))
        (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X))
        (InjectiveResolution.desc g (injectiveResolution Z) (injectiveResolution Y))))

Tactic:
apply HomotopyCategory.eq_of_homotopy

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Homotopy (C := InjectiveResolution.cocomplex (injectiveResolution X)) (D :=
    InjectiveResolution.cocomplex (injectiveResolution Z))
    (InjectiveResolution.desc (f ≫ g) (injectiveResolution Z) (injectiveResolution X))
    (CategoryStruct.comp (Y := InjectiveResolution.cocomplex (injectiveResolution Y))
      (InjectiveResolution.desc f (injectiveResolution Y) (injectiveResolution X))
      (InjectiveResolution.desc g (injectiveResolution Z) (injectiveResolution Y)))

Tactic:
apply InjectiveResolution.descCompHomotopy

Premises used: CategoryTheory.InjectiveResolution.descCompHomotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
h :
  Homotopy (C := cocomplex (injectiveResolution X))
    (CategoryStruct.comp (Y :=
      Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
      (desc f (injectiveResolution Y) (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J)))
    (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ)
⊢ Eq (α :=
    Functor.obj (injectiveResolutions C) X ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
    (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso)
    (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ)

Tactic:
apply HomotopyCategory.eq_of_homotopy

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
h :
  CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
      (CategoryStruct.comp (Y :=
        Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
        (desc f (injectiveResolution Y) (injectiveResolution X))
        (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J))) =
    Functor.map (CochainComplex.single₀ C) f ≫ J.ι
h₁ :
  CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ) =
    Functor.map (CochainComplex.single₀ C) f ≫ J.ι
⊢ Homotopy (C := cocomplex (injectiveResolution X))
    (CategoryStruct.comp (Y :=
      Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
      (desc f (injectiveResolution Y) (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J)))
    (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ)

Tactic:
apply descHomotopy f

Premises used: CategoryTheory.InjectiveResolution.descHomotopy
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
⊢ CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
      (CategoryStruct.comp (Y :=
        Quotient.as (r := homotopic C (ComplexShape.up ℕ)) (Functor.obj (injectiveResolutions C) Y))
        (desc f (injectiveResolution Y) (injectiveResolution X))
        (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution Y) J))) =
    Functor.map (CochainComplex.single₀ C) f ≫ J.ι

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
⊢ CategoryStruct.comp (Y := cocomplex (injectiveResolution X)) (ι (injectiveResolution X))
      (HomotopyEquiv.hom (homotopyEquiv (injectiveResolution X) I) ≫ φ) =
    Functor.map (CochainComplex.single₀ C) f ≫ J.ι

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ syzygies f) (f ≫ d 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
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π 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
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯ ⟶ ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯ :=
  { τ₁ := 𝟙 (ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₂ := 𝟙 (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₃ := ι (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)), comm₁₂ := ⋯, comm₂₃ := ⋯ }
rw : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯)

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono α]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯ ⟶ ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯ :=
  { τ₁ := 𝟙 (ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₂ := 𝟙 (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₃ := ι (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)), comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS :
  IsColimit (F :=
    parallelPair (X := ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯))
      (ShortComplex.f (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)) 0)
    (CokernelCofork.ofπ (ShortComplex.g (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)) ⋯)
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯ ⟶ ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯ :=
  { τ₁ := 𝟙 (ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₂ := 𝟙 (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₃ := ι (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)), comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsColimit (F :=
    parallelPair (X := ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯))
      (ShortComplex.f (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)) 0)
    (CokernelCofork.ofπ (ShortComplex.g (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)) ⋯)

Tactic:
apply cokernelIsCokernel

Premises used: CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z X₀ X₁ : C
f : X₀ ⟶ X₁
⊢ Eq (α := X₀ ⟶ syzygies f) (f ≫ d 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
inst_2 : EnoughInjectives.{v, u} C
Z : C
⊢ Eq.{v + 1} (α := HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (HomologicalComplex.d (ofCocomplex Z) 0 1) (d (Injective.ι Z))

Tactic:
simp [ofCocomplex]

Premises used: CategoryTheory.InjectiveResolution.ofCocomplex
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 1 + 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
rw : ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1))
⊢ HomologicalComplex.ExactAt.{v, u, 0} (ofCocomplex Z) (n + 1)

Tactic:
rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]

Premises used: HAdd.hAdd, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
simp :
  ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₁
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          n))
      (X₃ :=
      ShortComplex.X₁
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (n + 1 + 1)))
      (ShortComplex.f
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          n))
      (ShortComplex.f
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (n + 1)))
      ⋯)
⊢ ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1))

Tactic:
simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofCocomplex,
    CochainComplex.mk', CochainComplex.mk, CochainComplex.of_d]

Premises used: HomologicalComplex.shortComplexFunctor', CochainComplex.of_d, CategoryTheory.InjectiveResolution.ofCocomplex, CochainComplex.mk', HomologicalComplex.sc', CochainComplex.mk
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₁
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          0))
      (X₃ :=
      ShortComplex.X₁
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (HAdd.hAdd (α := ℕ) 0 1 + 1)))
      (ShortComplex.f
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          0))
      (ShortComplex.f
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (HAdd.hAdd (α := ℕ) 0 1)))
      ⋯)

Tactic:
apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)

Premises used: CochainComplex.mkAux, CategoryTheory.Injective.d, CategoryTheory.ShortComplex.f, OfNat.ofNat, CategoryTheory.exact_f_d, CategoryTheory.Injective.ι
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n_1 n : ℕ
⊢ ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₁
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (n + 1)))
      (X₃ :=
      ShortComplex.X₁
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (n + 1 + 1 + 1)))
      (ShortComplex.f
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (n + 1)))
      (ShortComplex.f
        (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
            (d (Injective.ι Z)))
          (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯
          (fun (S : ShortComplex.{v, u} C) ↦
            PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
              (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) ⋯))
          (n + 1 + 1)))
      ⋯)

Tactic:
apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n + 1)).f)

Premises used: CochainComplex.mkAux, HAdd.hAdd, CategoryTheory.Injective.d, CategoryTheory.ShortComplex.f, OfNat.ofNat, CategoryTheory.exact_f_d, CategoryTheory.Injective.ι