ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp 0 h = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ z₂' : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp (z₂ + z₂') h = z₁.comp z₂ h + z₁.comp z₂' h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ z₂' : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp (-z₂) h = -z₁.comp z₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>k : R<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp (k • z₂) h = k • z₁.comp z₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>k : Rˣ<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<GOAL>z₁.comp (k • z₂) h = k • z₁.comp z₂ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n<GOAL>z₁.comp (CochainComplex.HomComplex.Cochain.ofHom (𝟙 G)) ⋯ = z₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>φ : (p : ℤ) → F.X p ⟶ G.X p<VAR>ψ : (p : ℤ) → G.X p ⟶ K.X p<GOAL>(CochainComplex.HomComplex.Cochain.ofHoms φ).comp (CochainComplex.HomComplex.Cochain.ofHoms ψ) ⋯ = CochainComplex.HomComplex.Cochain.ofHoms fun p => φ p ≫ ψ p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>f : F ⟶ G<VAR>g : G ⟶ K<GOAL>CochainComplex.HomComplex.Cochain.ofHom (f ≫ g) = (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.Cochain.ofHom g) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(CochainComplex.HomComplex.Cochain.diff K).v p q hpq = K.d p q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : n + 1 = m<VAR>z : CochainComplex.HomComplex.Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + m = q<VAR>q₁ q₂ : ℤ<VAR>hq₁ : q₁ = q - 1<VAR>hq₂ : p + 1 = q₂<GOAL>(CochainComplex.HomComplex.δ n m z).v p q hpq = z.v p q₁ ⋯ ≫ G.d q₁ q + m.negOnePow • F.d p q₂ ≫ z.v q₂ q ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : ¬n + 1 = m<VAR>z : CochainComplex.HomComplex.Cochain F G n<GOAL>CochainComplex.HomComplex.δ n m z = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G n<GOAL>(CochainComplex.HomComplex.δ_hom R F G n m) z = CochainComplex.HomComplex.δ n m z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G n<GOAL>CochainComplex.HomComplex.δ n m (z₁ + z₂) = CochainComplex.HomComplex.δ n m z₁ + CochainComplex.HomComplex.δ n m z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cochain F G n<GOAL>CochainComplex.HomComplex.δ n m (z₁ - z₂) = CochainComplex.HomComplex.δ n m z₁ - CochainComplex.HomComplex.δ n m z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<GOAL>CochainComplex.HomComplex.δ n m 0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G n<GOAL>CochainComplex.HomComplex.δ n m (-z) = -CochainComplex.HomComplex.δ n m z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>k : R<VAR>z : CochainComplex.HomComplex.Cochain F G n<GOAL>CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>k : Rˣ<VAR>z : CochainComplex.HomComplex.Cochain F G n<GOAL>CochainComplex.HomComplex.δ n m (k • z) = k • CochainComplex.HomComplex.δ n m z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n₀ n₁ n₂ : ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G n₀<GOAL>CochainComplex.HomComplex.δ n₁ n₂ (CochainComplex.HomComplex.δ n₀ n₁ z) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>m₁ m₂ m₁₂ : ℤ<VAR>h₁₂ : n₁₂ + 1 = m₁₂<VAR>h₁ : n₁ + 1 = m₁<VAR>h₂ : n₂ + 1 = m₂<GOAL>CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G 0<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>m₂ : ℤ<VAR>h₂ : n₂ + 1 = m₂<GOAL>CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ⋯) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n₁ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K 0<VAR>m₁ : ℤ<VAR>h₁ : n₁ + 1 = m₁<GOAL>CochainComplex.HomComplex.δ n₁ m₁ (z₁.comp z₂ ⋯) = z₁.comp (CochainComplex.HomComplex.δ 0 1 z₂) h₁ + (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G 0<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(CochainComplex.HomComplex.δ 0 1 z).v p q hpq = z.v p p ⋯ ≫ G.d p q - F.d p q ≫ z.v q q ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>p : ℤ<VAR>φ : F ⟶ G<GOAL>CochainComplex.HomComplex.δ 0 p (CochainComplex.HomComplex.Cochain.ofHom φ) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : Homotopy φ₁ φ₂<GOAL>CochainComplex.HomComplex.δ (-1) 0 (CochainComplex.HomComplex.Cochain.ofHomotopy h) = CochainComplex.HomComplex.Cochain.ofHom φ₁ - CochainComplex.HomComplex.Cochain.ofHom φ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G (-1)<GOAL>CochainComplex.HomComplex.δ (-1) 0 z = CochainComplex.HomComplex.Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij => z.v i j ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>i : ℤ<GOAL>(F.HomComplex G).X i = AddCommGrp.of (CochainComplex.HomComplex.Cochain F G i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : n + 1 = m<VAR>z : CochainComplex.HomComplex.Cochain F G n<GOAL>z ∈ CochainComplex.HomComplex.cocycle F G n ↔ CochainComplex.HomComplex.δ n m z = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n<VAR>h : ↑z₁ = ↑z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n<GOAL>z₁ = z₂ ↔ ↑z₁ = ↑z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<GOAL>↑0 = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n<GOAL>↑(z₁ + z₂) = ↑z₁ + ↑z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G n<GOAL>↑(-z) = -↑z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G n<VAR>x : R<GOAL>↑(x • z) = x • ↑z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>R : Type u_1<VAR>Ring R<VAR>CategoryTheory.Linear R C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G n<VAR>x : Rˣ<GOAL>↑(x • z) = x • ↑z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ z₂ : CochainComplex.HomComplex.Cocycle F G n<GOAL>↑(z₁ - z₂) = ↑z₁ - ↑z₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : CochainComplex.HomComplex.Cochain F G n<VAR>m : ℤ<VAR>hnm : n + 1 = m<VAR>h : CochainComplex.HomComplex.δ n m z = 0<GOAL>↑(CochainComplex.HomComplex.Cocycle.mk z m hnm h) = z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>n : ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G n<VAR>m : ℤ<GOAL>CochainComplex.HomComplex.δ n m ↑z = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<GOAL>↑(CochainComplex.HomComplex.Cocycle.ofHom φ) = CochainComplex.HomComplex.Cochain.ofHom φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G 0<VAR>i : ℤ<GOAL>z.homOf.f i = (↑z).v i i ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<GOAL>(CochainComplex.HomComplex.Cocycle.ofHom φ).homOf = φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G 0<GOAL>CochainComplex.HomComplex.Cocycle.ofHom z.homOf = z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G 0<GOAL>CochainComplex.HomComplex.Cochain.ofHom z.homOf = ↑z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<GOAL>(CochainComplex.HomComplex.Cocycle.equivHom F G) φ = CochainComplex.HomComplex.Cocycle.ofHom φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>z : CochainComplex.HomComplex.Cocycle F G 0<GOAL>(CochainComplex.HomComplex.Cocycle.equivHom F G).symm z = z.homOf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K : CochainComplex C ℤ<GOAL>↑(CochainComplex.HomComplex.Cocycle.diff K) = CochainComplex.HomComplex.Cochain.diff K
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n<VAR>z₂ : CochainComplex.HomComplex.Cocycle G K 0<VAR>m : ℤ<GOAL>CochainComplex.HomComplex.δ n m (z₁.comp ↑z₂ ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp ↑z₂ ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n<VAR>f : G ⟶ K<VAR>m : ℤ<GOAL>CochainComplex.HomComplex.δ n m (z₁.comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯) = (CochainComplex.HomComplex.δ n m z₁).comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cocycle F G 0<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n<VAR>m : ℤ<GOAL>CochainComplex.HomComplex.δ n m ((↑z₁).comp z₂ ⋯) = (↑z₁).comp (CochainComplex.HomComplex.δ n m z₂) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G K : CochainComplex C ℤ<VAR>n : ℤ<VAR>f : F ⟶ G<VAR>z : CochainComplex.HomComplex.Cochain G K n<VAR>m : ℤ<GOAL>CochainComplex.HomComplex.δ n m ((CochainComplex.HomComplex.Cochain.ofHom f).comp z ⋯) = (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.δ n m z) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>z : { z // CochainComplex.HomComplex.Cochain.ofHom φ₁ = CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }<VAR>i j : ℤ<GOAL>((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂).symm z).hom i j = if hij : i + -1 = j then (↑z).v i j hij else 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>ho : Homotopy φ₁ φ₂<GOAL>↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) ho) = CochainComplex.HomComplex.Cochain.ofHomotopy ho
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : φ₁ = φ₂<GOAL>↑((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂) (Homotopy.ofEq h)) = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>f₁ f₂ : F ⟶ G<VAR>h : CochainComplex.HomComplex.Cochain.ofHom f₁ = CochainComplex.HomComplex.Cochain.ofHom f₂<GOAL>f₁ = f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>z : CochainComplex.HomComplex.Cochain K L n<VAR>Φ : C ⥤ D<VAR>Φ.Additive<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(z.map Φ).v p q hpq = Φ.map (z.v p q hpq)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>z z' : CochainComplex.HomComplex.Cochain K L n<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>(z + z').map Φ = z.map Φ + z'.map Φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>z : CochainComplex.HomComplex.Cochain K L n<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>(-z).map Φ = -z.map Φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>z z' : CochainComplex.HomComplex.Cochain K L n<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>(z - z').map Φ = z.map Φ - z'.map Φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n : ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>CochainComplex.HomComplex.Cochain.map 0 Φ = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>F G : CochainComplex C ℤ<VAR>K : CochainComplex C ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : CochainComplex.HomComplex.Cochain F G n₁<VAR>z₂ : CochainComplex.HomComplex.Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>(z₁.comp z₂ h).map Φ = (z₁.map Φ).comp (z₂.map Φ) h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>f : K ⟶ L<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>(CochainComplex.HomComplex.Cochain.ofHom f).map Φ = CochainComplex.HomComplex.Cochain.ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>CategoryTheory.Preadditive D<VAR>z : CochainComplex.HomComplex.Cochain K L n<VAR>Φ : C ⥤ D<VAR>Φ.Additive<GOAL>CochainComplex.HomComplex.δ n m (z.map Φ) = (CochainComplex.HomComplex.δ n m z).map Φ
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).Exact<GOAL>S.Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<VAR>hS : ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).ShortExact<GOAL>S.ShortExact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<GOAL>S.Exact ↔ ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).Exact
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Abelian C<VAR>S : CategoryTheory.ShortComplex (HomologicalComplex C c)<GOAL>S.ShortExact ↔ ∀ (i : ι), (S.map (HomologicalComplex.eval C c i)).ShortExact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>self : S.Exact<GOAL>∃ h, CategoryTheory.Limits.IsZero h.left.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<GOAL>S.HasHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<GOAL>CategoryTheory.Limits.HasZeroObject C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero S.homology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h : S.RightHomologyData<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero h.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero S.leftHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero S.rightHomology
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero h.left.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>S.Exact ↔ CategoryTheory.Limits.IsZero h.right.H
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>CategoryTheory.Limits.HasZeroObject C<GOAL>S.Exact ↔ Nonempty (S.homology ≅ 0)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h : S₁.Exact<GOAL>S₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<GOAL>S₁.Exact ↔ S₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<GOAL>S₁.Exact ∧ CategoryTheory.Mono S₁.f ↔ S₂.Exact ∧ CategoryTheory.Mono S₂.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>e : S₁ ≅ S₂<GOAL>S₁.Exact ∧ CategoryTheory.Epi S₁.g ↔ S₂.Exact ∧ CategoryTheory.Epi S₂.g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : CategoryTheory.Limits.IsZero S.X₂<GOAL>S.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S₁ S₂ : CategoryTheory.ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>CategoryTheory.Epi φ.τ₁<VAR>CategoryTheory.IsIso φ.τ₂<VAR>CategoryTheory.Mono φ.τ₃<GOAL>S₁.Exact ↔ S₂.Exact
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.HomologyData<GOAL>S.Exact ↔ CategoryTheory.CategoryStruct.comp h.left.i h.right.p = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>S.Exact ↔ CategoryTheory.CategoryStruct.comp h₁.i h₂.p = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<GOAL>S.Exact ↔ CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>S.HasHomology<VAR>CategoryTheory.Limits.HasKernel S.g<VAR>CategoryTheory.Limits.HasCokernel S.f<GOAL>S.Exact ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>S : CategoryTheory.ShortComplex C<VAR>h : S.Exact<GOAL>S.op.Exact