awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f').fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
                  Q.d n (n + 1) =
                P.d n (n + 1) ≫ f') ≫
            Q.d (n + 1) (n + 2) =
          P.d (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    PSigma.fst (β := fun (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ↦
      Eq (α := P.X (n + 1) ⟶ Q.X (n + 2))
        (CategoryStruct.comp (Y := Q.X (n + 1))
          (PSigma.fst (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
            PSigma.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
                  (PSigma.mk (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
                    ((P.mkHom Q zero one one_zero_comm succ).f n)
                    (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
                      (P.mkHom Q zero one one_zero_comm succ).f n ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
                      ((P.mkHom Q zero one one_zero_comm succ).f (n + 1)) ⋯)) ≫
                Q.d n (n + 1) =
              P.d n (n + 1) ≫ f')
            (PSigma.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
              (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
              (PSigma.mk (β := fun (f : P.X n ⟶ Q.X n) ↦
                (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
                ((P.mkHom Q zero one one_zero_comm succ).f n)
                (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
                  (P.mkHom Q zero one one_zero_comm succ).f n ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
                  ((P.mkHom Q zero one one_zero_comm succ).f (n + 1)) ⋯))))
          (Q.d (n + 1) (n + 2)))
        (P.d (n + 1) (n + 2) ≫ f''))
      (succ n
        (PSigma.mk (β := fun (f : P.X n ⟶ Q.X n) ↦
          (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
          ((P.mkHom Q zero one one_zero_comm succ).f n)
          (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
            (P.mkHom Q zero one one_zero_comm succ).f n ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f')
            ((P.mkHom Q zero one one_zero_comm succ).f (n + 1)) ⋯)))

Tactic:
dsimp [mkHom, mkHomAux]

Premises used: CochainComplex.mkHom, CochainComplex.mkHomAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
⊢ IsNormalEpiCategory (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
⟨fun p _ =>
  ⟨NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfEval _ _ (fun _ =>
      Abelian.isColimitMapCoconeOfCokernelCoforkOfπ _ _))⟩⟩

Premises used: CategoryTheory.IsNormalEpiCategory.mk, CategoryTheory.Limits.kernel, HomologicalComplex.eval, CategoryTheory.Limits.kernel.condition, CategoryTheory.NormalEpi.mk, Nonempty.intro, HomologicalComplex.isColimitOfEval, OfNat.ofNat, CategoryTheory.Limits.parallelPair, CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ, CategoryTheory.Limits.kernel.ι, CategoryTheory.Limits.CokernelCofork.ofπ
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
⊢ IsNormalMonoCategory (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
⟨fun p _ =>
  ⟨NormalMono.mk _ (cokernel.π p) (cokernel.condition _)
    (isLimitOfEval _ _ (fun _ =>
      Abelian.isLimitMapConeOfKernelForkOfι _ _))⟩⟩

Premises used: CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfι, CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.IsNormalMonoCategory.mk, CategoryTheory.Limits.cokernel, CategoryTheory.Limits.cokernel.condition, HomologicalComplex.eval, Nonempty.intro, CategoryTheory.NormalMono.mk, CategoryTheory.Limits.cokernel.π, OfNat.ofNat, CategoryTheory.Limits.parallelPair, HomologicalComplex.isLimitOfEval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
simp : ∀ (hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))), IsZero S.homology
⊢ S.Exact

Tactic:
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))
rw : Eq (α := S.homology ⟶ S.homology) (𝟙 S.homology) 0
⊢ IsZero S.homology

Tactic:
rw [IsZero.iff_id_eq_zero]

Premises used: CategoryTheory.Limits.IsZero.iff_id_eq_zero
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))
h : ∀ (i : ι), Hom.f (𝟙 S.homology) i = Hom.f 0 i
⊢ Eq (α := S.homology ⟶ S.homology) (𝟙 S.homology) 0

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : ∀ (i : ι), IsZero.{v_1, u_1} (ShortComplex.homology (S.map (eval C c i)))
i : ι
⊢ Hom.f (𝟙 S.homology) i = Hom.f 0 i

Tactic:
apply (IsZero.of_iso (hS i) (S.mapHomologyIso (eval C c i)).symm).eq_of_src

Premises used: HomologicalComplex.eval, CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
mp : S.Exact → ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))
mpr : (∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))) → S.Exact
⊢ S.Exact ↔ ∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
i : ι
⊢ ShortComplex.Exact (S.map (eval C c i))

