awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasLimit (F ⋙ π₁)
inst_4 : HasLimit (F ⋙ π₂)
inst_5 : HasLimit (F ⋙ π₃)
⊢ PreservesLimit F π₁

Tactic:
preservesLimit_of_preserves_limit_cone (isLimitLimitCone F) (isLimitπ₁MapConeLimitCone F)

Premises used: CategoryTheory.ShortComplex.isLimitLimitCone, CategoryTheory.ShortComplex.isLimitπ₁MapConeLimitCone, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasLimit (F ⋙ π₁)
inst_4 : HasLimit (F ⋙ π₂)
inst_5 : HasLimit (F ⋙ π₃)
⊢ PreservesLimit F π₂

Tactic:
preservesLimit_of_preserves_limit_cone (isLimitLimitCone F) (isLimitπ₂MapConeLimitCone F)

Premises used: CategoryTheory.ShortComplex.isLimitLimitCone, CategoryTheory.ShortComplex.isLimitπ₂MapConeLimitCone, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasLimit (F ⋙ π₁)
inst_4 : HasLimit (F ⋙ π₂)
inst_5 : HasLimit (F ⋙ π₃)
⊢ PreservesLimit F π₃

Tactic:
preservesLimit_of_preserves_limit_cone (isLimitLimitCone F) (isLimitπ₃MapConeLimitCone F)

Premises used: CategoryTheory.ShortComplex.isLimitLimitCone, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.ShortComplex.isLimitπ₃MapConeLimitCone
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteLimits.{v_2, u_2} C
⊢ HasFiniteLimits (ShortComplex.{v_2, u_2} C)

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteLimits.{v_2, u_2} C
⊢ PreservesFiniteLimits (C := ShortComplex.{v_2, u_2} C) π₁

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteLimits.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteLimits.{v_2, u_2} C
⊢ PreservesFiniteLimits (C := ShortComplex.{v_2, u_2} C) π₂

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteLimits.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasFiniteLimits.{v_2, u_2} C
⊢ PreservesFiniteLimits (C := ShortComplex.{v_2, u_2} C) π₃

Tactic:
⟨fun _ _ _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesFiniteLimits.mk
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasLimitsOfShape.{0, 0, v_2, u_2} WalkingCospan C
⊢ PreservesMonomorphisms (C := ShortComplex.{v_2, u_2} C) π₁

Tactic:
CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape _

Premises used: CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasLimitsOfShape.{0, 0, v_2, u_2} WalkingCospan C
⊢ PreservesMonomorphisms (C := ShortComplex.{v_2, u_2} C) π₂

Tactic:
CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape _

Premises used: CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
inst_3 : HasLimitsOfShape.{0, 0, v_2, u_2} WalkingCospan C
⊢ PreservesMonomorphisms (C := ShortComplex.{v_2, u_2} C) π₃

Tactic:
CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape _

Premises used: CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
⊢ ∀ (j : J),
    Eq (α := (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (h₁.desc (mapCocone π₁ s)) :
        (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (NatTrans.app (Cocone.ι (mapCocone π₁ s)) j :
        (F ⋙ π₁).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))) j)

Tactic:
have eq₁ := h₁.fac (π₁.mapCocone s)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (h₁.desc (mapCocone π₁ s)) :
        (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (NatTrans.app (Cocone.ι (mapCocone π₁ s)) j :
        (F ⋙ π₁).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))) j)
⊢ ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)

Tactic:
have eq₂ := h₂.fac (π₂.mapCocone s)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (h₁.desc (mapCocone π₁ s)) :
        (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (NatTrans.app (Cocone.ι (mapCocone π₁ s)) j :
        (F ⋙ π₁).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))) j)
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
⊢ ∀ (j : J), (c.ι.app j).τ₁ ≫ (obj (obj (const J) c.pt) j).f = (F.obj j).f ≫ (c.ι.app j).τ₂

