awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
⊢ f = g ↔
    Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
      Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
have refine : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
    Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g) →
  ∀ (h₁ : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g))
    (h₂ : Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)), f = g
Tactic: refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
h :
  Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g) ∧
    Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
h₁ : Eq (α := K.X i ⟶ A) (Hom.f biprod.inl i ≫ f) (Hom.f biprod.inl i ≫ g)
h₂ : Eq (α := L.X i ⟶ A) (Hom.f biprod.inr i ≫ f) (Hom.f biprod.inr i ≫ g)
⊢ f = g
have rw : 𝟙 ((K ⊞ L).X i) ≫ f = 𝟙 ((K ⊞ L).X i) ≫ g
Tactic: rw [← cancel_epi (𝟙 _)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
⊢ f = g ↔
    Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
      Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
have refine : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
    Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i) →
  ∀ (h₁ : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i))
    (h₂ : Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)), f = g
Tactic: refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
A : C
i : ι
f g : A ⟶ (K ⊞ L).X i
h :
  Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i) ∧
    Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
h₁ : Eq (α := A ⟶ K.X i) (f ≫ Hom.f biprod.fst i) (g ≫ Hom.f biprod.fst i)
h₂ : Eq (α := A ⟶ L.X i) (f ≫ Hom.f biprod.snd i) (g ≫ Hom.f biprod.snd i)
⊢ f = g
have rw : f ≫ 𝟙 ((K ⊞ L).X i) = g ≫ 𝟙 ((K ⊞ L).X i)
Tactic: rw [← cancel_mono (𝟙 _)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f (biprod.desc α β) i) = α.f i
have rw : (CategoryStruct.comp (Y := K ⊞ L) biprod.inl (biprod.desc α β)).f i = α.f i
Tactic: rw [← comp_f, biprod.inl_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : K ⟶ M
β : L ⟶ M
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) biprod.inl (biprod.desc α β)).f i = α.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inl i) (Hom.f (biprod.desc α β) i) = α.f i
have rw₁ : α.f i = α.f i
Tactic: rw [← comp_f, biprod.inl_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f (biprod.desc α β) i) = β.f i
have rw : (CategoryStruct.comp (Y := K ⊞ L) biprod.inr (biprod.desc α β)).f i = β.f i
Tactic: rw [← comp_f, biprod.inr_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : K ⟶ M
β : L ⟶ M
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) biprod.inr (biprod.desc α β)).f i = β.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f biprod.inr i) (Hom.f (biprod.desc α β) i) = β.f i
have rw₁ : β.f i = β.f i
Tactic: rw [← comp_f, biprod.inr_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f (biprod.lift α β) i) (Hom.f biprod.fst i) = α.f i
have rw : (CategoryStruct.comp (Y := K ⊞ L) (biprod.lift α β) biprod.fst).f i = α.f i
Tactic: rw [← comp_f, biprod.lift_fst]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : M ⟶ K
β : M ⟶ L
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) (biprod.lift α β) biprod.fst).f i = α.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f (biprod.lift α β) i) (Hom.f biprod.fst i) = α.f i
have rw₁ : α.f i = α.f i
Tactic: rw [← comp_f, biprod.lift_fst]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f (biprod.lift α β) i) (Hom.f biprod.snd i) = β.f i
have rw : (CategoryStruct.comp (Y := K ⊞ L) (biprod.lift α β) biprod.snd).f i = β.f i
Tactic: rw [← comp_f, biprod.lift_snd]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexBiprod (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (L.X i)
M : HomologicalComplex.{v_1, u_1, u_2} C c
α : M ⟶ K
β : M ⟶ L
i : ι
rw : (CategoryStruct.comp (Y := K ⊞ L) (biprod.lift α β) biprod.snd).f i = β.f i
⊢ CategoryStruct.comp (Y := (K ⊞ L).X i) (Hom.f (biprod.lift α β) i) (Hom.f biprod.snd i) = β.f i
have rw₁ : β.f i = β.f i
Tactic: rw [← comp_f, biprod.lift_snd]
-- 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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
⊢ Eq (α := t.pt.X i ⟶ s.pt.X i') ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')
have apply : ∀ (j : J),
  Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
Tactic: apply IsLimit.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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
have eq : ∀ (k : ι) (j : J),
  Eq (α := Cone.pt (F := F ⋙ eval C c k) (Functor.mapCone (eval C c k) t) ⟶ (F ⋙ eval C c k).obj j)
    ((hs k).lift (Functor.mapCone (eval C c k) t) ≫ NatTrans.app (Cone.π (Functor.mapCone (eval C c k) s)) j)
    (NatTrans.app (Cone.π (Functor.mapCone (eval C c k) t)) j)
Tactic: have eq := fun k => (hs k).fac ((eval C c k).mapCone 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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (CategoryStruct.comp (Y := Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))
        (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) : t.pt.X i ⟶ s.pt.X i')
        (NatTrans.app (Cone.π (Functor.mapCone (eval C c i') s)) j :
          Functor.obj.{v_2, v_1, u_3, u_1}
              (Functor.obj (Functor.const J) (Cone.pt (F := F ⋙ eval C c i') (Functor.mapCone (eval C c i') s))) j ⟶
            (F ⋙ eval C c i').obj j) :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
have simp : Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
  ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
  (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
Tactic: simp only [Functor.mapCone_π_app, eval_map, assoc]
-- 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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
have rw : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
Tactic: rw [eq i', ← Hom.comm, reassoc_of% (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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
rw : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
have rw₁ : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ (s.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
Tactic: rw [eq i', ← Hom.comm, reassoc_of% (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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
rw : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
rw₁ : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ (s.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
have rw₂ : (t.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
Tactic: rw [eq i', ← Hom.comm, reassoc_of% (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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
i i' : ι
h : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (hs k).lift (Functor.mapCone (eval C c k) t) ≫ (s.π.app j).f k = (t.π.app j).f k
rw : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
rw₁ : (hs i).lift (Functor.mapCone (eval C c i) t) ≫ (s.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
rw₂ : (t.π.app j).f i ≫ (F.obj j).d i i' = t.pt.d i i' ≫ (t.π.app j).f i'
⊢ Eq (α := t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    ((hs i).lift (Functor.mapCone (eval C c i) t) ≫ s.pt.d i i' ≫ (s.π.app j).f i' : t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
    (t.pt.d i i' ≫ (hs i').lift (Functor.mapCone (eval C c i') t) ≫ (s.π.app j).f i' :
      t.pt.X i ⟶ (F ⋙ eval C c i').obj j)
have rw₃ : t.pt.d i i' ≫ (t.π.app j).f i' = t.pt.d i i' ≫ (t.π.app j).f i'
Tactic: rw [eq i', ← Hom.comm, reassoc_of% (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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
j : J
⊢ { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } ≫ s.π.app j = t.π.app j
have h : ∀ (i : ι),
  Hom.f ({ f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := sorry } ≫ s.π.app j) 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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
⊢ m = { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ }
have h : ∀ (i : ι), m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
⊢ m.f i = Hom.f { f := fun (i : ι) ↦ (hs i).lift (Functor.mapCone (eval C c i) t), comm' := ⋯ } i
have h : ∀ (j : J),
  Eq (α := Cone.pt (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) t) ⟶ (F ⋙ eval C c i).obj j)
    (m.f i ≫ NatTrans.app (Cone.π (Functor.mapCone (eval C c i) s)) j)
    (NatTrans.app (Cone.π (Functor.mapCone (eval C c i) t)) j)
Tactic: apply (hs i).uniq ((eval C c i).mapCone 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 : Cone F
hs : (i : ι) → IsLimit (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
j : J
⊢ Eq (α := Cone.pt (F := F ⋙ eval C c i) (Functor.mapCone (eval C c i) t) ⟶ (F ⋙ eval C c i).obj j)
    (m.f i ≫ NatTrans.app (Cone.π (Functor.mapCone (eval C c i) s)) j)
    (NatTrans.app (Cone.π (Functor.mapCone (eval C c i) t)) j)
have h : m.f i ≫ (s.π.app j).f i = (t.π.app j).f i
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)
n m : ι
h : ¬c.Rel n m
⊢ Eq.{v_1 + 1} (α := limit (F ⋙ eval C c n) ⟶ limit (F ⋙ eval C c m))
    (limMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }) 0
have w : ∀ (j : J),
  Eq (α := limit (F ⋙ eval C c n) ⟶ (F ⋙ eval C c m).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m))
      (limMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := sorry }) (limit.π (F ⋙ eval C c m) j))
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
Tactic: ext j
-- 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 ⋙ eval C c m).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m))
      (limMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }) (limit.π (F ⋙ eval C c m) j))
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
have w : Eq (α := limit (F ⋙ eval C c n) ⟶ (F ⋙ eval C c m).obj j)
  (limit.π (F ⋙ eval C c n) j ≫ NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := sorry } j)
  (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
Tactic: rw [limMap_π]
-- 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 ⋙ eval C c m).obj j)
    (limit.π (F ⋙ eval C c n) j ≫ NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ } j)
    (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
have w : Eq (α := limit (F ⋙ eval C c n) ⟶ (F.obj j).X m) (limit.π (F ⋙ eval C c n) j ≫ (F.obj j).d n m)
  (CategoryStruct.comp (Y := limit (F ⋙ eval C c m)) 0 (limit.π (F ⋙ eval C c m) j))
Tactic: dsimp