ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>(tensorRight P.X).map (coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (tensorRight P.X).map (coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) ≫ (((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P.X).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P') ((M.X ⊗ X.X) ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯)) (M.X ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯)) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.invAux M N P') ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ (((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P.X).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P') ((M.X ⊗ X.X) ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯)) (M.X ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯)) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.invAux M N P') ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (((α_ M.X N.X P.X).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)) ≫ colimMap (parallelPairHom (M.actRight ▷ coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P') ((M.X ⊗ X.X) ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯)) (M.X ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯)) ⋯ ⋯)) ≫ coequalizer.desc (AssociatorBimod.invAux M N P') ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ (M.X ◁ colimMap (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft) ((N.X ⊗ Y.X) ◁ f.hom) (N.X ◁ f.hom) ⋯ ⋯) ≫ colimit.ι (parallelPair (M.actRight ▷ coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P')) WalkingParallelPair.one) ≫ coequalizer.desc (AssociatorBimod.invAux M N P') ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ (M.X ◁ (N.X ◁ f.hom ≫ colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) WalkingParallelPair.one) ≫ colimit.ι (parallelPair (M.actRight ▷ coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) ((α_ M.X X.X (coequalizer (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft))).hom ≫ M.X ◁ TensorBimod.actLeft N P')) WalkingParallelPair.one) ≫ coequalizer.desc (AssociatorBimod.invAux M N P') ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ M.X ◁ (N.X ◁ f.hom ≫ colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) WalkingParallelPair.one) ≫ AssociatorBimod.invAux M N P'
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ M.X ◁ (N.X ◁ f.hom ≫ colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) WalkingParallelPair.one) ≫ (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X P'.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ ((M.X ◁ N.X ◁ f.hom ≫ M.X ◁ colimit.ι (parallelPair (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)) WalkingParallelPair.one) ≫ (PreservesCoequalizer.iso (tensorLeft M.X) (N.actRight ▷ P'.X) ((α_ N.X Y.X P'.X).hom ≫ N.X ◁ P'.actLeft)).inv) ≫ coequalizer.desc ((α_ M.X N.X P'.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ M.X ◁ N.X ◁ f.hom ≫ (α_ M.X N.X P'.X).inv ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X ≫ coequalizer.π (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = (α_ M.X N.X P.X).hom ≫ (((α_ M.X N.X P.X).inv ≫ (M.X ⊗ N.X) ◁ f.hom) ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X) ≫ coequalizer.π (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = ((M.X ⊗ N.X) ◁ f.hom ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X) ≫ coequalizer.π (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M : Bimod W X<VAR>N : Bimod X Y<VAR>P P' : Bimod Y Z<VAR>f : P ⟶ P'<GOAL>((M.X ⊗ N.X) ◁ f.hom ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X) ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft)) Y.X P'.X).hom ≫ coequalizer (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ◁ P'.actLeft)) WalkingParallelPair.one = ((M.X ⊗ N.X) ◁ f.hom ≫ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P'.X) ≫ coequalizer.π (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>ab : a ≤ b<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : α → E<VAR>s✝ : Set α<VAR>f : α → E<VAR>s : Set α<VAR>hf : LocallyBoundedVariationOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>ba : b ≤ a<GOAL>variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → edist (f x) (f y) = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<GOAL>[].prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) []).sum
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<GOAL>∀ b ∈ Finsupp.support 1, degb b ≤ 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>f : R[A]<VAR>fs : List R[A]<GOAL>(f :: fs).prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) (f :: fs)).sum
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degb0 : degb 0 ≤ 0<VAR>degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b<VAR>f : R[A]<VAR>fs : List R[A]<GOAL>(f * fs.prod).support.sup degb ≤ f.support.sup degb + (List.map (fun f => f.support.sup degb) fs).sum
<VAR>m n : ℕ<VAR>k : Fin (n + 1)<GOAL>¬k - 1 < k ↔ ¬0 < k
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x h : (i : ι) → M₁ i<GOAL>∑ x_1 ∈ filter (fun x => 2 ≤ x.card) Finset.univ.powerset, f (x_1.piecewise h x) + ∑ x_1 ∈ filter (fun x => ¬2 ≤ x.card) Finset.univ.powerset, f (x_1.piecewise h x) = f x + (f.linearDeriv x) h + ∑ s ∈ filter (fun x => 2 ≤ x.card) Finset.univ.powerset, f (s.piecewise h x)
<VAR>ι : Type u_1<VAR>π : ι → Sort u_2<VAR>s : Finset ι<VAR>f g : (i : ι) → π i<VAR>inst✝¹ : (j : ι) → Decidable (j ∈ s)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<GOAL>{i}.piecewise f g = update g i (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a✝ b : α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>a ⊔ ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a ⊔ f i j
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>hu : ¬liminf u f = ⊥<VAR>hv : ¬liminf v f = ⊥<GOAL>liminf u f + liminf v f ≤ liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>hu : ¬liminf u f = ⊥<VAR>hv : ¬liminf v f = ⊥<VAR>h' : limsup (-(u + v)) f = limsup (-u + -v) f<GOAL>liminf u f + liminf v f ≤ liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>hu : ¬liminf u f = ⊥<VAR>hv : ¬liminf v f = ⊥<VAR>h' : limsup (-(u + v)) f = limsup (-u + -v) f<GOAL>-liminf (u + v) f ≤ -liminf u f + -liminf v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>hu : ¬-liminf u f = ⊤<VAR>hv : ¬-liminf v f = ⊤<VAR>h' : limsup (-(u + v)) f = limsup (-u + -v) f<GOAL>-liminf (u + v) f ≤ -liminf u f + -liminf v f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h' : limsup (-(u + v)) f = limsup (-u + -v) f<VAR>hu : ¬limsup (-u) f = ⊤<VAR>hv : ¬limsup (-v) f = ⊤<GOAL>limsup (-(u + v)) f ≤ limsup (-u) f + limsup (-v) f