Tactic:
have eq₁₂ := fun j => (c.ι.app j).comm₁₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (h₁.desc (mapCocone π₁ s)) :
        (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (NatTrans.app (Cocone.ι (mapCocone π₁ s)) j :
        (F ⋙ π₁).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))) j)
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ (obj (obj (const J) c.pt) j).f = (F.obj j).f ≫ (c.ι.app j).τ₂
⊢ ∀ (j : J), (s.ι.app j).τ₁ ≫ (obj (obj (const J) s.pt) j).f = (F.obj j).f ≫ (s.ι.app j).τ₂

Tactic:
have eq₁₂' := fun j => (s.ι.app j).comm₁₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (h₁.desc (mapCocone π₁ s)) :
        (F ⋙ π₁).obj j ⟶ Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))
      (NatTrans.app (Cocone.ι (mapCocone π₁ s)) j :
        (F ⋙ π₁).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ s))) j)
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ (obj (obj (const J) c.pt) j).f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ (obj (obj (const J) s.pt) j).f = (F.obj j).f ≫ (s.ι.app j).τ₂
dsimp :
  Eq (α := (F.obj j).X₁ ⟶ s.pt.X₂) ((c.ι.app j).τ₁ ≫ h₁.desc (mapCocone π₁ s) ≫ s.pt.f : (F.obj j).X₁ ⟶ s.pt.X₂)
    ((c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (mapCocone π₂ s) : (F.obj j).X₁ ⟶ s.pt.X₂)
⊢ Eq (α := (F ⋙ π₁).obj j ⟶ s.pt.X₂)
    (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
      (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (h₁.desc (mapCocone π₁ s) ≫ s.pt.f))
    (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₁) (mapCocone π₁ c))) j)
      (NatTrans.app (Cocone.ι (mapCocone π₁ c)) j) (c.pt.f ≫ h₂.desc (mapCocone π₂ s)))

Tactic:
dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₁ : ∀ (j : J), (c.ι.app j).τ₁ ≫ h₁.desc (mapCocone π₁ s) = (s.ι.app j).τ₁
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (mapCocone π₂ s) = (s.ι.app j).τ₂
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ c.pt.f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (s.ι.app j).τ₂
rw : (s.ι.app j).τ₁ ≫ s.pt.f = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (mapCocone π₂ s)
rw₁ : (F.obj j).f ≫ (s.ι.app j).τ₂ = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (mapCocone π₂ s)
rw₂ : (F.obj j).f ≫ (s.ι.app j).τ₂ = (F.obj j).f ≫ (c.ι.app j).τ₂ ≫ h₂.desc (mapCocone π₂ s)
rw₃ rw₄ : (F.obj j).f ≫ (s.ι.app j).τ₂ = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ Eq (α := (F.obj j).X₁ ⟶ s.pt.X₂) ((c.ι.app j).τ₁ ≫ h₁.desc (mapCocone π₁ s) ≫ s.pt.f : (F.obj j).X₁ ⟶ s.pt.X₂)
    ((c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (mapCocone π₂ s) : (F.obj j).X₁ ⟶ s.pt.X₂)

Tactic:
rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
⊢ ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)

Tactic:
have eq₂ := h₂.fac (π₂.mapCocone s)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
⊢ ∀ (j : J),
    Eq (α := (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₃ c)) j) (h₃.desc (mapCocone π₃ s)) :
        (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (NatTrans.app (Cocone.ι (mapCocone π₃ s)) j :
        (F ⋙ π₃).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))) j)

Tactic:
have eq₃ := h₃.fac (π₃.mapCocone s)
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
eq₃ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₃ c)) j) (h₃.desc (mapCocone π₃ s)) :
        (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (NatTrans.app (Cocone.ι (mapCocone π₃ s)) j :
        (F ⋙ π₃).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))) j)
⊢ ∀ (j : J), (c.ι.app j).τ₂ ≫ (obj (obj (const J) c.pt) j).g = (F.obj j).g ≫ (c.ι.app j).τ₃

Tactic:
have eq₂₃ := fun j => (c.ι.app j).comm₂₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
eq₃ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₃ c)) j) (h₃.desc (mapCocone π₃ s)) :
        (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (NatTrans.app (Cocone.ι (mapCocone π₃ s)) j :
        (F ⋙ π₃).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))) j)
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ (obj (obj (const J) c.pt) j).g = (F.obj j).g ≫ (c.ι.app j).τ₃
⊢ ∀ (j : J), (s.ι.app j).τ₂ ≫ (obj (obj (const J) s.pt) j).g = (F.obj j).g ≫ (s.ι.app j).τ₃

