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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
h : ∀ (i : ι), m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } i
⊢ m = { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ }

Tactic:
ext 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
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
h :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) t) ⟶ (F ⋙ eval C c i).obj j)
      (m.f i ≫ NatTrans.app (Cone.π (Functor.mapCone (eval C c i) s)) j)
      (NatTrans.app (Cone.π (Functor.mapCone (eval C c i) t)) j)
⊢ m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } i

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

Premises used: HomologicalComplex.eval, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.mapCone
-- 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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
j : J
h : m.f i ≫ (s.π.app j).f i = (t.π.app j).f i
⊢ Eq (α := Cone.pt (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) t) ⟶ (F ⋙ eval C c i).obj j)
    (m.f i ≫ NatTrans.app (Cone.π (Functor.mapCone (eval C c i) s)) j)
    (NatTrans.app (Cone.π (Functor.mapCone (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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
j : J
⊢ m.f i ≫ (s.π.app j).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 : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
w :
  ∀ (j : J),
    Eq (α := limit (F ⋙ eval C c n) ⟶ (F ⋙ eval C c m).obj j)
      (CategoryStruct.comp (Y := limit (F ⋙ eval C c m))
        (limMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }) (limit.π (F ⋙ eval C c m) j))
      (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
⊢ Eq.{v_1 + 1} (α := limit (F ⋙ eval C c n) ⟶ limit (F ⋙ eval C c m))
    (limMap { 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 : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F ⋙ eval C c m).obj j)
    (limit.π (F ⋙ eval C c n) j ≫ NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ } j)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
⊢ Eq (α := limit (F ⋙ eval C c n) ⟶ (F ⋙ eval C c m).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m))
      (limMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }) (limit.π (F ⋙ eval C c m) j))
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))

Tactic:
rw [limMap_π]

Premises used: CategoryTheory.Limits.limMap_π
-- 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 : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) (limit.π (F ⋙ eval C c n) j ≫ (F.obj j).d n m)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
⊢ Eq (α := limit (F ⋙ eval C c n) ⟶ (F ⋙ eval C c m).obj j)
    (limit.π (F ⋙ eval C c n) j ≫ NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ } j)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) 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
inst_3 : ∀ (n : ι), HasLimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) (limit.π (F ⋙ eval C c n) j ≫ 0)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
w₁ :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) 0
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
w₂ w₃ : Eq.{v_1 + 1} (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) 0 0
⊢ Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) (limit.π (F ⋙ eval C c n) j ≫ (F.obj j).d n m)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))

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

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 : ι), HasLimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
h :
  ∀ (n : ι),
    Eq (α :=
      (Functor.obj
              (Functor.obj (Functor.const J)
                { X := fun (n : ι) ↦ limit (F ⋙ eval C c n),
                  d := fun (n m : ι) ↦
                    limMap
                      { 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 })
              i).X
          n ⟶
        (F.obj j).X n)
      (Hom.f
        (CategoryTheory.Functor.map
            (Functor.obj (Functor.const J)
              { X := fun (n : ι) ↦ limit (F ⋙ eval C c n),
                d := fun (n m : ι) ↦
                  limMap
                    { 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 })
            φ ≫
          { f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) j, comm' := ⋯ })
        n)
      (Hom.f ({ f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) i, comm' := ⋯ } ≫ F.map φ) n)
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          { X := fun (n : ι) ↦ limit (F ⋙ eval C c n),
            d := fun (n m : ι) ↦
              limMap
                { 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 })
        i ⟶
      F.obj j)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          { X := fun (n : ι) ↦ limit (F ⋙ eval C c n),
            d := fun (n m : ι) ↦
              limMap
                { 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 })
        φ ≫
      { f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) j, comm' := ⋯ })
    ({ f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) i, comm' := ⋯ } ≫ F.map φ)

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 : ι), HasLimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h : 𝟙 (limit (F ⋙ eval C c n)) ≫ limit.π (F ⋙ eval C c n) j = limit.π (F ⋙ eval C c n) i ≫ (F.map φ).f n
⊢ Eq (α :=
    (Functor.obj
            (Functor.obj (Functor.const J)
              { X := fun (n : ι) ↦ limit (F ⋙ eval C c n),
                d := fun (n m : ι) ↦
                  limMap
                    { 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 })
            i).X
        n ⟶
      (F.obj j).X n)
    (Hom.f
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const J)
            { X := fun (n : ι) ↦ limit (F ⋙ eval C c n),
              d := fun (n m : ι) ↦
                limMap
                  { 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 })
          φ ≫
        { f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) j, comm' := ⋯ })
      n)
    (Hom.f ({ f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) i, comm' := ⋯ } ≫ F.map φ) 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 : ι), HasLimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X n) (limit.π (F ⋙ eval C c n) j)
    (limit.π (F ⋙ eval C c n) i ≫ (F.map φ).f n)
⊢ 𝟙 (limit (F ⋙ eval C c n)) ≫ limit.π (F ⋙ eval C c n) j = limit.π (F ⋙ eval C c n) i ≫ (F.map φ).f n

Tactic:
simp only [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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 : ι), HasLimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X n) (limit.π (F ⋙ eval C c n) j)
    (limit.π (F ⋙ eval C c n) i ≫ CategoryTheory.Functor.map (eval C c n) (F.map φ))
h₁ :
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X n) (limit.π (F ⋙ eval C c n) j)
    (limit.π (F ⋙ eval C c n) i ≫ (F ⋙ eval C c n).map φ)
h₂ h₃ : Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X n) (limit.π (F ⋙ eval C c n) j) (limit.π (F ⋙ eval C c n) j)
⊢ Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X n) (limit.π (F ⋙ eval C c n) j)
    (limit.π (F ⋙ eval C c n) i ≫ (F.map φ).f n)

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

Premises used: HomologicalComplex.eval_map, CategoryTheory.Functor.comp_map, CategoryTheory.Limits.limit.w
-- 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 : ι), HasLimit (F ⋙ eval C c n)
⊢ HasLimit F

Tactic:
⟨⟨⟨_, isLimitConeOfHasLimitEval F⟩⟩⟩

Premises used: HomologicalComplex.isLimitConeOfHasLimitEval, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.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 : ι), HasLimit (F ⋙ eval C c n)
n : ι
⊢ PreservesLimit F (eval C c n)

