awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
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 (α := (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)))
have eq₁₂' : ∀ (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₁₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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).τ₂
⊢ 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)))
have 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₂)
Tactic: dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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).τ₂
⊢ 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₂)
have rw : (s.ι.app j).τ₁ ≫ s.pt.f = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (mapCocone π₂ s)
Tactic: rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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)
⊢ 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₂)
have rw₁ : (F.obj j).f ≫ (s.ι.app j).τ₂ = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (mapCocone π₂ s)
Tactic: rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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)
⊢ 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₂)
have rw₂ : (F.obj j).f ≫ (s.ι.app j).τ₂ = (F.obj j).f ≫ (c.ι.app j).τ₂ ≫ h₂.desc (mapCocone π₂ s)
Tactic: rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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)
⊢ 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₂)
have rw₃ : (F.obj j).f ≫ (s.ι.app j).τ₂ = (F.obj j).f ≫ (s.ι.app j).τ₂
Tactic: rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
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 (α := (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)))
have 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)
Tactic: have eq₂ := h₂.fac (π₂.mapCocone s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
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 (α := (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)))
have 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)
Tactic: have eq₃ := h₃.fac (π₃.mapCocone s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
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 (α := (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)))
have eq₂₃ : ∀ (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₂₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (hypothesis)
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 (α := (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)))
have eq₂₃' : ∀ (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₂₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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).τ₃
⊢ 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)))
have 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₃)
Tactic: dsimp at eq₂ eq₃ eq₂₃ eq₂₃' ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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).τ₃
⊢ 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₃)
have rw : (s.ι.app j).τ₂ ≫ s.pt.g = (c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (mapCocone π₃ s)
Tactic: rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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)
⊢ 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₃)
have rw₁ : (F.obj j).g ≫ (s.ι.app j).τ₃ = (c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (mapCocone π₃ s)
Tactic: rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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)
⊢ 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₃)
have rw₂ : (F.obj j).g ≫ (s.ι.app j).τ₃ = (F.obj j).g ≫ (c.ι.app j).τ₃ ≫ h₃.desc (mapCocone π₃ s)
Tactic: rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Limits (goal)
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)
⊢ 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₃)
have rw₃ : (F.obj j).g ≫ (s.ι.app j).τ₃ = (F.obj j).g ≫ (s.ι.app j).τ₃
Tactic: rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]