ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.single C c j).obj A).homologyπ j ≫ (HomologicalComplex.singleObjHomologySelfIso c j A).hom = (HomologicalComplex.singleObjCyclesSelfIso 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.singleObjCyclesSelfIso c j A).hom ≫ (HomologicalComplex.singleObjHomologySelfIso c j A).inv = ((HomologicalComplex.single C c j).obj A).homologyπ 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).hom ≫ (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom = ((HomologicalComplex.single C c j).obj A).iCycles j ≫ ((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).homologyπ j = (HomologicalComplex.singleObjHomologySelfIso c j A).inv
<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.singleObjHomologySelfIso c j A).inv ≫ ((HomologicalComplex.single C c j).obj A).homologyι j = (HomologicalComplex.singleObjOpcyclesSelfIso 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.single C c j).obj A).homologyι j ≫ (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv = (HomologicalComplex.singleObjHomologySelfIso 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.singleObjHomologySelfIso c j A).hom ≫ (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom = ((HomologicalComplex.single C c j).obj A).homologyι 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 B : C<VAR>f : A ⟶ B<GOAL>HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).map f) j ≫ (HomologicalComplex.singleObjCyclesSelfIso c j B).hom = (HomologicalComplex.singleObjCyclesSelfIso c j A).hom ≫ f
<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 B : C<VAR>f : A ⟶ B<GOAL>(HomologicalComplex.singleObjCyclesSelfIso c j A).inv ≫ HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).map f) j = f ≫ (HomologicalComplex.singleObjCyclesSelfIso c j B).inv
<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 B : C<VAR>f : A ⟶ B<GOAL>HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).map f) j ≫ (HomologicalComplex.singleObjHomologySelfIso c j B).hom = (HomologicalComplex.singleObjHomologySelfIso c j A).hom ≫ f
<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 B : C<VAR>f : A ⟶ B<GOAL>(HomologicalComplex.singleObjHomologySelfIso c j A).inv ≫ HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).map f) j = f ≫ (HomologicalComplex.singleObjHomologySelfIso c j B).inv
<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 B : C<VAR>f : A ⟶ B<GOAL>(HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom ≫ HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).map f) j = f ≫ (HomologicalComplex.singleObjOpcyclesSelfIso c j B).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 B : C<VAR>f : A ⟶ B<GOAL>HomologicalComplex.opcyclesMap ((HomologicalComplex.single C c j).map f) j ≫ (HomologicalComplex.singleObjOpcyclesSelfIso c j B).inv = (HomologicalComplex.singleObjOpcyclesSelfIso c j A).inv ≫ f
<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>CategoryTheory.CategoryWithHomology C<VAR>X : C<GOAL>(HomologicalComplex.homologyFunctorSingleIso C c j).inv.app X = (HomologicalComplex.singleObjHomologySelfIso c j X).inv
<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>CategoryTheory.CategoryWithHomology C<VAR>X : C<GOAL>(HomologicalComplex.homologyFunctorSingleIso C c j).hom.app X = (HomologicalComplex.singleObjHomologySelfIso c j X).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>A : C<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt ((ChainComplex.single₀ C).obj A) (n + 1)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>A : C<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt ((CochainComplex.single₀ C).obj A) (n + 1)
<VAR>R : Type u<VAR>Semiring R<VAR>self : IsField R<GOAL>∃ x y, x ≠ y
<VAR>R : Type u<VAR>Semiring R<VAR>self : IsField R<VAR>x y : R<GOAL>x * y = y * x
<VAR>R : Type u<VAR>Semiring R<VAR>self : IsField R<VAR>a : R<GOAL>a ≠ 0 → ∃ b, a * b = 1
<VAR>R : Type u<VAR>Semifield R<GOAL>IsField R
<VAR>R : Type u<VAR>Field R<GOAL>IsField R
<VAR>R : Type u<VAR>Semiring R<VAR>h : IsField R<GOAL>Nontrivial R
<VAR>R : Type u<VAR>Semiring R<VAR>Subsingleton R<GOAL>¬IsField R
<VAR>R : Type u<VAR>Ring R<VAR>hf : IsField R<VAR>x : R<GOAL>x ≠ 0 → ∃! y, x * y = 1
<VAR>M : Type u_1<VAR>F : Type u_5<VAR>Monoid F<VAR>c : F → M → M<VAR>h1 : c 1 = id<VAR>hmul : ∀ (f g : F), c (f * g) = c f ∘ c g<VAR>f : F<VAR>n : ℕ<GOAL>c (f ^ n) = (c f)^[n]
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Add M<VAR>FunLike F M M<VAR>AddHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x y : M<GOAL>(⇑f)^[n] (x + y) = (⇑f)^[n] x + (⇑f)^[n] y
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Mul M<VAR>FunLike F M M<VAR>MulHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x y : M<GOAL>(⇑f)^[n] (x * y) = (⇑f)^[n] x * (⇑f)^[n] y
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Zero M<VAR>FunLike F M M<VAR>ZeroHomClass F M M<VAR>f : F<VAR>n : ℕ<GOAL>(⇑f)^[n] 0 = 0
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>One M<VAR>FunLike F M M<VAR>OneHomClass F M M<VAR>f : F<VAR>n : ℕ<GOAL>(⇑f)^[n] 1 = 1
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>AddGroup M<VAR>FunLike F M M<VAR>AddMonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x : M<GOAL>(⇑f)^[n] (-x) = -(⇑f)^[n] x
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Group M<VAR>FunLike F M M<VAR>MonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x : M<GOAL>(⇑f)^[n] x⁻¹ = ((⇑f)^[n] x)⁻¹
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>AddGroup M<VAR>FunLike F M M<VAR>AddMonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x y : M<GOAL>(⇑f)^[n] (x - y) = (⇑f)^[n] x - (⇑f)^[n] y
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Group M<VAR>FunLike F M M<VAR>MonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x y : M<GOAL>(⇑f)^[n] (x / y) = (⇑f)^[n] x / (⇑f)^[n] y
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Monoid M<VAR>FunLike F M M<VAR>MonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x : M<VAR>k : ℕ<GOAL>(⇑f)^[n] (x ^ k) = (⇑f)^[n] x ^ k
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>AddMonoid M<VAR>FunLike F M M<VAR>AddMonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x : M<VAR>k : ℕ<GOAL>(⇑f)^[n] (k • x) = k • (⇑f)^[n] x
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>Group M<VAR>FunLike F M M<VAR>MonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x : M<VAR>k : ℤ<GOAL>(⇑f)^[n] (x ^ k) = (⇑f)^[n] x ^ k
<VAR>M : Type u_5<VAR>F : Type u_6<VAR>AddGroup M<VAR>FunLike F M M<VAR>AddMonoidHomClass F M M<VAR>f : F<VAR>n : ℕ<VAR>x : M<VAR>k : ℤ<GOAL>(⇑f)^[n] (k • x) = k • (⇑f)^[n] x
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>AddMonoid G<VAR>a : G<VAR>n : ℕ<VAR>AddAction G H<GOAL>(fun x => a +ᵥ x)^[n] = fun x => n • a +ᵥ x
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Monoid G<VAR>a : G<VAR>n : ℕ<VAR>MulAction G H<GOAL>(fun x => a • x)^[n] = fun x => a ^ n • x
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>Monoid G<VAR>a : G<VAR>n : ℕ<VAR>MulAction G H<VAR>b : H<GOAL>(fun x => a • x)^[n] b = a ^ n • b
<VAR>G : Type u_3<VAR>H : Type u_4<VAR>AddMonoid G<VAR>a : G<VAR>n : ℕ<VAR>AddAction G H<VAR>b : H<GOAL>(fun x => a +ᵥ x)^[n] b = n • a +ᵥ b
<VAR>G : Type u_3<VAR>Monoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => a * x)^[n] = fun x => a ^ n * x
<VAR>G : Type u_3<VAR>AddMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => a + x)^[n] = fun x => n • a + x
<VAR>G : Type u_3<VAR>Monoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => x * a)^[n] = fun x => x * a ^ n
<VAR>G : Type u_3<VAR>AddMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => x + a)^[n] = fun x => x + n • a
<VAR>G : Type u_3<VAR>Monoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => x * a)^[n] 1 = a ^ n
<VAR>G : Type u_3<VAR>AddMonoid G<VAR>a : G<VAR>n : ℕ<GOAL>(fun x => x + a)^[n] 0 = n • a
<VAR>G : Type u_3<VAR>Monoid G<VAR>n j : ℕ<GOAL>(fun x => x ^ n)^[j] = fun x => x ^ n ^ j
<VAR>G : Type u_3<VAR>AddMonoid G<VAR>n j : ℕ<GOAL>(fun x => n • x)^[j] = fun x => n ^ j • x
<VAR>G : Type u_3<VAR>AddGroup G<VAR>n : ℤ<VAR>j : ℕ<GOAL>(fun x => n • x)^[j] = fun x => n ^ j • x
<VAR>G : Type u_3<VAR>Group G<VAR>n : ℤ<VAR>j : ℕ<GOAL>(fun x => x ^ n)^[j] = fun x => x ^ n ^ j
<VAR>G : Type u_3<VAR>AddSemigroup G<VAR>a b c : G<VAR>h : AddSemiconjBy a b c<GOAL>Function.Semiconj (fun x => a + x) (fun x => b + x) fun x => c + x
<VAR>G : Type u_3<VAR>Semigroup G<VAR>a b c : G<VAR>h : SemiconjBy a b c<GOAL>Function.Semiconj (fun x => a * x) (fun x => b * x) fun x => c * x
<VAR>G : Type u_3<VAR>Semigroup G<VAR>a b : G<VAR>h : Commute a b<GOAL>Function.Commute (fun x => a * x) fun x => b * x
<VAR>G : Type u_3<VAR>AddSemigroup G<VAR>a b : G<VAR>h : AddCommute a b<GOAL>Function.Commute (fun x => a + x) fun x => b + x
<VAR>G : Type u_3<VAR>Semigroup G<VAR>a b c : G<VAR>h : SemiconjBy a b c<GOAL>Function.Semiconj (fun x => x * a) (fun x => x * c) fun x => x * b
<VAR>G : Type u_3<VAR>AddSemigroup G<VAR>a b c : G<VAR>h : AddSemiconjBy a b c<GOAL>Function.Semiconj (fun x => x + a) (fun x => x + c) fun x => x + b
<VAR>G : Type u_3<VAR>AddSemigroup G<VAR>a b : G<VAR>h : AddCommute a b<GOAL>Function.Commute (fun x => x + a) fun x => x + b
<VAR>G : Type u_3<VAR>Semigroup G<VAR>a b : G<VAR>h : Commute a b<GOAL>Function.Commute (fun x => x * a) fun x => x * b
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.CategoryWithHomology C<VAR>i : ι<GOAL>(HomologicalComplex.quasiIso C c).IsInvertedBy (HomologicalComplex.homologyFunctor C c i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.CategoryWithHomology C<VAR>(HomologicalComplex.quasiIso C c).HasLocalization<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<GOAL>CategoryTheory.IsIso (HomologicalComplexUpToQuasiIso.Q.map f) ↔ HomologicalComplex.quasiIso C c f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>(HomologicalComplex.quasiIso C c).HasLocalization<GOAL>(HomologicalComplex.homotopyEquivalences C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>X Y : HomotopyCategory C c<VAR>f : X ⟶ Y<GOAL>HomotopyCategory.quasiIso C c f ↔ ∀ (n : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c n).map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>K L : HomologicalComplex C c<VAR>f : K ⟶ L<GOAL>HomotopyCategory.quasiIso C c ((HomotopyCategory.quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>i : ι<GOAL>(HomotopyCategory.quasiIso C c).IsInvertedBy (HomotopyCategory.homologyFunctor C c i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<GOAL>HomotopyCategory.quasiIso C c = (HomologicalComplex.quasiIso C c).map (HomotopyCategory.quotient C c)
<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>C : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>self : c.QFactorsThroughHomotopy C<VAR>K L : HomologicalComplex C c<VAR>f g : K ⟶ L<VAR>h : Homotopy f g<GOAL>CategoryTheory.AreEqualizedByLocalization (HomologicalComplex.quasiIso C c) f g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>(HomologicalComplex.quasiIso C c).HasLocalization<VAR>c.QFactorsThroughHomotopy C<VAR>K L : HomologicalComplex C c<VAR>f g : K ⟶ L<VAR>h : Homotopy f g<GOAL>HomologicalComplexUpToQuasiIso.Q.map f = HomologicalComplexUpToQuasiIso.Q.map g
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.CategoryWithHomology C<VAR>(HomologicalComplex.quasiIso C c).HasLocalization<VAR>c.QFactorsThroughHomotopy C<GOAL>(HomotopyCategory.quasiIso C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Qh
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<GOAL>(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>CategoryTheory.CategoryWithHomology C<GOAL>c.QFactorsThroughHomotopy C
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.CategoryWithHomology C<VAR>CategoryTheory.CategoryWithHomology D<VAR>F.Additive<VAR>F.PreservesHomology<GOAL>(F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).functor = F.mapHomologicalComplex c
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.CategoryWithHomology C<VAR>CategoryTheory.CategoryWithHomology D<VAR>(HomologicalComplex.quasiIso D c).HasLocalization<VAR>F.Additive<VAR>F.PreservesHomology<GOAL>(HomologicalComplex.quasiIso C c).IsInvertedBy (F.mapHomologicalComplex c ⋙ HomologicalComplexUpToQuasiIso.Q)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.CategoryWithHomology C<VAR>CategoryTheory.CategoryWithHomology D<VAR>(HomologicalComplex.quasiIso C c).HasLocalization<VAR>(HomologicalComplex.quasiIso D c).HasLocalization<VAR>F.Additive<VAR>F.PreservesHomology<VAR>c.QFactorsThroughHomotopy C<VAR>c.QFactorsThroughHomotopy D<VAR>(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)<VAR>K : HomologicalComplex C c<GOAL>(F.mapHomologicalComplexUpToQuasiIsoFactorsh c).hom.app ((HomotopyCategory.quotient C c).obj K) = (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫ HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>l : List R<GOAL>Tropical.trop l.sum = (List.map Tropical.trop l).prod
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>s : Multiset R<GOAL>Tropical.trop s.sum = (Multiset.map Tropical.trop s).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid R<VAR>s : Finset S<VAR>f : S → R<GOAL>Tropical.trop (∑ i ∈ s, f i) = ∏ i ∈ s, Tropical.trop (f i)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>l : List (Tropical R)<GOAL>Tropical.untrop l.prod = (List.map Tropical.untrop l).sum
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>s : Multiset (Tropical R)<GOAL>Tropical.untrop s.prod = (Multiset.map Tropical.untrop s).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>Tropical.untrop (∏ i ∈ s, f i) = ∑ i ∈ s, Tropical.untrop (f i)
<VAR>R : Type u_1<VAR>LinearOrder R<VAR>l : List R<GOAL>Tropical.trop l.minimum = (List.map (Tropical.trop ∘ WithTop.some) l).sum
<VAR>R : Type u_1<VAR>LinearOrder R<VAR>OrderTop R<VAR>s : Multiset R<GOAL>Tropical.trop s.inf = (Multiset.map Tropical.trop s).sum
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>LinearOrder R<VAR>OrderTop R<VAR>s : Finset S<VAR>f : S → R<GOAL>Tropical.trop (s.inf f) = ∑ i ∈ s, Tropical.trop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → WithTop R<GOAL>Tropical.trop (sInf (f '' ↑s)) = ∑ i ∈ s, Tropical.trop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ConditionallyCompleteLinearOrder R<VAR>Fintype S<VAR>f : S → WithTop R<GOAL>Tropical.trop (⨅ i, f i) = ∑ i : S, Tropical.trop (f i)
<VAR>R : Type u_1<VAR>LinearOrder R<VAR>OrderTop R<VAR>s : Multiset (Tropical R)<GOAL>Tropical.untrop s.sum = (Multiset.map Tropical.untrop s).inf
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>LinearOrder R<VAR>OrderTop R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>Tropical.untrop (∑ i ∈ s, f i) = s.inf (Tropical.untrop ∘ f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → Tropical (WithTop R)<GOAL>Tropical.untrop (∑ i ∈ s, f i) = sInf (Tropical.untrop ∘ f '' ↑s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ConditionallyCompleteLinearOrder R<VAR>Fintype S<VAR>f : S → Tropical (WithTop R)<GOAL>Tropical.untrop (∑ i : S, f i) = ⨅ i, Tropical.untrop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ConditionallyCompleteLinearOrder R<VAR>s : Finset S<VAR>f : S → Tropical (WithTop R)<GOAL>Tropical.untrop (∑ i ∈ s, f i) = ⨅ i, Tropical.untrop (f ↑i)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>DecidableEq J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>L₁.HasMapBifunctor L₂ F c<VAR>i₁ i₁' : I₁<VAR>i₂ : I₂<VAR>j j' : J<VAR>h : c₁.π c₂ c (i₁', i₂) = j<VAR>h' : c₁.prev i₁' = i₁<GOAL>K₁.ιMapBifunctor K₂ F c i₁' i₂ j h ≫ HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j' = c₁.ε₁ c₂ c (i₁, i₂) • (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>CategoryTheory.Category.{u_8, u_1} C₁<VAR>CategoryTheory.Category.{u_9, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>DecidableEq J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>L₁.HasMapBifunctor L₂ F c<VAR>j j' : J<VAR>h : ¬c.Rel j' j<GOAL>HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j' = 0
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D : Type u_3<VAR>I₁ : Type u_4<VAR>I₂ : Type u_5<VAR>J : Type u_6<VAR>CategoryTheory.Category.{u_9, u_1} C₁<VAR>CategoryTheory.Category.{u_8, u_2} C₂<VAR>CategoryTheory.Category.{u_7, u_3} D<VAR>CategoryTheory.Preadditive C₁<VAR>CategoryTheory.Preadditive C₂<VAR>CategoryTheory.Preadditive D<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K₁ L₁ : HomologicalComplex C₁ c₁<VAR>f₁ f₁' : K₁ ⟶ L₁<VAR>h₁ : Homotopy f₁ f₁'<VAR>K₂ L₂ : HomologicalComplex C₂ c₂<VAR>f₂ : K₂ ⟶ L₂<VAR>F : C₁ ⥤ C₂ ⥤ D<VAR>F.Additive<VAR>∀ (X₁ : C₁), (F.obj X₁).Additive<VAR>c : ComplexShape J<VAR>DecidableEq J<VAR>TotalComplexShape c₁ c₂ c<VAR>K₁.HasMapBifunctor K₂ F c<VAR>L₁.HasMapBifunctor L₂ F c<VAR>i₁ i₁' : I₁<VAR>hi₁ : c₁.Rel i₁ i₁'<VAR>i₂ i₂' : I₂<VAR>hi₂ : c₂.Rel i₂ i₂'<VAR>j : J<VAR>hj : c₁.π c₂ c (i₁', i₂) = j<GOAL>c₁.ε₁ c₂ c (i₁, i₂) • (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j = -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j) ≫ HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j