Tactic:
preservesLimit_of_preserves_limit_cone (isLimitConeOfHasLimitEval F) (limit.isLimit _)

Premises used: HomologicalComplex.isLimitConeOfHasLimitEval, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- 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 : HasLimitsOfShape.{v_2, u_3, v_1, u_1} J C
⊢ HasLimitsOfShape J (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasLimitsOfShape.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 : HasLimitsOfShape.{v_2, u_3, v_1, u_1} J C
n : ι
⊢ PreservesLimitsOfShape (C := HomologicalComplex.{v_1, u_1, u_2} C c) J (eval C c n)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesLimitsOfShape.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 : HasFiniteLimits.{v_1, u_1} C
⊢ HasFiniteLimits (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
⟨fun _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.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 : HasFiniteLimits.{v_1, u_1} C
n : ι
⊢ PreservesFiniteLimits (C := HomologicalComplex.{v_1, u_1, u_2} C c) (eval C c n)

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteLimits.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 : HasFiniteLimits.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
inst_4 : Mono φ
n : ι
change : Mono (X := Functor.obj (eval C c n) K) (CategoryTheory.Functor.map (eval C c n) φ)
⊢ Mono (φ.f n)

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

Premises used: CategoryTheory.Mono, 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 : HasFiniteLimits.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
inst_4 : Mono φ
n : ι
⊢ Mono (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
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
i i' : ι
h : c.Rel i i'
apply :
  ∀ (j : J),
    Eq (α := (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
      (CategoryStruct.comp (Y :=
        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) s))) j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j)
        ((hs i).desc (Functor.mapCocone (eval C c i) t) ≫ t.pt.d i i'))
      (CategoryStruct.comp (Y :=
        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) s))) j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j)
        (s.pt.d i i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t)))
