ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>α : CochainComplex.HomComplex.Cocycle K F 1<VAR>β : CochainComplex.HomComplex.Cochain K G 0<VAR>eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(CochainComplex.mappingCone.lift φ α β eq).f p = (↑α).v p q hpq ≫ (CochainComplex.mappingCone.inl φ).v q p ⋯ + β.v p p ⋯ ≫ (CochainComplex.mappingCone.inr φ).f p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>n' m' : ℤ<VAR>α' : CochainComplex.HomComplex.Cochain F L m'<VAR>β' : CochainComplex.HomComplex.Cochain G L n'<VAR>h : n + 1 = m<VAR>h' : m' + 1 = n'<VAR>p : ℤ<VAR>hp : n + n' = p<GOAL>(CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.descCochain φ α' β' h') hp = α.comp α' ⋯ + β.comp β' ⋯
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>n' m' : ℤ<VAR>α' : CochainComplex.HomComplex.Cochain F L m'<VAR>β' : CochainComplex.HomComplex.Cochain G L n'<VAR>h : n + 1 = m<VAR>h' : m' + 1 = n'<VAR>p : ℤ<VAR>hp : n + n' = p<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + n = p₂<VAR>h₂₃ : p₂ + n' = p₃<VAR>q : ℤ<VAR>hq : p₁ + m = q<GOAL>(CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (CochainComplex.mappingCone.descCochain φ α' β' h').v p₂ p₃ h₂₃ = α.v p₁ q hq ≫ α'.v q p₃ ⋯ + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>K L : CochainComplex C ℤ<VAR>α : CochainComplex.HomComplex.Cocycle K F 1<VAR>β : CochainComplex.HomComplex.Cochain K G 0<VAR>eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0<VAR>α' : CochainComplex.HomComplex.Cochain F L (-1)<VAR>β' : G ⟶ L<VAR>eq' : CochainComplex.HomComplex.δ (-1) 0 α' = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β')<VAR>n n' : ℤ<VAR>hnn' : n + 1 = n'<GOAL>(CochainComplex.mappingCone.lift φ α β eq).f n ≫ (CochainComplex.mappingCone.desc φ α' β' eq').f n = (↑α).v n n' hnn' ≫ α'.v n' n ⋯ + β.v n n ⋯ ≫ β'.f n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>H.Additive<VAR>HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>(CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm).hom = H.map ((↑(CochainComplex.mappingCone.fst φ)).v n m ⋯) ≫ (CochainComplex.mappingCone.inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯ + H.map ((CochainComplex.mappingCone.snd φ).v n n ⋯) ≫ (CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>H.Additive<VAR>HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>(CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm).inv = (↑(CochainComplex.mappingCone.fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯ ≫ H.map ((CochainComplex.mappingCone.inl φ).v m n ⋯) + (CochainComplex.mappingCone.snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫ H.map ((CochainComplex.mappingCone.inr φ).f n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>H.Additive<VAR>HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<VAR>n m : ℤ<VAR>hnm : n + 1 = m<GOAL>CochainComplex.mappingCone.mapHomologicalComplexXIso φ H n = CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n m hnm
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>H : C ⥤ D<VAR>H.Additive<VAR>HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)<GOAL>(H.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr φ) ≫ (CochainComplex.mappingCone.mapHomologicalComplexIso φ H).hom = CochainComplex.mappingCone.inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>i : Option ι<VAR>hi : i = none<GOAL>CategoryTheory.Limits.IsZero (HomologicalComplex.extend.X K i)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>i j : Option ι<VAR>hi : i = none<GOAL>HomologicalComplex.extend.d K i j = 0
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>i j : Option ι<VAR>hj : j = none<GOAL>HomologicalComplex.extend.d K i j = 0
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>i j : Option ι<VAR>a b : ι<VAR>hi : i = some a<VAR>hj : j = some b<GOAL>HomologicalComplex.extend.d K i j = (HomologicalComplex.extend.XIso K hi).hom ≫ K.d a b ≫ (HomologicalComplex.extend.XIso K hj).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>hi' : e.r i' = none<GOAL>CategoryTheory.Limits.IsZero ((K.extend e).X i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' : ι'<VAR>hi' : ∀ (i : ι), e.f i ≠ i'<GOAL>CategoryTheory.Limits.IsZero ((K.extend e).X i')
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>i j : ι<VAR>hi : e.f i = i'<VAR>hj : e.f j = j'<GOAL>(K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>i : ι<VAR>hi : e.f i = i'<VAR>hi' : ¬c.Rel i (c.next i)<GOAL>(K.extend e).d i' j' = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>j : ι<VAR>hj : e.f j = j'<VAR>hj' : ¬c.Rel (c.prev j) j<GOAL>(K.extend e).d i' j' = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>HomologicalComplex₂.toGradedObjectMap φ (i₁, i₂) = (φ.f i₁).f i₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<GOAL>∀ {X Y : HomologicalComplex₂ C c₁ c₂} (φ : X ⟶ Y) (i : I₁ × I₂), (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).map φ i = HomologicalComplex₂.toGradedObjectMap φ i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<GOAL>(HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).obj K = K.toGradedObject
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : CategoryTheory.GradedObject (I₁ × I₂) C<VAR>d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)<VAR>d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')<VAR>shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0<VAR>shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0<VAR>d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0<VAR>d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0<VAR>comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).X i₂ = X (i₁, i₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : CategoryTheory.GradedObject (I₁ × I₂) C<VAR>d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)<VAR>d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')<VAR>shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0<VAR>shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0<VAR>d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0<VAR>d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0<VAR>comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'<VAR>i₁ : I₁<VAR>i₂ i₂' : I₂<GOAL>((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).d i₂ i₂' = d₂ i₁ i₂ i₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : CategoryTheory.GradedObject (I₁ × I₂) C<VAR>d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)<VAR>d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')<VAR>shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0<VAR>shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0<VAR>d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0<VAR>d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0<VAR>comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'<VAR>i₁ i₁' : I₁<VAR>i₂ : I₂<GOAL>((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).d i₁ i₁').f i₂ = d₁ i₁ i₁' i₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : CategoryTheory.GradedObject (I₁ × I₂) C<VAR>d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)<VAR>d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')<VAR>shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0<VAR>shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0<VAR>d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0<VAR>d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0<VAR>comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'<GOAL>(HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).toGradedObject = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>f : K.toGradedObject ⟶ L.toGradedObject<VAR>comm₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), c₁.Rel i₁ i₁' → f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f (i₁', i₂)<VAR>comm₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), c₂.Rel i₂ i₂' → f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f (i₁, i₂')<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>((HomologicalComplex₂.homMk f comm₁ comm₂).f i₁).f i₂ = f (i₁, i₂)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i₁ i₁' : I₁<VAR>h : ¬c₁.Rel i₁ i₁'<VAR>i₂ : I₂<GOAL>(K.d i₁ i₁').f i₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i₁ i₁' i₁'' : I₁<VAR>i₂ : I₂<GOAL>(K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i₁ i₁' : I₁<VAR>i₂ i₂' : I₂<GOAL>(K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>f : K ⟶ L<VAR>i₁ i₁' : I₁<VAR>i₂ : I₂<GOAL>(f.f i₁).f i₂ ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ (f.f i₁').f i₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i : I₂<VAR>j : I₁<GOAL>(K.flip.X i).X j = (K.X j).X i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i : I₂<VAR>j j' : I₁<GOAL>(K.flip.X i).d j j' = (K.d j j').f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i i' : I₂<VAR>j : I₁<GOAL>(K.flip.d i i').f j = (K.X j).d i i'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<GOAL>K.flip.flip = K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L : HomologicalComplex₂ C c₁ c₂<VAR>f : K ⟶ L<VAR>i : I₂<VAR>j : I₁<GOAL>(((HomologicalComplex₂.flipFunctor C c₁ c₂).map f).f i).f j = (f.f j).f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<GOAL>(HomologicalComplex₂.flipFunctor C c₁ c₂).obj K = K.flip
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : HomologicalComplex₂ C c₁ c₂<VAR>i : I₁<GOAL>∀ (i_1 : I₂), (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).hom.app X).f i).f i_1 = 𝟙 ((X.X i).X i_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : HomologicalComplex₂ C c₁ c₂<VAR>i : I₁<GOAL>∀ (i_1 : I₂), (((HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂).inv.app X).f i).f i_1 = 𝟙 ((X.X i).X i_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : HomologicalComplex₂ C c₂ c₁<VAR>i : I₂<GOAL>∀ (i_1 : I₁), (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).inv.app X).f i).f i_1 = 𝟙 ((X.X i).X i_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>X : HomologicalComplex₂ C c₂ c₁<VAR>i : I₂<GOAL>∀ (i_1 : I₁), (((HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂).hom.app X).f i).f i_1 = 𝟙 ((X.X i).X i_1)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<GOAL>(HomologicalComplex₂.flipEquivalence C c₁ c₂).inverse = HomologicalComplex₂.flipFunctor C c₂ c₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<GOAL>(HomologicalComplex₂.flipEquivalence C c₁ c₂).unitIso = HomologicalComplex₂.flipEquivalenceUnitIso C c₁ c₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<GOAL>(HomologicalComplex₂.flipEquivalence C c₁ c₂).functor = HomologicalComplex₂.flipFunctor C c₁ c₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<GOAL>(HomologicalComplex₂.flipEquivalence C c₁ c₂).counitIso = HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>HomologicalComplex₂.XXIsoOfEq C c₁ c₂ K ⋯ ⋯ = CategoryTheory.Iso.refl ((K.X i₁).X i₂)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernel g<VAR>w : f ≫ g = 0<GOAL>CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernel g<VAR>w : f ≫ g = 0<VAR>h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g<GOAL>(CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernel g<VAR>w : f ≫ g = 0<GOAL>imageToKernel f g w ≫ (CategoryTheory.Limits.kernelSubobject g).arrow = (CategoryTheory.Limits.imageSubobject f).arrow
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernel g<VAR>CategoryTheory.ConcreteCategory V<VAR>w : f ≫ g = 0<VAR>x : (CategoryTheory.forget V).obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f))<GOAL>(CategoryTheory.Limits.kernelSubobject g).arrow ((imageToKernel f g w) x) = (CategoryTheory.Limits.imageSubobject f).arrow x
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernel g<VAR>w : f ≫ g = 0<GOAL>CategoryTheory.Limits.factorThruImageSubobject f ≫ imageToKernel f g w = CategoryTheory.Limits.factorThruKernelSubobject g f w
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasZeroObject V<VAR>w : 0 ≫ g = 0<GOAL>imageToKernel 0 g w = 0
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImages V<VAR>w : f ≫ 0 = 0<GOAL>imageToKernel f 0 w = (CategoryTheory.Limits.imageSubobject f).arrow ≫ CategoryTheory.inv (CategoryTheory.Limits.kernelSubobject 0).arrow
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasImages V<VAR>D : V<VAR>h : C ⟶ D<VAR>w : f ≫ g = 0<GOAL>imageToKernel f (g ≫ h) ⋯ = imageToKernel f g w ≫ (CategoryTheory.Limits.kernelSubobject g).ofLE (CategoryTheory.Limits.kernelSubobject (g ≫ h)) ⋯
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasImages V<VAR>Z : V<VAR>h : Z ⟶ A<VAR>w : f ≫ g = 0<GOAL>imageToKernel (h ≫ f) g ⋯ = (CategoryTheory.Limits.imageSubobject (h ≫ f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯ ≫ imageToKernel f g w
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>g : B ⟶ C<VAR>CategoryTheory.Limits.HasKernels V<VAR>CategoryTheory.Limits.HasImages V<VAR>D : V<VAR>h : C ⟶ D<VAR>CategoryTheory.Mono h<VAR>w : f ≫ g ≫ h = 0<GOAL>imageToKernel f (g ≫ h) w = imageToKernel f g ⋯ ≫ ((CategoryTheory.Limits.kernelSubobject (g ≫ h)).isoOfEq (CategoryTheory.Limits.kernelSubobject g) ⋯).inv