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>p q : ℤ<VAR>hpq : q + 1 = p<GOAL>(CochainComplex.mappingCone.inl φ).v p q ⋯ ≫ (↑(CochainComplex.mappingCone.fst φ)).v q p hpq = 𝟙 (F.X 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>p q : ℤ<VAR>hpq : p + -1 = q<GOAL>(CochainComplex.mappingCone.inl φ).v p q hpq ≫ (CochainComplex.mappingCone.snd φ).v q q ⋯ = 0
<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>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(CochainComplex.mappingCone.inr φ).f p ≫ (↑(CochainComplex.mappingCone.fst φ)).v p q hpq = 0
<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>p : ℤ<GOAL>(CochainComplex.mappingCone.inr φ).f p ≫ (CochainComplex.mappingCone.snd φ).v p p ⋯ = 𝟙 (G.X 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 φ<GOAL>(CochainComplex.mappingCone.inl φ).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ = CochainComplex.HomComplex.Cochain.ofHom (𝟙 F)
<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 φ<GOAL>(CochainComplex.mappingCone.inl φ).comp (CochainComplex.mappingCone.snd φ) ⋯ = 0
<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 φ<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ = 0
<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 φ<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp (CochainComplex.mappingCone.snd φ) ⋯ = CochainComplex.HomComplex.Cochain.ofHom (𝟙 G)
<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>d e : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain F K d<VAR>he : 1 + d = e<GOAL>(CochainComplex.mappingCone.inl φ).comp ((↑(CochainComplex.mappingCone.fst φ)).comp γ he) ⋯ = γ
<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>d e f : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain G K d<VAR>he : 0 + d = e<VAR>hf : -1 + e = f<GOAL>(CochainComplex.mappingCone.inl φ).comp ((CochainComplex.mappingCone.snd φ).comp γ he) hf = 0
<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>d e f : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain F K d<VAR>he : 1 + d = e<VAR>hf : 0 + e = f<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ((↑(CochainComplex.mappingCone.fst φ)).comp γ he) hf = 0
<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>d e : ℤ<VAR>γ : CochainComplex.HomComplex.Cochain G K d<VAR>he : 0 + d = e<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp ((CochainComplex.mappingCone.snd φ).comp γ he) ⋯ = γ
<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>i j : ℤ<VAR>hij : i + 1 = j<VAR>A : C<VAR>f g : A ⟶ (CochainComplex.mappingCone φ).X i<VAR>h₁ : f ≫ (↑(CochainComplex.mappingCone.fst φ)).v i j hij = g ≫ (↑(CochainComplex.mappingCone.fst φ)).v i j hij<VAR>h₂ : f ≫ (CochainComplex.mappingCone.snd φ).v i i ⋯ = g ≫ (CochainComplex.mappingCone.snd φ).v i i ⋯<GOAL>f = g
<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>i j : ℤ<VAR>hij : i + 1 = j<VAR>A : C<VAR>f g : A ⟶ (CochainComplex.mappingCone φ).X i<GOAL>f = g ↔ f ≫ (↑(CochainComplex.mappingCone.fst φ)).v i j hij = g ≫ (↑(CochainComplex.mappingCone.fst φ)).v i j hij ∧ f ≫ (CochainComplex.mappingCone.snd φ).v i i ⋯ = g ≫ (CochainComplex.mappingCone.snd φ).v i i ⋯
<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>i j : ℤ<VAR>hij : j + 1 = i<VAR>A : C<VAR>f g : (CochainComplex.mappingCone φ).X j ⟶ A<VAR>h₁ : (CochainComplex.mappingCone.inl φ).v i j ⋯ ≫ f = (CochainComplex.mappingCone.inl φ).v i j ⋯ ≫ g<VAR>h₂ : (CochainComplex.mappingCone.inr φ).f j ≫ f = (CochainComplex.mappingCone.inr φ).f j ≫ g<GOAL>f = g
<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>i j : ℤ<VAR>hij : j + 1 = i<VAR>A : C<VAR>f g : (CochainComplex.mappingCone φ).X j ⟶ A<GOAL>f = g ↔ (CochainComplex.mappingCone.inl φ).v i j ⋯ ≫ f = (CochainComplex.mappingCone.inl φ).v i j ⋯ ≫ g ∧ (CochainComplex.mappingCone.inr φ).f j ≫ f = (CochainComplex.mappingCone.inr φ).f j ≫ g
<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>i : ℤ<VAR>A : C<VAR>f : A ⟶ (CochainComplex.mappingCone φ).X i<VAR>j : ℤ<VAR>hij : i + 1 = j<GOAL>∃ a b, f = a ≫ (CochainComplex.mappingCone.inl φ).v j i ⋯ + b ≫ (CochainComplex.mappingCone.inr φ).f i
<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>j : ℤ<VAR>A : C<VAR>f : (CochainComplex.mappingCone φ).X j ⟶ A<VAR>i : ℤ<VAR>hij : j + 1 = i<GOAL>∃ a b, f = (↑(CochainComplex.mappingCone.fst φ)).v j i hij ≫ a + (CochainComplex.mappingCone.snd φ).v j j ⋯ ≫ b
<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>i j : ℤ<VAR>hij : i + 1 = j<VAR>K : CochainComplex C ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain K (CochainComplex.mappingCone φ) i<GOAL>γ₁ = γ₂ ↔ γ₁.comp (↑(CochainComplex.mappingCone.fst φ)) hij = γ₂.comp (↑(CochainComplex.mappingCone.fst φ)) hij ∧ γ₁.comp (CochainComplex.mappingCone.snd φ) ⋯ = γ₂.comp (CochainComplex.mappingCone.snd φ) ⋯
<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>i j : ℤ<VAR>hij : i + 1 = j<VAR>K : CochainComplex C ℤ<VAR>γ₁ γ₂ : CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) K j<GOAL>γ₁ = γ₂ ↔ (CochainComplex.mappingCone.inl φ).comp γ₁ ⋯ = (CochainComplex.mappingCone.inl φ).comp γ₂ ⋯ ∧ (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp γ₁ ⋯ = (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).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 φ<GOAL>(↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.mappingCone.inl φ) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯ = CochainComplex.HomComplex.Cochain.ofHom (𝟙 (CochainComplex.mappingCone φ))
<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>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(↑(CochainComplex.mappingCone.fst φ)).v p q hpq ≫ (CochainComplex.mappingCone.inl φ).v q p ⋯ + (CochainComplex.mappingCone.snd φ).v p p ⋯ ≫ (CochainComplex.mappingCone.inr φ).f p = 𝟙 ((CochainComplex.mappingCone φ).X 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>i j k : ℤ<VAR>hij : i + -1 = j<VAR>hik : k + -1 = i<GOAL>(CochainComplex.mappingCone.inl φ).v i j hij ≫ (CochainComplex.mappingCone φ).d j i = φ.f i ≫ (CochainComplex.mappingCone.inr φ).f i - F.d i k ≫ (CochainComplex.mappingCone.inl φ).v k i hik
<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>n₁ n₂ : ℤ<GOAL>(CochainComplex.mappingCone.inr φ).f n₁ ≫ (CochainComplex.mappingCone φ).d n₁ n₂ = G.d n₁ n₂ ≫ (CochainComplex.mappingCone.inr φ).f n₂
<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>i j k : ℤ<VAR>hij : i + 1 = j<VAR>hjk : j + 1 = k<GOAL>(CochainComplex.mappingCone φ).d i j ≫ (↑(CochainComplex.mappingCone.fst φ)).v j k hjk = -(↑(CochainComplex.mappingCone.fst φ)).v 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>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>HomologicalComplex.HasHomotopyCofiber φ<VAR>i j : ℤ<VAR>hij : i + 1 = j<GOAL>(CochainComplex.mappingCone φ).d (i - 1) i ≫ (↑(CochainComplex.mappingCone.fst φ)).v i j hij = -(↑(CochainComplex.mappingCone.fst φ)).v (i - 1) i ⋯ ≫ F.d i j
<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>i j : ℤ<VAR>hij : i + 1 = j<GOAL>(CochainComplex.mappingCone φ).d i j ≫ (CochainComplex.mappingCone.snd φ).v j j ⋯ = (↑(CochainComplex.mappingCone.fst φ)).v i j hij ≫ φ.f j + (CochainComplex.mappingCone.snd φ).v i i ⋯ ≫ G.d i j
<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>n : ℤ<GOAL>(CochainComplex.mappingCone φ).d (n - 1) n ≫ (CochainComplex.mappingCone.snd φ).v n n ⋯ = (↑(CochainComplex.mappingCone.fst φ)).v (n - 1) n ⋯ ≫ φ.f n + (CochainComplex.mappingCone.snd φ).v (n - 1) (n - 1) ⋯ ≫ G.d (n - 1) n
<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 φ<GOAL>CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.mappingCone.inl φ) = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ CochainComplex.mappingCone.inr φ)
<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 φ<GOAL>CochainComplex.HomComplex.δ 0 1 (CochainComplex.mappingCone.snd φ) = -(↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯
<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>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K m<VAR>β : CochainComplex.HomComplex.Cochain G K n<VAR>h : m + 1 = n<GOAL>(CochainComplex.mappingCone.inl φ).comp (CochainComplex.mappingCone.descCochain φ α β 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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K m<VAR>β : CochainComplex.HomComplex.Cochain G K n<VAR>h : m + 1 = n<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)).comp (CochainComplex.mappingCone.descCochain φ α β 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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K m<VAR>β : CochainComplex.HomComplex.Cochain G K n<VAR>h : m + 1 = n<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + -1 = p₂<VAR>h₂₃ : p₂ + n = p₃<GOAL>(CochainComplex.mappingCone.inl φ).v p₁ p₂ h₁₂ ≫ (CochainComplex.mappingCone.descCochain φ α β h).v p₂ p₃ h₂₃ = α.v p₁ 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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K m<VAR>β : CochainComplex.HomComplex.Cochain G K n<VAR>h : m + 1 = n<VAR>p₁ p₂ : ℤ<VAR>h₁₂ : p₁ + n = p₂<GOAL>(CochainComplex.mappingCone.inr φ).f p₁ ≫ (CochainComplex.mappingCone.descCochain φ α β h).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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K m<VAR>β : CochainComplex.HomComplex.Cochain G K n<VAR>h : m + 1 = n<VAR>n' : ℤ<VAR>hn' : n + 1 = n'<GOAL>CochainComplex.HomComplex.δ n n' (CochainComplex.mappingCone.descCochain φ α β h) = (↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.HomComplex.δ m n α + n'.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.δ n n' β) ⋯
<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>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K m<VAR>β : CochainComplex.HomComplex.Cocycle G K n<VAR>h : m + 1 = n<VAR>eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯<GOAL>↑(CochainComplex.mappingCone.descCocycle φ α β h eq) = CochainComplex.mappingCone.descCochain φ α (↑β) 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 : CochainComplex C ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β)<GOAL>CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.desc φ α β eq) = CochainComplex.mappingCone.descCochain φ α (CochainComplex.HomComplex.Cochain.ofHom β) ⋯
<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.Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β)<VAR>p q : ℤ<VAR>h : p + -1 = q<GOAL>(CochainComplex.mappingCone.inl φ).v p q h ≫ (CochainComplex.mappingCone.desc φ α β eq).f q = α.v p q 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 : CochainComplex C ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β)<GOAL>(CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.desc φ α β eq)) ⋯ = α
<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.Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β)<VAR>p : ℤ<GOAL>(CochainComplex.mappingCone.inr φ).f p ≫ (CochainComplex.mappingCone.desc φ α β eq).f p = β.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 : CochainComplex C ℤ<VAR>α : CochainComplex.HomComplex.Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β)<GOAL>CochainComplex.mappingCone.inr φ ≫ CochainComplex.mappingCone.desc φ α β eq = β
<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.Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : CochainComplex.HomComplex.δ (-1) 0 α = CochainComplex.HomComplex.Cochain.ofHom (φ ≫ β)<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(CochainComplex.mappingCone.desc φ α β eq).f p = (↑(CochainComplex.mappingCone.fst φ)).v p q hpq ≫ α.v q p ⋯ + (CochainComplex.mappingCone.snd φ).v p p ⋯ ≫ β.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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>h : n + 1 = m<GOAL>(CochainComplex.mappingCone.liftCochain φ α β h).comp (↑(CochainComplex.mappingCone.fst φ)) 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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>h : n + 1 = m<GOAL>(CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.snd φ) ⋯ = β
<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>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>h : n + 1 = m<VAR>p₁ p₂ p₃ : ℤ<VAR>h₁₂ : p₁ + n = p₂<VAR>h₂₃ : p₂ + 1 = p₃<GOAL>(CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (↑(CochainComplex.mappingCone.fst φ)).v p₂ p₃ h₂₃ = α.v p₁ 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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>h : n + 1 = m<VAR>p₁ p₂ : ℤ<VAR>h₁₂ : p₁ + n = p₂<GOAL>(CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (CochainComplex.mappingCone.snd φ).v p₂ p₂ ⋯ = β.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 : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cochain K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>h : n + 1 = m<VAR>m' : ℤ<VAR>hm' : m + 1 = m'<GOAL>CochainComplex.HomComplex.δ n m (CochainComplex.mappingCone.liftCochain φ α β h) = -(CochainComplex.HomComplex.δ m m' α).comp (CochainComplex.mappingCone.inl φ) ⋯ + (CochainComplex.HomComplex.δ n m β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯).comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯
<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>n m : ℤ<VAR>α : CochainComplex.HomComplex.Cocycle K F m<VAR>β : CochainComplex.HomComplex.Cochain K G n<VAR>h : n + 1 = m<VAR>eq : CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0<GOAL>↑(CochainComplex.mappingCone.liftCocycle φ α β h eq) = CochainComplex.mappingCone.liftCochain φ (↑α) β 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 : 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<GOAL>CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq) = CochainComplex.mappingCone.liftCochain φ (↑α) β ⋯
<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 ≫ (↑(CochainComplex.mappingCone.fst φ)).v p q hpq = (↑α).v p q hpq
<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<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq)).comp ↑(CochainComplex.mappingCone.fst φ) ⋯ = ↑α
<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 + 0 = q<GOAL>(CochainComplex.mappingCone.lift φ α β eq).f p ≫ (CochainComplex.mappingCone.snd φ).v p q hpq = β.v p q hpq
<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<GOAL>(CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.lift φ α β eq)).comp (CochainComplex.mappingCone.snd φ) ⋯ = β