awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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
⊢ 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))
have 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))
Tactic: rw [(F.obj j).shape _ _ h, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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))
⊢ 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))
have 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))
Tactic: rw [(F.obj j).shape _ _ h, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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))
⊢ 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))
have w₂ : Eq.{v_1 + 1} (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) 0 0
Tactic: rw [(F.obj j).shape _ _ h, comp_zero, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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
⊢ 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 φ)
have 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 := sorry :
                      NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
                shape := sorry, d_comp_d' := sorry : 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 := sorry :
                    NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
              shape := sorry, d_comp_d' := sorry : HomologicalComplex.{v_1, u_1, u_2} C c })
          φ ≫
        { f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) j, comm' := sorry })
      n)
    (Hom.f ({ f := fun (x : ι) ↦ limit.π (F ⋙ eval C c x) i, comm' := sorry } ≫ F.map φ) n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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 : ι
⊢ 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)
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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 : ι
⊢ 𝟙 (limit (F ⋙ eval C c n)) ≫ limit.π (F ⋙ eval C c n) j = limit.π (F ⋙ eval C c n) i ≫ (F.map φ).f n
have 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)
Tactic: simp only [Category.id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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 : ι
⊢ 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)
have 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 φ))
Tactic: rw [← eval_map, ← Functor.comp_map, limit.w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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 φ))
⊢ 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)
have 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 φ)
Tactic: rw [← eval_map, ← Functor.comp_map, limit.w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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 φ)
⊢ 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)
have 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)
Tactic: rw [← eval_map, ← Functor.comp_map, limit.w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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 (φ.f n)
have change : Mono (X := Functor.obj (eval C c n) K) (CategoryTheory.Functor.map (eval C c n) φ)
Tactic: change Mono ((HomologicalComplex.eval C c n).map φ)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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'
⊢ 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')
have 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)))
Tactic: apply IsColimit.hom_ext (hs i)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (hypothesis)
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 (α := (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)))
have eq : ∀ (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)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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
⊢ 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)))
have 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')
Tactic: simp only [Functor.mapCocone_ι_app, eval_map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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
⊢ 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')
have 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)
Tactic: rw [reassoc_of% (eq i), Hom.comm_assoc, eq i', Hom.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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)
⊢ 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')
have 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)
Tactic: rw [reassoc_of% (eq i), Hom.comm_assoc, eq i', Hom.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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)
⊢ 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')
have rw₂ : (t.ι.app j).f i ≫ t.pt.d i i' = (F.obj j).d i i' ≫ (t.ι.app j).f i'
Tactic: rw [reassoc_of% (eq i), Hom.comm_assoc, eq i', Hom.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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'
⊢ 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')
have rw₃ : (F.obj j).d i i' ≫ (t.ι.app j).f i' = (F.obj j).d i i' ≫ (t.ι.app j).f i'
Tactic: rw [reassoc_of% (eq i), Hom.comm_assoc, eq i', Hom.comm]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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
⊢ s.ι.app j ≫ { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ } = t.ι.app j
have h : ∀ (i : ι),
  Hom.f (s.ι.app j ≫ { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := sorry }) i =
    (t.ι.app j).f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
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
⊢ m = { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ }
have h : ∀ (i : ι), m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := sorry } i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cocone F
hs : (i : ι) → IsColimit (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
⊢ m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).desc (Functor.mapCocone (eval C c i) t), comm' := ⋯ } i
have h : ∀ (j : J),
  Eq (α := (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
    (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j ≫ m.f i :
      (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
    (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) t)) j :
      (F ⋙ eval C c i).obj j ⟶
        Functor.obj.{v_2, v_1, u_3, u_1}
          (Functor.obj (Functor.const J) (Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))) j)
Tactic: apply (hs i).uniq ((eval C c i).mapCocone t)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
s : Cocone F
hs : (i : ι) → IsColimit (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
j : J
⊢ Eq (α := (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
    (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) s)) j ≫ m.f i :
      (F ⋙ eval C c i).obj j ⟶ Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))
    (NatTrans.app (Cocone.ι (Functor.mapCocone (eval C c i) t)) j :
      (F ⋙ eval C c i).obj j ⟶
        Functor.obj.{v_2, v_1, u_3, u_1}
          (Functor.obj (Functor.const J) (Cocone.pt (F := F ⋙ eval C c i) (Functor.mapCocone (eval C c i) t))) j)
have h : (s.ι.app j).f i ≫ m.f i = (t.ι.app j).f i
Tactic: dsimp