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>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel j i<VAR>A : C<VAR>f g : HomologicalComplex.homotopyCofiber.X φ j ⟶ A<VAR>h₁ : HomologicalComplex.homotopyCofiber.inlX φ i j hij ≫ f = HomologicalComplex.homotopyCofiber.inlX φ i j hij ≫ g<VAR>h₂ : HomologicalComplex.homotopyCofiber.inrX φ j ≫ f = HomologicalComplex.homotopyCofiber.inrX φ j ≫ g<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i : ι<VAR>hi : ¬c.Rel i (c.next i)<VAR>A : C<VAR>f g : HomologicalComplex.homotopyCofiber.X φ i ⟶ A<VAR>h : HomologicalComplex.homotopyCofiber.inrX φ i ≫ f = HomologicalComplex.homotopyCofiber.inrX φ i ≫ g<GOAL>f = g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>HomologicalComplex.homotopyCofiber.d φ i j ≫ HomologicalComplex.homotopyCofiber.fstX φ j k hjk = -HomologicalComplex.homotopyCofiber.fstX φ i j hij ≫ F.d j k
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>HomologicalComplex.homotopyCofiber.d φ i j ≫ HomologicalComplex.homotopyCofiber.sndX φ j = HomologicalComplex.homotopyCofiber.fstX φ i j hij ≫ φ.f j + HomologicalComplex.homotopyCofiber.sndX φ i ≫ G.d i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>HomologicalComplex.homotopyCofiber.inlX φ j i hij ≫ HomologicalComplex.homotopyCofiber.d φ i j = -F.d j k ≫ HomologicalComplex.homotopyCofiber.inlX φ k j hjk + φ.f j ≫ HomologicalComplex.homotopyCofiber.inrX φ j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>hj : ¬c.Rel j (c.next j)<GOAL>HomologicalComplex.homotopyCofiber.inlX φ j i hij ≫ HomologicalComplex.homotopyCofiber.d φ i j = φ.f j ≫ HomologicalComplex.homotopyCofiber.inrX φ j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<VAR>hij : ¬c.Rel i j<GOAL>HomologicalComplex.homotopyCofiber.d φ i j = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<GOAL>HomologicalComplex.homotopyCofiber.inrX φ i ≫ HomologicalComplex.homotopyCofiber.d φ i j = G.d i j ≫ HomologicalComplex.homotopyCofiber.inrX φ j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i j : ι<GOAL>(HomologicalComplex.homotopyCofiber φ).d i j = HomologicalComplex.homotopyCofiber.d φ i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i : ι<GOAL>(HomologicalComplex.homotopyCofiber φ).X i = HomologicalComplex.homotopyCofiber.X φ i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>i : ι<GOAL>(HomologicalComplex.homotopyCofiber.inr φ).f i = HomologicalComplex.homotopyCofiber.inrX φ i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>(HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j = HomologicalComplex.homotopyCofiber.inlX φ i j hij
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>i j : ι<VAR>hij : ¬c.Rel j i<GOAL>(HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>j k : ι<VAR>hjk : c.Rel j k<GOAL>(HomologicalComplex.homotopyCofiber.desc φ α hα).f j = HomologicalComplex.homotopyCofiber.fstX φ j k hjk ≫ hα.hom k j + HomologicalComplex.homotopyCofiber.sndX φ j ≫ α.f j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>j : ι<VAR>hj : ¬c.Rel j (c.next j)<GOAL>(HomologicalComplex.homotopyCofiber.desc φ α hα).f j = HomologicalComplex.homotopyCofiber.sndX φ j ≫ α.f j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>i j : ι<VAR>hjk : c.Rel j i<GOAL>HomologicalComplex.homotopyCofiber.inlX φ i j hjk ≫ (HomologicalComplex.homotopyCofiber.desc φ α hα).f j = hα.hom i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>i : ι<GOAL>HomologicalComplex.homotopyCofiber.inrX φ i ≫ (HomologicalComplex.homotopyCofiber.desc φ α hα).f i = α.f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<GOAL>HomologicalComplex.homotopyCofiber.inr φ ≫ HomologicalComplex.homotopyCofiber.desc φ α hα = α
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>α : G ⟶ K<VAR>hα : Homotopy (φ ≫ α) 0<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>i j : ι<GOAL>(HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).hom i j ≫ (HomologicalComplex.homotopyCofiber.desc φ α hα).f j = hα.hom i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>DecidableRel c.Rel<VAR>f : HomologicalComplex.homotopyCofiber φ ⟶ K<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<GOAL>f = HomologicalComplex.homotopyCofiber.desc φ (HomologicalComplex.homotopyCofiber.inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((HomologicalComplex.homotopyCofiber.inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>DecidableRel c.Rel<VAR>K : HomologicalComplex C c<VAR>x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0<GOAL>x = y ↔ x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>φ₀ φ₁ : K ⟶ F<VAR>h : Homotopy φ₀ φ₁<GOAL>HomologicalComplex.cylinder.ι₀ K ≫ HomologicalComplex.cylinder.desc φ₀ φ₁ h = φ₀
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>φ₀ φ₁ : K ⟶ F<VAR>h : Homotopy φ₀ φ₁<GOAL>HomologicalComplex.cylinder.ι₁ K ≫ HomologicalComplex.cylinder.desc φ₀ φ₁ h = φ₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<GOAL>HomologicalComplex.cylinder.ι₀ K ≫ HomologicalComplex.cylinder.π K = 𝟙 K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<GOAL>HomologicalComplex.cylinder.ι₁ K ≫ HomologicalComplex.cylinder.π K = 𝟙 K
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>HomologicalComplex.cylinder.inlX K i j hij ≫ (HomologicalComplex.cylinder.π K).f j = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>i : ι<GOAL>HomologicalComplex.cylinder.inrX K i ≫ (HomologicalComplex.cylinder.π K).f i = (CategoryTheory.Limits.biprod.desc (𝟙 K) (𝟙 K)).f i
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>i j : ι<VAR>hij : c.Rel j i<GOAL>HomologicalComplex.cylinder.inlX K i j hij ≫ (HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j = HomologicalComplex.cylinder.inlX K i j hij ≫ (HomologicalComplex.cylinder.π K ≫ HomologicalComplex.cylinder.ι₀ K - 𝟙 K.cylinder).f j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<GOAL>CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K) = CategoryTheory.Limits.biprod.inl - CategoryTheory.Limits.biprod.inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>j : ι<GOAL>HomologicalComplex.cylinder.inrX K j ≫ (HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K).f j = HomologicalComplex.cylinder.inrX K j ≫ (HomologicalComplex.cylinder.π K ≫ HomologicalComplex.cylinder.ι₀ K - 𝟙 K.cylinder).f j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<GOAL>HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K = HomologicalComplex.cylinder.π K ≫ HomologicalComplex.cylinder.ι₀ K - 𝟙 K.cylinder
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 K) (-𝟙 K))<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>H : HomologicalComplex C c ⥤ D<VAR>hH : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H<GOAL>H.map (HomologicalComplex.cylinder.ι₀ K) = H.map (HomologicalComplex.cylinder.ι₁ K)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G : HomologicalComplex C c<VAR>DecidableRel c.Rel<VAR>φ₀ φ₁ : F ⟶ G<VAR>h : Homotopy φ₀ φ₁<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)<VAR>HomologicalComplex.HasHomotopyCofiber (CategoryTheory.Limits.biprod.lift (𝟙 F) (-𝟙 F))<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} D<VAR>H : HomologicalComplex C c ⥤ D<VAR>hH : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H<GOAL>H.map φ₀ = H.map φ₁
<VAR>α : Type u_1<VAR>NNRatCast α<VAR>q : ℚ≥0<GOAL>MulOpposite.op ↑q = ↑q
<VAR>α : Type u_1<VAR>NNRatCast α<VAR>q : ℚ≥0<GOAL>AddOpposite.op ↑q = ↑q
<VAR>α : Type u_1<VAR>NNRatCast α<VAR>q : ℚ≥0<GOAL>MulOpposite.unop ↑q = ↑q
<VAR>α : Type u_1<VAR>NNRatCast α<VAR>q : ℚ≥0<GOAL>AddOpposite.unop ↑q = ↑q
<VAR>α : Type u_1<VAR>RatCast α<VAR>q : ℚ<GOAL>MulOpposite.op ↑q = ↑q
<VAR>α : Type u_1<VAR>RatCast α<VAR>q : ℚ<GOAL>AddOpposite.op ↑q = ↑q
<VAR>α : Type u_1<VAR>RatCast α<VAR>q : ℚ<GOAL>MulOpposite.unop ↑q = ↑q
<VAR>α : Type u_1<VAR>RatCast α<VAR>q : ℚ<GOAL>AddOpposite.unop ↑q = ↑q
<VAR>α : Type u_4<VAR>self : DivisionSemiring α<VAR>q : ℚ≥0<VAR>a : α<GOAL>DivisionSemiring.nnqsmul q a = ↑q * a
<VAR>α : Type u_4<VAR>self : DivisionSemiring α<VAR>q : ℚ≥0<GOAL>↑q = ↑q.num / ↑q.den
<VAR>α : Type u_4<VAR>self : DivisionRing α<GOAL>0⁻¹ = 0
<VAR>α : Type u_4<VAR>self : DivisionRing α<VAR>a : ℚ<VAR>x : α<GOAL>DivisionRing.qsmul a x = ↑a * x
<VAR>α : Type u_4<VAR>self : DivisionRing α<VAR>q : ℚ<GOAL>↑q = ↑q.num / ↑q.den
<VAR>α : Type u_4<VAR>self : DivisionRing α<VAR>q : ℚ≥0<VAR>a : α<GOAL>DivisionRing.nnqsmul q a = ↑q * a
<VAR>α : Type u_4<VAR>self : DivisionRing α<VAR>q : ℚ≥0<GOAL>↑q = ↑q.num / ↑q.den
<VAR>α : Type u_4<VAR>self : DivisionRing α<VAR>a : α<GOAL>a ≠ 0 → a * a⁻¹ = 1
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>q : ℚ≥0<GOAL>↑q = ↑q.num / ↑q.den
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>q : ℚ≥0<VAR>a : α<GOAL>q • a = ↑q * a
<VAR>α : Type u_1<VAR>DivisionSemiring α<VAR>q : ℚ≥0<GOAL>q • 1 = ↑q
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>q : ℚ<GOAL>↑q = ↑q.num / ↑q.den
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a : ℤ<VAR>b : ℕ<VAR>h1 : b ≠ 0<VAR>h2 : a.natAbs.Coprime b<GOAL>↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a / ↑b
<VAR>K : Type u_3<VAR>DivisionRing K<VAR>a : ℚ<VAR>x : K<GOAL>a • x = ↑a * x
<VAR>A : Type u_4<VAR>DivisionRing A<VAR>m : ℚ<GOAL>m • 1 = ↑m
<VAR>m : ℕ<VAR>s : Bool<VAR>e : ℕ<GOAL>Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n : ℤ<VAR>h : Odd n<VAR>a : α<GOAL>(-a) ^ n = -a ^ n
<VAR>α : Type u_1<VAR>DivisionRing α<VAR>n : ℤ<VAR>h : Odd n<GOAL>(-1) ^ n = -1
<VAR>R : Type u<VAR>CommRing R<VAR>X Y : AlgebraCat R<GOAL>↑(AlgebraCat.instMonoidalCategory.tensorObj X Y) = TensorProduct R ↑X ↑Y
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : AlgebraCat R<GOAL>(CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).map (α_ X Y Z).hom = (α_ ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj X) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj Y) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj Z)).hom
<VAR>R : Type u<VAR>CommRing R<VAR>X Y Z : AlgebraCat R<GOAL>(CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).map (α_ X Y Z).inv = (α_ ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj X) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj Y) ((CategoryTheory.forget₂ (AlgebraCat R) (ModuleCat R)).obj Z)).inv
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>j j' : J<GOAL>(K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>j j' : J<GOAL>(K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>j j' : J<GOAL>(K.totalFlipIso c).hom.f j ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIso c).hom.f j'
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>j j' : J<GOAL>(K.totalFlipIso c).hom.f j ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIso c).hom.f j'
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₂.π c₁ c (i₂, i₁) = j<GOAL>K.flip.ιTotal c i₂ i₁ j h ≫ (K.totalFlipIso c).hom.f j = c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>j : J<VAR>h : c₁.π c₂ c (i₁, i₂) = j<GOAL>K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯
<VAR>C : Type u_1<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>J : Type u_4<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K : HomologicalComplex₂ C c₁ c₂<VAR>c : ComplexShape J<VAR>TotalComplexShape c₁ c₂ c<VAR>TotalComplexShape c₂ c₁ c<VAR>TotalComplexShapeSymmetry c₁ c₂ c<VAR>K.HasTotal c<VAR>K.flip.HasTotal c<VAR>DecidableEq J<VAR>TotalComplexShapeSymmetry c₂ c₁ c<VAR>TotalComplexShapeSymmetrySymmetry c₁ c₂ c<GOAL>K.flip.totalFlipIso c = (K.totalFlipIso c).symm
<VAR>α : Type u<VAR>NNRatCast α<VAR>q : ℚ≥0<GOAL>{ down := ↑q } = ↑q
<VAR>α : Type u<VAR>NNRatCast α<VAR>q : ℚ≥0<GOAL>(↑q).down = ↑q
<VAR>α : Type u<VAR>RatCast α<VAR>q : ℚ<GOAL>{ down := ↑q } = ↑q
<VAR>α : Type u<VAR>RatCast α<VAR>q : ℚ<GOAL>(↑q).down = ↑q
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Semiring A<VAR>Semiring B<VAR>hB : IsField B<VAR>e : A ≃* B<GOAL>IsField A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<VAR>i : ι<VAR>hi : i ≠ j<GOAL>((HomologicalComplex.single C c j).obj A).ExactAt i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<VAR>i : ι<VAR>hi : i ≠ j<GOAL>CategoryTheory.Limits.IsZero (((HomologicalComplex.single C c j).obj A).homology i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<GOAL>(HomologicalComplex.singleObjCyclesSelfIso c j A).hom = ((HomologicalComplex.single C c j).obj A).iCycles j ≫ (HomologicalComplex.singleObjXSelf c j A).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<GOAL>(HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom = (HomologicalComplex.singleObjXSelf c j A).inv ≫ ((HomologicalComplex.single C c j).obj A).pOpcycles j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<GOAL>(HomologicalComplex.singleObjCyclesSelfIso c j A).inv ≫ ((HomologicalComplex.single C c j).obj A).iCycles j = (HomologicalComplex.singleObjXSelf c j A).inv