awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cocone F
hs : (i : ι) → IsColimit (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
h :
  ∀ (j : J),
    Eq (α := (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
      (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j ≫ m.f i :
        (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
      (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) t)) j :
        (F ⋙ eval C c i).obj j ⟶
          Functor.obj.{v_2, v_1, u_3, u_1}
            (Functor.obj (Functor.const J) (Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))) j)
⊢ m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ } i

Tactic:
apply (hs i).uniq ((eval C c i).mapCocone t)

Premises used: CategoryTheory.Functor.mapCocone, HomologicalComplex.eval, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cocone F
hs : (i : ι) → IsColimit (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
j : J
h : (s.ι.app j).f i ≫ m.f i = (t.ι.app j).f i
⊢ Eq (α := (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
    (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j ≫ m.f i :
      (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
    (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) t)) j :
      (F ⋙ eval C c i).obj j ⟶
        Functor.obj.{v_2, v_1, u_3, u_1}
          (Functor.obj (Functor.const J) (Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))) j)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cocone F
hs : (i : ι) → IsColimit (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
j : J
⊢ (s.ι.app j).f i ≫ m.f i = (t.ι.app j).f i

Tactic:
simp only [← comp_f, hm]

Premises used: HomologicalComplex.comp_f
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
w :
  ∀ (j : J),
    Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
      (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j)
        (colimMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }))
      (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
⊢ Eq.{v_1 + 1} (α := colimit (F ⋙ eval C c n) ⟶ colimit (F ⋙ eval C c m))
    (colimMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }) 0

Tactic:
ext j
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
    (NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ } j ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
⊢ Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j)
      (colimMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }))
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)

Tactic:
rw [ι_colimMap]

