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
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) ⋯))
          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)))
      ⋯)

Tactic:
match n with
  | 0 => apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)
  | n + 1 => apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n + 1)).f)
-- 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 : ℕ
zero : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0)
succ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1))
succ₁ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))
succ₂ : ∀ (n : ℕ), Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (n + 1 + 1 + 1))
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) n)

Tactic:
obtain (_ | _ | _ | n) := n
-- 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
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0)

Tactic:
apply Injective.injective_under

Premises used: CategoryTheory.Injective.injective_under
-- 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
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
apply Injective.injective_under

Premises used: CategoryTheory.Injective.injective_under
-- 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
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))

Tactic:
apply Injective.injective_under

Premises used: CategoryTheory.Injective.injective_under
-- 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 : ℕ
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (n + 1 + 1 + 1))

Tactic:
apply Injective.injective_under

Premises used: CategoryTheory.Injective.injective_under
-- 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
rw :
  Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (Injective.ι Z ≫ d (Injective.ι Z) : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
rw₁ :
  Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 ≫ Injective.ι (cokernel.{v, u} (Y := under.{v, u} Z) (Injective.ι Z)) :
      Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
rw₂ rw₃ : Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) 0 0
⊢ Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) (Injective.ι Z : Z ⟶ under.{v, u} Z)
      (HomologicalComplex.d (ofCocomplex Z) 0 1))
    0

Tactic:
rw [ofCocomplex_d_0_1, cokernel.condition_assoc, zero_comp]

Premises used: CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CategoryTheory.Limits.cokernel.condition_assoc, CategoryTheory.Limits.zero_comp
-- 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 : ℕ
zero :
  QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    0
succ :
  ∀ (n : ℕ),
    QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
      ofCocomplex Z)
      ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
          (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
            (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
        (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
            Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
              (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0)
            (Injective.ι Z) ⋯ :
          { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
            Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
              (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0 }))
      (n + 1)
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    n

Tactic:
cases n
-- 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
dsimp : Mono.{v, u} (Y := under.{v, u} Z) (Injective.ι Z)
⊢ Mono.{v, u} (X :=
    ShortComplex.X₁.{v, u}
      (ShortComplex.mk (X₂ := under.{v, u} Z) (X₃ := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (Injective.ι Z) (d (Injective.ι Z)) ⋯))
    (ShortComplex.f
      (ShortComplex.mk (X₂ := under.{v, u} Z) (X₃ := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (Injective.ι Z) (d (Injective.ι Z)) ⋯))

Tactic:
dsimp
-- 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
⊢ Mono.{v, u} (Y := under.{v, u} Z) (Injective.ι Z)

Tactic:
infer_instance
-- 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
⊢ Iso (C := ShortComplex.{v, u} C)
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
          (Functor.obj (CochainComplex.single₀ C) Z)))
      (X₂ :=
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
      (ShortComplex.Hom.τ₂
        (Functor.map (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
          ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
              (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
                (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
            (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
                Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                  (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0)
                (Injective.ι Z) ⋯ :
              { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
                Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                  (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0 }))))
      (ShortComplex.g
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
      ⋯)
    (ShortComplex.mk (X₂ := under.{v, u} Z) (X₃ := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
      (Injective.ι Z) (d (Injective.ι Z)) ⋯)

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
          (by simp [ofCocomplex])

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.isoMk
-- 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} (α :=
    ShortComplex.X₁.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
          (Functor.obj (CochainComplex.single₀ C) Z)) ⟶
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
          (Functor.obj (CochainComplex.single₀ C) Z)))
    (ShortComplex.f
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
        (Functor.obj (CochainComplex.single₀ C) Z)))
    0

Tactic:
rfl
-- 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} (α :=
    ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
          (Functor.obj (CochainComplex.single₀ C) Z)) ⟶
      ShortComplex.X₃.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
          (Functor.obj (CochainComplex.single₀ C) Z)))
    (ShortComplex.g
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
        (Functor.obj (CochainComplex.single₀ C) Z)))
    0