Tactic:
hS.map (eval C c i)

Premises used: HomologicalComplex.eval, CategoryTheory.ShortComplex.Exact.map
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
i : ι
⊢ ShortComplex.Exact (S.map (eval C c i))

Tactic:
exact hS.map (eval C c i)

Premises used: HomologicalComplex.eval, CategoryTheory.ShortComplex.Exact.map
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
⊢ (∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))) → S.Exact

Tactic:
exact_of_degreewise_exact S

Premises used: HomologicalComplex.exact_of_degreewise_exact
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
⊢ (∀ (i : ι), ShortComplex.Exact (S.map (eval C c i))) → S.Exact

Tactic:
exact exact_of_degreewise_exact S

Premises used: HomologicalComplex.exact_of_degreewise_exact
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
mp : S.ShortExact → ∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))
mpr : (∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))) → S.ShortExact
⊢ S.ShortExact ↔ ∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
⊢ Mono S.f

Tactic:
have := hS.mono_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
this : Mono S.f
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
this_1 : Mono S.f
this : Epi S.g
⊢ ShortComplex.ShortExact (S.map (eval C c i))

Tactic:
hS.map (eval C c i)

Premises used: CategoryTheory.ShortComplex.ShortExact.map, HomologicalComplex.eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.ShortExact
i : ι
this_1 : Mono S.f
this : Epi S.g
⊢ ShortComplex.ShortExact (S.map (eval C c i))

Tactic:
exact hS.map (eval C c i)

Premises used: CategoryTheory.ShortComplex.ShortExact.map, HomologicalComplex.eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
⊢ (∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))) → S.ShortExact

Tactic:
shortExact_of_degreewise_shortExact S

Premises used: HomologicalComplex.shortExact_of_degreewise_shortExact
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
⊢ (∀ (i : ι), ShortComplex.ShortExact (S.map (eval C c i))) → S.ShortExact

Tactic:
exact shortExact_of_degreewise_shortExact S

Premises used: HomologicalComplex.shortExact_of_degreewise_shortExact
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
pos : ∀ (hij : j = i), Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
neg : ∀ (hij : ¬j = i), Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)

Tactic:
by_cases hij : j = i
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
hij : j = i
pos : Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c j) I) j)
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)

Tactic:
subst hij
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
j : ι
I : C
inst_4 pos : Injective.{v_1, u_1} I
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c j) I) j)

Tactic:
simp only [single_obj_X_self]

Premises used: HomologicalComplex.single_obj_X_self
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
⊢ Injective.{v_1, u_1} I

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
hij : ¬j = i
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)

Tactic:
(isZero_single_obj_X _ _ _ _ hij).injective

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.injective
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
I : C
inst_4 : Injective.{v_1, u_1} I
hij : ¬j = i
⊢ Injective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) I) j)

Tactic:
exact (isZero_single_obj_X _ _ _ _ hij).injective

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.injective
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
pos : ∀ (hij : j = i), Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
neg : ∀ (hij : ¬j = i), Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)

Tactic:
by_cases hij : j = i
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
hij : j = i
pos : Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c j) P) j)
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)

Tactic:
subst hij
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
j : ι
P : C
inst_4 pos : Projective.{v_1, u_1} P
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c j) P) j)

Tactic:
simp only [single_obj_X_self]

Premises used: HomologicalComplex.single_obj_X_self
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
⊢ Projective.{v_1, u_1} P

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
hij : ¬j = i
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)

Tactic:
(isZero_single_obj_X _ _ _ _ hij).projective

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.projective
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : DecidableEq ι
i j : ι
P : C
inst_4 : Projective.{v_1, u_1} P
hij : ¬j = i
⊢ Projective.{v_1, u_1} (X.{v_1, u_1, u_2} (Functor.obj (single C c i) P) j)