Premises used: CategoryTheory.Limits.ι_colimMap
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) ((F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
⊢ Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
    (NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ } j ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) (0 ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
w₁ :
  Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) 0
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
w₂ w₃ : Eq.{v_1 + 1} (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) 0 0
⊢ Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) ((F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)

Tactic:
rw [(F.obj j).shape _ _ h, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
h :
  ∀ (n : ι),
    Eq (α :=
      (F.obj i).X n ⟶
        (Functor.obj
              (Functor.obj (Functor.const J)
                { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
                  d := fun (n m : ι) ↦
                    colimMap
                      { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ :
                        NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
                  shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
              j).X
          n)
      (Hom.f (F.map φ ≫ { f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) j, comm' := ⋯ }) n)
      (Hom.f
        ({ f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) i, comm' := ⋯ } ≫
          CategoryTheory.Functor.map
            (Functor.obj (Functor.const J)
              { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
                d := fun (n m : ι) ↦
                  colimMap
                    { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ :
                      NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
                shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
            φ)
        n)
⊢ Eq (α :=
    F.obj i ⟶
      Functor.obj
        (Functor.obj (Functor.const J)
          { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
            d := fun (n m : ι) ↦
              colimMap
                { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ : NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
        j)
    (F.map φ ≫ { f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) j, comm' := ⋯ })
    ({ f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) i, comm' := ⋯ } ≫
      CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
            d := fun (n m : ι) ↦
              colimMap
                { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ : NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
        φ)

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h : (F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i ≫ 𝟙 (colimit (F ⋙ eval C c n))
⊢ Eq (α :=
    (F.obj i).X n ⟶
      (Functor.obj
            (Functor.obj (Functor.const J)
              { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
                d := fun (n m : ι) ↦
                  colimMap
                    { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ :
                      NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
                shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
            j).X
        n)
    (Hom.f (F.map φ ≫ { f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) j, comm' := ⋯ }) n)
    (Hom.f
      ({ f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) i, comm' := ⋯ } ≫
        CategoryTheory.Functor.map
          (Functor.obj (Functor.const J)
            { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
              d := fun (n m : ι) ↦
                colimMap
                  { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ :
                    NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
              shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
          φ)
      n)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h :
  Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)
⊢ (F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i ≫ 𝟙 (colimit (F ⋙ eval C c n))

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h :
  Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
    (CategoryTheory.Functor.map (eval C c n) (F.map φ) ≫ colimit.ι (F ⋙ eval C c n) j :
      (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
    (colimit.ι (F ⋙ eval C c n) i : (F ⋙ eval C c n).obj i ⟶ colimit (F ⋙ eval C c n))
h₁ :
  Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F ⋙ eval C c n).map φ ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)
h₂ h₃ : Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) i) (colimit.ι (F ⋙ eval C c n) i)
⊢ Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)

Tactic:
rw [← eval_map, ← Functor.comp_map, colimit.w]

Premises used: HomologicalComplex.eval_map, CategoryTheory.Limits.colimit.w, CategoryTheory.Functor.comp_map
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
⊢ HasColimit F

Tactic:
⟨⟨⟨_, isColimitCoconeOfHasColimitEval F⟩⟩⟩

Premises used: HomologicalComplex.isColimitCoconeOfHasColimitEval, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n : ι
⊢ PreservesColimit F (eval C c n)

Tactic:
preservesColimit_of_preserves_colimit_cocone (isColimitCoconeOfHasColimitEval F)
    (colimit.isColimit _)

Premises used: HomologicalComplex.isColimitCoconeOfHasColimitEval, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasColimitsOfShape.{v_2, u_3, v_1, u_1} J C
⊢ HasColimitsOfShape J (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
⟨inferInstance⟩

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, inferInstance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasColimitsOfShape.{v_2, u_3, v_1, u_1} J C
n : ι
⊢ PreservesColimitsOfShape (C := HomologicalComplex.{v_1, u_1, u_2} C c) J (eval C c n)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteColimits.{v_1, u_1} C
⊢ HasFiniteColimits (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteColimits.{v_1, u_1} C
n : ι
⊢ PreservesFiniteColimits (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c n)

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: CategoryTheory.Limits.PreservesFiniteColimits.mk, inferInstance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteColimits.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
inst_4 : Epi φ
n : ι
change : Epi (X := Functor.obj (eval C c n) K) (CategoryTheory.Functor.map (eval C c n) φ)
⊢ Epi (φ.f n)

Tactic:
change Epi ((HomologicalComplex.eval C c n).map φ)

Premises used: CategoryTheory.Epi, HomologicalComplex.eval, CategoryTheory.Functor.map
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteColimits.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
inst_4 : Epi φ
n : ι
⊢ Epi (X := Functor.obj (eval C c n) K) (CategoryTheory.Functor.map (eval C c n) φ)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
D : Type u_4
inst_3 : Category.{v_3, u_4} D
G : D ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
h : ∀ (i : ι), PreservesLimitsOfShape.{v_2, u_3, v_3, v_1, u_4, u_1} J (G ⋙ eval C c i)
⊢ PreservesLimitsOfShape J G

Tactic:
⟨fun {_} => ⟨fun hs ↦ ⟨isLimitOfEval _ _
    (fun i => isLimitOfPreserves (G ⋙ eval C c i) hs)⟩⟩⟩

Premises used: CategoryTheory.Functor.comp, HomologicalComplex.eval, Nonempty.intro, CategoryTheory.Limits.PreservesLimitsOfShape.mk, CategoryTheory.Limits.PreservesLimit.mk, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.isLimitOfPreserves, HomologicalComplex.isLimitOfEval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
D : Type u_4
inst_3 : Category.{v_3, u_4} D
G : D ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
h : ∀ (i : ι), PreservesColimitsOfShape.{v_2, u_3, v_3, v_1, u_4, u_1} J (G ⋙ eval C c i)
⊢ PreservesColimitsOfShape J G

Tactic:
⟨fun {_} => ⟨fun hs ↦ ⟨isColimitOfEval _ _
    (fun i => isColimitOfPreserves (G ⋙ eval C c i) hs)⟩⟩⟩

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.comp, HomologicalComplex.eval, Nonempty.intro, HomologicalComplex.isColimitOfEval, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Limits.PreservesColimitsOfShape.mk, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
pos :
  ∀ (h : j = i),
    PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
neg :
  ∀ (h : ¬j = i),
    PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))

Tactic:
by_cases h : j = i
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
h : j = i
pos :
  PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c j) (eval C c j))
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
j : ι
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c j) (eval C c j))

Tactic:
preservesLimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Iso.symm, HomologicalComplex.singleCompEvalIsoSelf
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
j : ι
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c j) (eval C c j))

Tactic:
exact preservesLimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, CategoryTheory.Iso.symm, HomologicalComplex.singleCompEvalIsoSelf
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))

Tactic:
Functor.preservesLimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _

Premises used: CategoryTheory.Functor.preservesLimitsOfShape_of_isZero, HomologicalComplex.isZero_single_comp_eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))

Tactic:
exact Functor.preservesLimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _

Premises used: CategoryTheory.Functor.preservesLimitsOfShape_of_isZero, HomologicalComplex.isZero_single_comp_eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
pos :
  ∀ (h : j = i),
    PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
neg :
  ∀ (h : ¬j = i),
    PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
⊢ PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))

Tactic:
by_cases h : j = i
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
h : j = i
pos :
  PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c j) (eval C c j))
⊢ PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))

Tactic:
subst h