⊢ Eq (α := s.pt.X i ⟶ t.pt.X i') ((hs i).desc (Functor.mapCocone (eval C c i) t) ≫ t.pt.d i i' : s.pt.X i ⟶ t.pt.X i')
    (s.pt.d i i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t) : s.pt.X i ⟶ t.pt.X i')

Tactic:
apply IsColimit.hom_ext (hs i)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- 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
i i' : ι
h : c.Rel i i'
j : J
⊢ ∀ (k : ι) (j : J),
    Eq (α := (F ⋙ eval C c k).obj j ⟶ Cocone.pt (F := F ⋙ eval C c k) (Functor.mapCocone (eval C c k) t))
      (CategoryStruct.comp (Y :=
          Functor.obj.{v_2, v_1, u_3, u_1}
            (Functor.obj (Functor.const J) (Cocone.pt (F := F ⋙ eval C c k) (Functor.mapCocone (eval C c k) s))) j)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c k) s)) j)
          ((hs k).desc (Functor.mapCocone (eval C c k) t)) :
        (F ⋙ eval C c k).obj j ⟶ Cocone.pt (F := F ⋙ eval C c k) (Functor.mapCocone (eval C c k) t))
      (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c k) t)) j :
        (F ⋙ eval C c k).obj j ⟶
          Functor.obj.{v_2, v_1, u_3, u_1}
            (Functor.obj (Functor.const J) (Cocone.pt (F := F ⋙ eval C c k) (Functor.mapCocone (eval C c k) t))) j)

Tactic:
have eq := fun k => (hs k).fac ((eval C c k).mapCocone t)
-- 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
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (s.ι.app j).f k ≫ (hs k).desc (Functor.mapCocone (eval C c k) t) = (t.ι.app j).f k
simp :
  Eq (α := (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
    ((s.ι.app j).f i ≫ (hs i).desc (Functor.mapCocone (eval C c i) t) ≫ t.pt.d i i' :
      (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
    ((s.ι.app j).f i ≫ s.pt.d i i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t) :
      (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
⊢ Eq (α := (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
    (CategoryStruct.comp (Y :=
      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) s))) j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j)
      ((hs i).desc (Functor.mapCocone (eval C c i) t) ≫ t.pt.d i i'))
    (CategoryStruct.comp (Y :=
      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) s))) j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j)
      (s.pt.d i i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t)))

Tactic:
simp only [Functor.mapCocone_ι_app, eval_map]

Premises used: CategoryTheory.Functor.mapCocone_ι_app, HomologicalComplex.eval_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
s : Cocone F
hs : (i : ι) → IsColimit (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) s)
t : Cocone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (s.ι.app j).f k ≫ (hs k).desc (Functor.mapCocone (eval C c k) t) = (t.ι.app j).f k
rw : (t.ι.app j).f i ≫ t.pt.d i i' = (s.ι.app j).f i ≫ s.pt.d i i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t)
rw₁ :
  (t.ι.app j).f i ≫ t.pt.d i i' = (F.obj j).d i i' ≫ (s.ι.app j).f i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t)
rw₂ : (t.ι.app j).f i ≫ t.pt.d i i' = (F.obj j).d i i' ≫ (t.ι.app j).f i'
rw₃ rw₄ : (F.obj j).d i i' ≫ (t.ι.app j).f i' = (F.obj j).d i i' ≫ (t.ι.app j).f i'
⊢ Eq (α := (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
    ((s.ι.app j).f i ≫ (hs i).desc (Functor.mapCocone (eval C c i) t) ≫ t.pt.d i i' :
      (F ⋙ eval C c i).obj j ⟶ t.pt.X i')
    ((s.ι.app j).f i ≫ s.pt.d i i' ≫ (hs i').desc (Functor.mapCocone (eval C c i') t) :
      (F ⋙ eval C c i).obj j ⟶ t.pt.X i')

Tactic:
rw [reassoc_of% (eq i), Hom.comm_assoc, eq i', Hom.comm]

Premises used: HomologicalComplex.Hom.comm_assoc, HomologicalComplex.Hom.comm
-- 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
j : J
h :
  ∀ (i : ι),
    Hom.f (s.ι.app j ≫ { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ }) i =
      (t.ι.app j).f i
⊢ s.ι.app j ≫ { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ } = t.ι.app j

Tactic:
ext 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
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
j : J
i : ι
⊢ Hom.f (s.ι.app j ≫ { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ }) i =
    (t.ι.app j).f i

Tactic:
apply (hs i).fac

Premises used: CategoryTheory.Limits.IsColimit.fac
-- 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
h : ∀ (i : ι), m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ } i
⊢ m = { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ }

Tactic:
ext i