Tactic:
exact (isZero_single_obj_X _ _ _ _ hij).projective

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.projective
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroMorphisms.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_4 : F.PreservesZeroMorphisms
J : Type u_4
inst_5 : Category.{v_3, u_4} J
inst_6 : HasLimitsOfShape.{v_3, u_4, v_1, u_1} J C
inst_7 : PreservesLimitsOfShape.{v_3, u_4, v_1, v_2, u_1, u_2} J F
⊢ PreservesLimitsOfShape (C := HomologicalComplex.{v_1, u_1, u_3} C c) (D := HomologicalComplex.{v_2, u_2, u_3} D c) J
    (F.mapHomologicalComplex c)

Tactic:
HomologicalComplex.preservesLimitsOfShape_of_eval _ (fun i ↦
    inferInstanceAs <| PreservesLimitsOfShape J <| HomologicalComplex.eval C c i ⋙ F)

Premises used: HomologicalComplex.preservesLimitsOfShape_of_eval, _private.0.CategoryTheory.instPreservesLimitsOfShapeHomologicalComplexMapHomologicalComplexOfHasLimitsOfShape._proof_1
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroMorphisms.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_4 : F.PreservesZeroMorphisms
J : Type u_4
inst_5 : Category.{v_3, u_4} J
inst_6 : HasColimitsOfShape.{v_3, u_4, v_1, u_1} J C
inst_7 : PreservesColimitsOfShape.{v_3, u_4, v_1, v_2, u_1, u_2} J F
⊢ PreservesColimitsOfShape (C := HomologicalComplex.{v_1, u_1, u_3} C c) (D := HomologicalComplex.{v_2, u_2, u_3} D c) J
    (F.mapHomologicalComplex c)

Tactic:
HomologicalComplex.preservesColimitsOfShape_of_eval _ (fun i ↦
    inferInstanceAs <| PreservesColimitsOfShape J <| HomologicalComplex.eval C c i ⋙ F)

Premises used: _private.0.CategoryTheory.instPreservesColimitsOfShapeHomologicalComplexMapHomologicalComplexOfHasColimitsOfShape._proof_1, HomologicalComplex.preservesColimitsOfShape_of_eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroMorphisms.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_4 : HasFiniteLimits.{v_1, u_1} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits F
J : Type
inst_7 : SmallCategory J
inst_8 : FinCategory J
⊢ PreservesLimitsOfShape (C := HomologicalComplex.{v_1, u_1, u_3} C c) (D := HomologicalComplex.{v_2, u_2, u_3} D c) J
    (F.mapHomologicalComplex c)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasZeroMorphisms.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
c : ComplexShape ι
inst_4 : HasFiniteColimits.{v_1, u_1} C
inst_5 : F.PreservesZeroMorphisms
inst_6 : PreservesFiniteColimits F
J : Type
inst_7 : SmallCategory J
inst_8 : FinCategory J
⊢ PreservesColimitsOfShape (C := HomologicalComplex.{v_1, u_1, u_3} C c) (D := HomologicalComplex.{v_2, u_2, u_3} D c) J
    (F.mapHomologicalComplex c)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
dsimp : HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
⊢ HasBinaryBiproduct.{v_1, u_1} (Functor.obj (eval C c i) K) (Functor.obj (eval C c i) L)

Tactic:
dsimp [eval]

Premises used: HomologicalComplex.eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
⊢ HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
have : ∀ (e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)), HasLimit (pair K L ⋙ eval C c i)
⊢ HasLimit (pair K L ⋙ eval C c i)

Tactic:
have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasLimit (pair K L ⋙ eval C c i)

Tactic:
hasLimit_of_iso e.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasLimit (pair K L ⋙ eval C c i)

Tactic:
exact hasLimit_of_iso e.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
have : ∀ (e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)), HasColimit (pair K L ⋙ eval C c i)
⊢ HasColimit (pair K L ⋙ eval C c i)

Tactic:
have e : _ ≅ pair (K.X i) (L.X i) := diagramIsoPair (pair K L ⋙ eval C c i)
-- Module: Mathlib.Algebra.Homology.HomologicalComplexBiprod
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
i : ι
e : pair K L ⋙ eval C c i ≅ pair (K.X i) (L.X i)
⊢ HasColimit (pair K L ⋙ eval C c i)

Tactic:
hasColimit_of_iso e

Premises used: CategoryTheory.Limits.hasColimit_of_iso