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
c : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₁) (mapCone π₁ s) ⟶ (F ⋙ π₁).obj j)
      (h₁.lift (mapCone π₁ s) ≫ NatTrans.app (Cone.π (mapCone π₁ c)) j) (NatTrans.app (Cone.π (mapCone π₁ s)) j)
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) c.pt) j).f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = (obj (obj (const J) s.pt) j).f ≫ (s.π.app j).τ₂
dsimp : (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
⊢ Eq (α := s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (h₁.lift (mapCone π₁ s) ≫ c.pt.f : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))
        (s.pt.f ≫ h₂.lift (mapCone π₂ s) : s.pt.X₁ ⟶ c.pt.X₂)
        (NatTrans.app (Cone.π (mapCone π₂ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₂) (mapCone π₂ c))) j ⟶ (F ⋙ π₂).obj j) :
      s.pt.X₁ ⟶ (F ⋙ π₂).obj j)

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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₁ : ∀ (j : J), h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ = (s.π.app j).τ₁
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₁₂ : ∀ (j : J), (c.π.app j).τ₁ ≫ (F.obj j).f = c.pt.f ≫ (c.π.app j).τ₂
eq₁₂' : ∀ (j : J), (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw : h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂
rw₁ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ c.pt.f ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₂ :
  Eq (α := s.pt.X₁ ⟶ (F.obj j).X₂) (h₁.lift (mapCone π₁ s) ≫ (c.π.app j).τ₁ ≫ (F.obj j).f : s.pt.X₁ ⟶ (F.obj j).X₂)
    (s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ : s.pt.X₁ ⟶ (F.obj j).X₂)
rw₃ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂
rw₄ : (s.π.app j).τ₁ ≫ (F.obj j).f = s.pt.f ≫ (s.π.app j).τ₂
rw₅ rw₆ : s.pt.f ≫ (s.π.app j).τ₂ = s.pt.f ≫ (s.π.app j).τ₂
⊢ (h₁.lift (mapCone π₁ s) ≫ c.pt.f) ≫ (c.π.app j).τ₂ = (s.pt.f ≫ h₂.lift (mapCone π₂ s)) ≫ (c.π.app j).τ₂

Tactic:
rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']

Premises used: CategoryTheory.Category.assoc
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)

Tactic:
have eq₂ := h₂.fac (π₂.mapCone 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
⊢ ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)

Tactic:
have eq₃ := h₃.fac (π₃.mapCone 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₃ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
⊢ ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) c.pt) 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₃ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) c.pt) j).g ≫ (c.π.app j).τ₃
⊢ ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) s.pt) 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₂) (mapCone π₂ s) ⟶ (F ⋙ π₂).obj j)
      (h₂.lift (mapCone π₂ s) ≫ NatTrans.app (Cone.π (mapCone π₂ c)) j) (NatTrans.app (Cone.π (mapCone π₂ s)) j)