Tactic:
have eq₂₃' := fun j => (s.ι.app j).comm₂₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s)) :
        (F ⋙ π₂).obj j ⟶ Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))
      (NatTrans.app (Cocone.ι (mapCocone π₂ s)) j :
        (F ⋙ π₂).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ s))) j)
eq₃ :
  ∀ (j : J),
    Eq (α := (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ c))) j)
          (NatTrans.app (Cocone.ι (mapCocone π₃ c)) j) (h₃.desc (mapCocone π₃ s)) :
        (F ⋙ π₃).obj j ⟶ Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))
      (NatTrans.app (Cocone.ι (mapCocone π₃ s)) j :
        (F ⋙ π₃).obj j ⟶ obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₃) (mapCocone π₃ s))) j)
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ (obj (obj (const J) c.pt) j).g = (F.obj j).g ≫ (c.ι.app j).τ₃
eq₂₃' : ∀ (j : J), (s.ι.app j).τ₂ ≫ (obj (obj (const J) s.pt) j).g = (F.obj j).g ≫ (s.ι.app j).τ₃
dsimp :
  Eq (α := (F.obj j).X₂ ⟶ s.pt.X₃) ((c.ι.app j).τ₂ ≫ h₂.desc (mapCocone π₂ s) ≫ s.pt.g : (F.obj j).X₂ ⟶ s.pt.X₃)
    ((c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (mapCocone π₃ s) : (F.obj j).X₂ ⟶ s.pt.X₃)
⊢ Eq (α := (F ⋙ π₂).obj j ⟶ s.pt.X₃)
    (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
      (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (h₂.desc (mapCocone π₂ s) ≫ s.pt.g))
    (CategoryStruct.comp (Y := obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cocone.pt (F := F ⋙ π₂) (mapCocone π₂ c))) j)
      (NatTrans.app (Cocone.ι (mapCocone π₂ c)) j) (c.pt.g ≫ h₃.desc (mapCocone π₃ s)))

Tactic:
dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢
-- Module: Mathlib.Algebra.Homology.ShortComplex.Limits
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
inst_2 : HasZeroMorphisms.{v_2, u_2} C
F : J ⥤ ShortComplex.{v_2, u_2} C
c : Cocone F
h₁ : IsColimit (F := F ⋙ π₁) (mapCocone π₁ c)
h₂ : IsColimit (F := F ⋙ π₂) (mapCocone π₂ c)
h₃ : IsColimit (F := F ⋙ π₃) (mapCocone π₃ c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (mapCocone π₂ s) = (s.ι.app j).τ₂
eq₃ : ∀ (j : J), (c.ι.app j).τ₃ ≫ h₃.desc (mapCocone π₃ s) = (s.ι.app j).τ₃
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ c.pt.g = (F.obj j).g ≫ (c.ι.app j).τ₃
eq₂₃' : ∀ (j : J), (s.ι.app j).τ₂ ≫ s.pt.g = (F.obj j).g ≫ (s.ι.app j).τ₃
rw : (s.ι.app j).τ₂ ≫ s.pt.g = (c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (mapCocone π₃ s)
rw₁ : (F.obj j).g ≫ (s.ι.app j).τ₃ = (c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (mapCocone π₃ s)
rw₂ : (F.obj j).g ≫ (s.ι.app j).τ₃ = (F.obj j).g ≫ (c.ι.app j).τ₃ ≫ h₃.desc (mapCocone π₃ s)
rw₃ rw₄ : (F.obj j).g ≫ (s.ι.app j).τ₃ = (F.obj j).g ≫ (s.ι.app j).τ₃
⊢ Eq (α := (F.obj j).X₂ ⟶ s.pt.X₃) ((c.ι.app j).τ₂ ≫ h₂.desc (mapCocone π₂ s) ≫ s.pt.g : (F.obj j).X₂ ⟶ s.pt.X₃)
    ((c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (mapCocone π₃ s) : (F.obj j).X₂ ⟶ s.pt.X₃)

Tactic:
rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]