Tactic:
rfl
-- 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} (α :=
    ShortComplex.X₁.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)) ⟶
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
    (ShortComplex.f (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
    0

Tactic:
rfl
-- 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 : ℕ
succ : HomologicalComplex.ExactAt.{v, u, 0} (ofCocomplex Z) (n + 1)
succ₁ : HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) Z) (n + 1)
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    (n + 1)

Tactic:
rw [quasiIsoAt_iff_exactAt]

Premises used: quasiIsoAt_iff_exactAt
-- 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 : ℕ
⊢ HomologicalComplex.ExactAt.{v, u, 0} (ofCocomplex Z) (n + 1)

Tactic:
apply ofCocomplex_exactAt_succ

Premises used: CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ
-- 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 : ℕ
⊢ HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) Z) (n + 1)

Tactic:
apply CochainComplex.exactAt_succ_single_obj

Premises used: CochainComplex.exactAt_succ_single_obj
-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
ip : InjectivePresentation.{v, u} X
⊢ ShortComplex.ShortExact ip.shortComplex

Tactic:
{ exact := ShortComplex.exact_cokernel ip.f }

Premises used: CategoryTheory.InjectivePresentation.f, CategoryTheory.ShortComplex.exact_cokernel, CategoryTheory.ShortComplex.ShortExact.mk
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
dsimp :
  Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Functor.map F.leftDerivedToHomotopyCategory f) ≫
      Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex))
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
          (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
      HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)
⊢ (F.leftDerived n).map f ≫ Iso.hom (Q.isoLeftDerivedObj F n) =
    Iso.hom (P.isoLeftDerivedObj F n) ≫
      Functor.map
        (Functor.comp (D := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ))
          (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n))
        φ

Tactic:
dsimp [isoLeftDerivedObj, Functor.leftDerived]

Premises used: CategoryTheory.ProjectiveResolution.isoLeftDerivedObj, CategoryTheory.Functor.leftDerived
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
⊢ Eq (α :=
    Functor.obj (C := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) (Functor.obj F.leftDerivedToHomotopyCategory X) ⟶
      HomologicalComplex.homology (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex) n)
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        Functor.map (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
    (Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n)
        (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
      NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) ≫
        HomologicalComplex.homologyMap (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ) n)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
⊢ IsZero.{v_1, u_1} ((F.leftDerived (n + 1)).obj X)

Tactic:
IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoLeftDerivedObj F (n + 1))

Premises used: CategoryTheory.ProjectiveResolution.isoLeftDerivedObj, CategoryTheory.ProjectiveResolution.self, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
refine :
  IsZero.{v_1, u_1}
    (obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1))
      (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (ProjectiveResolution.self X))))
⊢ IsZero.{v_1, u_1} ((F.leftDerived (n + 1)).obj X)

Tactic:
refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoLeftDerivedObj F (n + 1))

Premises used: CategoryTheory.ProjectiveResolution.isoLeftDerivedObj, CategoryTheory.ProjectiveResolution.self, CategoryTheory.Limits.IsZero.of_iso, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
erw :
  HomologicalComplex.ExactAt
    (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
      (ProjectiveResolution.complex (ProjectiveResolution.self X)))
    (n + 1)
⊢ IsZero.{v_1, u_1}
    (obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) (n + 1))
      (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
        (ProjectiveResolution.complex (ProjectiveResolution.self X))))

Tactic:
erw [← HomologicalComplex.exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
⊢ IsZero.{v, u} (HomologicalComplex.X.{v, u, 0} (ProjectiveResolution.complex (ProjectiveResolution.self X)) (n + 1))

Tactic:
apply isZero_zero

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
n : ℕ
X : C
inst_6 : Projective.{v, u} X
⊢ HomologicalComplex.ExactAt
    (obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ)) (F.mapHomologicalComplex (ComplexShape.down ℕ))
      (ProjectiveResolution.complex (ProjectiveResolution.self X)))
    (n + 1)

Tactic:
exact ShortComplex.exact_of_isZero_X₂ _ (F.map_isZero (by apply isZero_zero))

Premises used: CategoryTheory.ShortComplex.exact_of_isZero_X₂