eq₃ :
  ∀ (j : J),
    Eq (α := Cone.pt (F := F ⋙ π₃) (mapCone π₃ s) ⟶ (F ⋙ π₃).obj j)
      (h₃.lift (mapCone π₃ s) ≫ NatTrans.app (Cone.π (mapCone π₃ c)) j) (NatTrans.app (Cone.π (mapCone π₃ s)) j)
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) c.pt) j).g ≫ (c.π.app j).τ₃
eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = (obj (obj (const J) s.pt) j).g ≫ (s.π.app j).τ₃
dsimp : (h₂.lift (mapCone π₂ s) ≫ c.pt.g) ≫ (c.π.app j).τ₃ = (s.pt.g ≫ h₃.lift (mapCone π₃ s)) ≫ (c.π.app j).τ₃
⊢ Eq (α := s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (h₂.lift (mapCone π₂ s) ≫ c.pt.g : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))
        (s.pt.g ≫ h₃.lift (mapCone π₃ s) : s.pt.X₂ ⟶ c.pt.X₃)
        (NatTrans.app (Cone.π (mapCone π₃ c)) j :
          obj.{v_1, v_2, u_1, u_2} (obj (const J) (Cone.pt (F := F ⋙ π₃) (mapCone π₃ c))) j ⟶ (F ⋙ π₃).obj j) :
      s.pt.X₂ ⟶ (F ⋙ π₃).obj j)

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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
eq₂ : ∀ (j : J), h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ = (s.π.app j).τ₂
eq₃ : ∀ (j : J), h₃.lift (mapCone π₃ s) ≫ (c.π.app j).τ₃ = (s.π.app j).τ₃
eq₂₃ : ∀ (j : J), (c.π.app j).τ₂ ≫ (F.obj j).g = c.pt.g ≫ (c.π.app j).τ₃
eq₂₃' : ∀ (j : J), (s.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ (s.π.app j).τ₃
rw : h₂.lift (mapCone π₂ s) ≫ c.pt.g ≫ (c.π.app j).τ₃ = (s.pt.g ≫ h₃.lift (mapCone π₃ s)) ≫ (c.π.app j).τ₃
rw₁ :
  Eq (α := s.pt.X₂ ⟶ (F.obj j).X₃) (h₂.lift (mapCone π₂ s) ≫ c.pt.g ≫ (c.π.app j).τ₃ : s.pt.X₂ ⟶ (F.obj j).X₃)
    (s.pt.g ≫ h₃.lift (mapCone π₃ s) ≫ (c.π.app j).τ₃ : s.pt.X₂ ⟶ (F.obj j).X₃)
rw₂ :
  Eq (α := s.pt.X₂ ⟶ (F.obj j).X₃) (h₂.lift (mapCone π₂ s) ≫ (c.π.app j).τ₂ ≫ (F.obj j).g : s.pt.X₂ ⟶ (F.obj j).X₃)
    (s.pt.g ≫ h₃.lift (mapCone π₃ s) ≫ (c.π.app j).τ₃ : s.pt.X₂ ⟶ (F.obj j).X₃)
