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>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>hT : T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C<GOAL>T.rotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>hT : T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C<VAR>n : ℤ<GOAL>(CategoryTheory.Pretriangulated.Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>hT : T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C<GOAL>T.invRotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<GOAL>T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C ↔ T.rotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>T₁ T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))<VAR>hT₁ : T₁ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C<VAR>hT₂ : T₂ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>X Y : CochainComplex C ℤ<VAR>f : X ⟶ Y<GOAL>CochainComplex.mappingCone.triangleh f ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>b : R<VAR>v : DirectSum ι fun i => M i<VAR>i : ι<GOAL>(b • v) i = b • v i
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i : ι<VAR>b : M i<GOAL>(DirectSum.lof R ι M i) b = (DirectSum.of M i) b
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i : ι<VAR>b : M i<GOAL>DFinsupp.single i b = (DirectSum.lof R ι M i) b
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>s : Finset ι<VAR>c : R<VAR>x : (i : ↑↑s) → M ↑i<GOAL>(DirectSum.mk M s) (c • x) = c • (DirectSum.mk M s) x
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i : ι<VAR>c : R<VAR>x : M i<GOAL>(DirectSum.of M i) (c • x) = c • (DirectSum.of M i) x
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>(i : ι) → (x : M i) → Decidable (x ≠ 0)<VAR>c : R<VAR>v : DirectSum ι fun i => M i<GOAL>DFinsupp.support (c • v) ⊆ DFinsupp.support v
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>AddCommMonoid N<VAR>Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<GOAL>⇑(DirectSum.toModule R ι N φ) = ⇑(DirectSum.toAddMonoid fun i => (φ i).toAddMonoidHom)
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>AddCommMonoid N<VAR>Module R N<VAR>φ : (i : ι) → M i →ₗ[R] N<VAR>i : ι<VAR>x : M i<GOAL>(DirectSum.toModule R ι N φ) ((DirectSum.lof R ι M i) x) = (φ i) x
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>AddCommMonoid N<VAR>Module R N<VAR>ψ : (DirectSum ι fun i => M i) →ₗ[R] N<VAR>f : DirectSum ι fun i => M i<GOAL>ψ f = (DirectSum.toModule R ι N fun i => ψ ∘ₗ DirectSum.lof R ι M i) f
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>N : Type u₁<VAR>AddCommMonoid N<VAR>Module R N<VAR>ψ ψ' : (DirectSum ι fun i => M i) →ₗ[R] N<VAR>H : ∀ (i : ι), ψ ∘ₗ DirectSum.lof R ι M i = ψ' ∘ₗ DirectSum.lof R ι M i<GOAL>ψ = ψ'
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<GOAL>∀ (a : Π₀ (i : ι), (fun i => M i) i) (a_1 : ι), (DirectSum.linearEquivFunOnFintype R ι M) a a_1 = a a_1
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M i<GOAL>(DirectSum.linearEquivFunOnFintype R ι M) ((DirectSum.lof R ι M i) m) = Pi.single i m
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>i : ι<VAR>m : M i<GOAL>(DirectSum.linearEquivFunOnFintype R ι M).symm (Pi.single i m) = (DirectSum.lof R ι M i) m
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>Fintype ι<VAR>f : DirectSum ι fun i => M i<GOAL>(DirectSum.linearEquivFunOnFintype R ι M).symm ⇑f = f
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>f : DirectSum ι fun i => M i<VAR>i : ι<GOAL>f i = (DirectSum.component R ι M i) f
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>f g : DirectSum ι fun i => M i<VAR>h : ∀ (i : ι), (DirectSum.component R ι M i) f = (DirectSum.component R ι M i) g<GOAL>f = g
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>f g : DirectSum ι fun i => M i<GOAL>f = g ↔ ∀ (i : ι), (DirectSum.component R ι M i) f = (DirectSum.component R ι M i) g
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i : ι<VAR>b : M i<GOAL>((DirectSum.lof R ι M i) b) i = b
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i : ι<VAR>b : M i<GOAL>(DirectSum.component R ι M i) ((DirectSum.lof R ι M i) b) = b
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i j : ι<VAR>b : M j<GOAL>(DirectSum.component R ι M i) ((DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>M : ι → Type w<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>κ : Type u_1<VAR>h : ι ≃ κ<VAR>f : DirectSum ι fun i => M i<VAR>k : κ<GOAL>((DirectSum.lequivCongrLeft R h) f) k = f (h.symm k)
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>α : ι → Type u_1<VAR>δ : (i : ι) → α i → Type w<VAR>(i : ι) → (j : α i) → AddCommMonoid (δ i j)<VAR>(i : ι) → (j : α i) → Module R (δ i j)<VAR>f : DirectSum ((x : ι) × α x) fun i => δ i.fst i.snd<VAR>i : ι<VAR>j : α i<GOAL>(((DirectSum.sigmaLcurry R) f) i) j = f ⟨i, j⟩
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>α : ι → Type u_1<VAR>δ : (i : ι) → α i → Type w<VAR>(i : ι) → (j : α i) → AddCommMonoid (δ i j)<VAR>(i : ι) → (j : α i) → Module R (δ i j)<VAR>f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j<VAR>i : ι<VAR>j : α i<GOAL>((DirectSum.sigmaLuncurry R) f) ⟨i, j⟩ = (f i) j
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>α : Option ι → Type w<VAR>(i : Option ι) → AddCommMonoid (α i)<VAR>(i : Option ι) → Module R (α i)<GOAL>∀ (a : DirectSum (Option ι) fun i => α i), (DirectSum.lequivProdDirectSum R) a = DirectSum.addEquivProdDirectSum.toFun a
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>α : Option ι → Type w<VAR>(i : Option ι) → AddCommMonoid (α i)<VAR>(i : Option ι) → Module R (α i)<GOAL>∀ (a : α none × DirectSum ι fun i => α (some i)), (DirectSum.lequivProdDirectSum R).symm a = DirectSum.addEquivProdDirectSum.invFun a
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>DecidableEq M<VAR>x : DirectSum ι fun i => ↥(A i)<GOAL>(DirectSum.coeLinearMap A) x = DFinsupp.sum x fun i x => ↑x
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>i : ι<VAR>x : ↥(A i)<GOAL>(DirectSum.coeLinearMap A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>i : ι<VAR>x : ↥(A i)<GOAL>((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ↑x) i = x
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : ↥(A i)<GOAL>((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ↑x) j = 0
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>i : ι<VAR>x : M<VAR>hx : x ∈ A i<GOAL>((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm x) i = ⟨x, hx⟩
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>i j : ι<VAR>hij : i ≠ j<VAR>x : M<VAR>hx : x ∈ A i<GOAL>((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm x) j = 0
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<GOAL>iSup A = ⊤
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<GOAL>CompleteLattice.Independent A
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<GOAL>⇑(h.collectedBasis v) = fun a => ↑((v a.fst) a.snd)
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>a : (i : ι) × α i<GOAL>(h.collectedBasis v) a ∈ A a.fst
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>x : M<VAR>i : ι<VAR>a : α i<VAR>hx : x ∈ A i<GOAL>((h.collectedBasis v).repr x) ⟨i, a⟩ = ((v i).repr ⟨x, hx⟩) a
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>h : DirectSum.IsInternal A<VAR>α : ι → Type u_2<VAR>v : (i : ι) → Basis (α i) R ↥(A i)<VAR>x : M<VAR>i j : ι<VAR>hij : i ≠ j<VAR>a : α j<VAR>hx : x ∈ A i<GOAL>((h.collectedBasis v).repr x) ⟨j, a⟩ = 0
<VAR>R : Type u<VAR>Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Set.univ = {i, j}<VAR>hi : DirectSum.IsInternal A<GOAL>IsCompl (A i) (A j)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>hi : CompleteLattice.Independent A<VAR>hs : iSup A = ⊤<GOAL>DirectSum.IsInternal A
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>A : ι → Submodule R M<GOAL>DirectSum.IsInternal A ↔ CompleteLattice.Independent A ∧ iSup A = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Set.univ = {i, j}<GOAL>DirectSum.IsInternal A ↔ IsCompl (A i) (A j)
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>A : ι → Submodule R M<GOAL>(DirectSum.IsInternal fun i => A ↑i) ↔ DirectSum.IsInternal A
<VAR>R : Type u<VAR>Ring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>A : ι → Submodule R M<VAR>s : Set ι<VAR>h : CompleteLattice.Independent fun i => A ↑i<GOAL>DirectSum.IsInternal fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)
<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>A : ι → AddSubmonoid M<VAR>h : DirectSum.IsInternal A<GOAL>CompleteLattice.Independent A
<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>A : ι → AddSubgroup M<VAR>h : DirectSum.IsInternal A<GOAL>CompleteLattice.Independent A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>a b x : ℤ<GOAL>K.shiftFunctor₁XXIso a x (a + x) ⋯ b = CategoryTheory.Iso.refl ((((HomologicalComplex₂.shiftFunctor₁ C x).obj K).X a).X b)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>a b y : ℤ<GOAL>K.shiftFunctor₂XXIso a b y (b + y) ⋯ = CategoryTheory.Iso.refl ((((HomologicalComplex₂.shiftFunctor₂ C y).obj K).X a).X b)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>x : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>n₀ n₁ n₀' n₁' : ℤ<VAR>h₀ : n₀ + x = n₀'<VAR>h₁ : n₁ + x = n₁'<GOAL>((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₁ (ComplexShape.up ℤ) n₀' n₁'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>x : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>n₀ n₁ n₀' n₁' : ℤ<VAR>h₀ : n₀ + x = n₀'<VAR>h₁ : n₁ + x = n₁'<GOAL>((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (ComplexShape.up ℤ) n₀' n₁'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>x : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>a' : ℤ<VAR>ha' : a' = a + x<VAR>n' : ℤ<VAR>hn' : n' = n + x<GOAL>((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n = (K.shiftFunctor₁XXIso a x a' ha' b).hom ≫ K.ιTotal (ComplexShape.up ℤ) a' b n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>x : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>a' n' : ℤ<VAR>ha' : a' + b = n'<VAR>hn' : n' = n + x<GOAL>K.ιTotal (ComplexShape.up ℤ) a' b n' ha' ≫ (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv ≫ (K.totalShift₁Iso x).inv.f n = (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>f : K ⟶ L<VAR>x : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>L.HasTotal (ComplexShape.up ℤ)<GOAL>HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁ C x).map f) (ComplexShape.up ℤ) ≫ (L.totalShift₁Iso x).hom = (K.totalShift₁Iso x).hom ≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (HomologicalComplex₂.total.map f (ComplexShape.up ℤ))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>n₀ n₁ n₀' n₁' : ℤ<VAR>h₀ : n₀ + y = n₀'<VAR>h₁ : n₁ + y = n₁'<GOAL>((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (ComplexShape.up ℤ) n₀' n₁'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>n₀ n₁ n₀' n₁' : ℤ<VAR>h₀ : n₀ + y = n₀'<VAR>h₁ : n₁ + y = n₁'<GOAL>((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₂ (ComplexShape.up ℤ) n₀' n₁'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>b' : ℤ<VAR>hb' : b' = b + y<VAR>n' : ℤ<VAR>hn' : n' = n + y<GOAL>((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n = (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' hb').hom ≫ K.ιTotal (ComplexShape.up ℤ) a b' n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>a b n : ℤ<VAR>h : a + b = n<VAR>b' n' : ℤ<VAR>hb' : a + b' = n'<VAR>hn' : n' = n + y<GOAL>K.ιTotal (ComplexShape.up ℤ) a b' n' hb' ≫ (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) y n n' hn').inv ≫ (K.totalShift₂Iso y).inv.f n = (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).ιTotal (ComplexShape.up ℤ) a b n h
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>f : K ⟶ L<VAR>y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<VAR>L.HasTotal (ComplexShape.up ℤ)<GOAL>HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₂ C y).map f) (ComplexShape.up ℤ) ≫ (L.totalShift₂Iso y).hom = (K.totalShift₂Iso y).hom ≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (HomologicalComplex₂.total.map f (ComplexShape.up ℤ))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>x y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<GOAL>((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) x).mapIso (K.totalShift₂Iso y) = (x * y).negOnePow • HomologicalComplex₂.total.mapIso ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).app K) (ComplexShape.up ℤ) ≪≫ ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y ≪≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).mapIso (K.totalShift₁Iso x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).app (K.total (ComplexShape.up ℤ))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)<VAR>x y : ℤ<VAR>K.HasTotal (ComplexShape.up ℤ)<GOAL>(((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom ≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom = (x * y).negOnePow • HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ) ≫ (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom ≫ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom ≫ (CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ))
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i j : ℕ<GOAL>(ChainComplex.truncate.obj C).d i j = C.d (i + 1) (j + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i : ℕ<GOAL>(ChainComplex.truncate.obj C).X i = C.X (i + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<GOAL>∀ {X Y : ChainComplex V ℕ} (f : X ⟶ Y) (i : ℕ), (ChainComplex.truncate.map f).f i = f.f (i + 1)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>w : C.d 1 0 ≫ f = 0<GOAL>(C.augment f w).X 0 = X
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>w : C.d 1 0 ≫ f = 0<VAR>i : ℕ<GOAL>(C.augment f w).X (i + 1) = C.X i
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>w : C.d 1 0 ≫ f = 0<GOAL>(C.augment f w).d 1 0 = f
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>w : C.d 1 0 ≫ f = 0<VAR>i j : ℕ<GOAL>(C.augment f w).d (i + 1) (j + 1) = C.d i j
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>w : C.d 1 0 ≫ f = 0<VAR>i : ℕ<GOAL>(C.truncateAugment f w).hom.f i = 𝟙 (C.X i)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>X : V<VAR>f : C.X 0 ⟶ X<VAR>w : C.d 1 0 ≫ f = 0<VAR>i : ℕ<GOAL>(C.truncateAugment f w).inv.f i = 𝟙 ((ChainComplex.truncate.obj (C.augment f w)).X i)
<VAR>V : Type u<VAR>CategoryTheory.Category.{v, u} V<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i : ℕ<GOAL>C.d (i + 2) 0 = 0