rw₃ : (s.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ h₃.lift (mapCone π₃ s) ≫ (c.π.app j).τ₃
rw₄ : (s.π.app j).τ₂ ≫ (F.obj j).g = s.pt.g ≫ (s.π.app j).τ₃
rw₅ rw₆ : s.pt.g ≫ (s.π.app j).τ₃ = s.pt.g ≫ (s.π.app j).τ₃
⊢ (h₂.lift (mapCone π₂ s) ≫ c.pt.g) ≫ (c.π.app j).τ₃ = (s.pt.g ≫ h₃.lift (mapCone π₃ s)) ≫ (c.π.app j).τ₃

Tactic:
rw [assoc, assoc, ← eq₂₃, reassoc_of% eq₂, eq₃, eq₂₃']

Premises used: CategoryTheory.Category.assoc
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
h₄ :
  Hom.τ₁
      ({ τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j) =
    (s.π.app j).τ₁
h₅ :
  Hom.τ₂
      ({ τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j) =
    (s.π.app j).τ₂
h₆ :
  Hom.τ₃
      ({ τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j) =
    (s.π.app j).τ₃
⊢ { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ } ≫
      c.π.app j =
    s.π.app j

Tactic:
ext
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ Hom.τ₁
      ({ τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j) =
    (s.π.app j).τ₁

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ Hom.τ₂
      ({ τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j) =
    (s.π.app j).τ₂

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
j : J
⊢ Hom.τ₃
      ({ τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ } ≫
        c.π.app j) =
    (s.π.app j).τ₃

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
h₄ :
  m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
h₅ :
  m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
h₆ :
  m.τ₃ =
    Hom.τ₃
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }
⊢ m =
    { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
      comm₂₃ := ⋯ }

Tactic:
ext
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
h₁.uniq (π₁.mapCone s) _ (fun j => π₁.congr_map (hm j))

Premises used: CategoryTheory.ShortComplex.π₁, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Functor.mapCone
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₁ =
    Hom.τ₁
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
exact h₁.uniq (π₁.mapCone s) _ (fun j => π₁.congr_map (hm j))

Premises used: CategoryTheory.ShortComplex.π₁, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Functor.mapCone
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
h₂.uniq (π₂.mapCone s) _ (fun j => π₂.congr_map (hm j))

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Functor.mapCone, CategoryTheory.ShortComplex.π₂
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₂ =
    Hom.τ₂
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
exact h₂.uniq (π₂.mapCone s) _ (fun j => π₂.congr_map (hm j))

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Functor.mapCone, CategoryTheory.ShortComplex.π₂
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₃ =
    Hom.τ₃
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
h₃.uniq (π₃.mapCone s) _ (fun j => π₃.congr_map (hm j))

Premises used: CategoryTheory.ShortComplex.π₃, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Functor.mapCone
-- 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 : Cone F
h₁ : IsLimit (F := F ⋙ π₁) (mapCone π₁ c)
h₂ : IsLimit (F := F ⋙ π₂) (mapCone π₂ c)
h₃ : IsLimit (F := F ⋙ π₃) (mapCone π₃ c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₃ =
    Hom.τ₃
      { τ₁ := h₁.lift (mapCone π₁ s), τ₂ := h₂.lift (mapCone π₂ s), τ₃ := h₃.lift (mapCone π₃ s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }

Tactic:
exact h₃.uniq (π₃.mapCone s) _ (fun j => π₃.congr_map (hm j))

Premises used: CategoryTheory.ShortComplex.π₃, CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.Functor.congr_map, CategoryTheory.Functor.mapCone
-- 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 ⋙ π₃)
j : J
⊢ limit.π (F ⋙ π₁) j ≫ (F.obj j).f =
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          j).f ≫
      limit.π (F ⋙ π₂) j

Tactic:
simp
-- 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 ⋙ π₃)
j : J
⊢ limit.π (F ⋙ π₂) j ≫ (F.obj j).g =
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          j).g ≫
      limit.π (F ⋙ π₃) j

Tactic:
simp
-- 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 ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x).X₁ ⟶
      (F.obj x_1).X₁)
    (Hom.τ₁
      (Functor.map
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₁
      ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f))

Tactic:
simp [← limit.w _ f]

Premises used: CategoryTheory.Limits.limit.w
-- 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 ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x).X₂ ⟶
      (F.obj x_1).X₂)
    (Hom.τ₂
      (Functor.map
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₂
      ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f))

Tactic:
simp [← limit.w _ f]

Premises used: CategoryTheory.Limits.limit.w
-- 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 ⋙ π₃)
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α :=
    (obj
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          x).X₃ ⟶
      (F.obj x_1).X₃)
    (Hom.τ₃
      (Functor.map
          (obj (const J)
            (mk (X₁ := limit (F ⋙ π₁)) (X₂ := limit (F ⋙ π₂)) (X₃ := limit (F ⋙ π₃)) (limMap (F.whiskerLeft π₁Toπ₂))
              (limMap (F.whiskerLeft π₂Toπ₃)) ⋯))
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x_1, τ₂ := limit.π (F ⋙ π₂) x_1, τ₃ := limit.π (F ⋙ π₃) x_1, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }))
    (Hom.τ₃
      ({ τ₁ := limit.π (F ⋙ π₁) x, τ₂ := limit.π (F ⋙ π₂) x, τ₃ := limit.π (F ⋙ π₃) x, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f))

Tactic:
simp [← limit.w _ f]

Premises used: CategoryTheory.Limits.limit.w
-- 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 ⋙ π₃)
⊢ HasLimit F

Tactic:
⟨⟨⟨_, isLimitLimitCone _⟩⟩⟩

Premises used: CategoryTheory.ShortComplex.isLimitLimitCone, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk