ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace M✝<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : ContinuousMul M✝<VAR>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : ι → X → M<VAR>hf : LocallyFinite fun i => mulSupport (f i)<VAR>x₀ : X<VAR>U : Set X<VAR>hxU : U ∈ 𝓝 x₀<VAR>hUf : {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}.Finite<VAR>y : X<VAR>hy : y ∈ U<VAR>i : ι<VAR>hi : i ∈ mulSupport fun i => f i y<GOAL>i ∈ {i | ((fun i => mulSupport (f i)) i ∩ U).Nonempty}
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#(α ↪ β) = 0 ↔ #β < #α
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>h✝ h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ<GOAL>⇑h '' Metric.sphere x r = Metric.sphere (h x) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>x✝ : α<GOAL>x✝ ≠ a ∧ x✝ ∈ s ↔ x✝ ∈ ↑s \ {a}
<VAR>K✝ : Type uK<VAR>inst✝⁷ : Field K✝<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁶ : AddCommGroup V₁<VAR>inst✝⁵ : Module K✝ V₁<VAR>inst✝⁴ : AddCommGroup V₂<VAR>inst✝³ : Module K✝ V₂<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>W : Submodule K (Dual K V)<VAR>x✝ : FiniteDimensional K ↥W<GOAL>FiniteDimensional K (V ⧸ W.dualCoannihilator)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>s.append nil = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = s.append nil ∧ s2 = s) (s.append nil).destruct s.destruct
<VAR>n : ℕ<GOAL>n# ≤ 4 ^ n
<VAR>n : ℕ<VAR>ihn : ∀ m < n, m# ≤ 4 ^ m<GOAL>n# ≤ 4 ^ n
<VAR>n : ℕ<VAR>ihn : ∀ m < n + 1, m# ≤ 4 ^ m<GOAL>(n + 1)# ≤ 4 ^ (n + 1)
<VAR>m : ℕ<VAR>ihn : ∀ m_1 < m + m + 1, m_1# ≤ 4 ^ m_1<GOAL>(m + m + 1)# ≤ 4 ^ (m + m + 1)
<VAR>n : ℕ<VAR>ihn : ∀ m < n + 1, m# ≤ 4 ^ m<VAR>ho : Odd n<GOAL>(n + 1)# ≤ 4 ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>h : ∀ (x : α), p x → q (f x)<VAR>x : β<VAR>hx : q x<GOAL>⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' {x | p x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>h : ∀ (x : α), p x → q (f x)<VAR>x : β<VAR>hx : q x<GOAL>(∃ a, ∃ (h_1 : p a), ⟨f a, ⋯⟩ = ⟨x, hx⟩) ↔ ∃ x_1 ∈ {x | p x}, f x_1 = x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>p : Submodule K V<VAR>hp : p < ⊤<GOAL>∃ f, f ≠ 0 ∧ p ≤ ker f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>p : Submodule K V<VAR>hp : p < ⊤<VAR>v : V<VAR>hpv : v ∉ p<GOAL>∃ f, f ≠ 0 ∧ p ≤ ker f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>p : Submodule K V<VAR>v : V<VAR>hpv : v ∉ p<GOAL>∃ f, f ≠ 0 ∧ p ≤ ker f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>p : Submodule K V<VAR>v : V<VAR>hpv : v ∉ p<VAR>f : V →ₗ[K] K<VAR>hf : f ∘ₗ ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).domain.subtype = ({ domain := p, toFun := 0 }.supSpanSingleton v 1 hpv).toFun<GOAL>∃ f, f ≠ 0 ∧ p ≤ ker f
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>(whiskerRight (isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom Q ≫ (isoOfIso { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ M.whiskerLeft (isoOfIso { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom).hom = ((isoOfIso { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ (isoOfIso { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q), hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom).hom
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>coequalizer.π (((M.tensorBimod N).tensorBimod P).actRight ▷ Q.X) ((α_ ((M.tensorBimod N).tensorBimod P).X Y.X Q.X).hom ≫ ((M.tensorBimod N).tensorBimod P).X ◁ Q.actLeft) ≫ (whiskerRight (isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom Q ≫ (isoOfIso { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ M.whiskerLeft (isoOfIso { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom).hom = coequalizer.π (((M.tensorBimod N).tensorBimod P).actRight ▷ Q.X) ((α_ ((M.tensorBimod N).tensorBimod P).X Y.X Q.X).hom ≫ ((M.tensorBimod N).tensorBimod P).X ◁ Q.actLeft) ≫ ((isoOfIso { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ (isoOfIso { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q), hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom).hom
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X) ((α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X).hom ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft) ≫ colimMap (parallelPairHom (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X) ((α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X).hom ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft) (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X) ((α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X).hom ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft) (coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Y.X ▷ Q.X) (coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X) ⋯ ⋯) ≫ coequalizer.desc (AssociatorBimod.homAux M (N.tensorBimod P) Q) ⋯ ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) = coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X) ((α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X).hom ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft) ≫ coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯ ≫ coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>((coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫ colimit.ι (parallelPair (TensorBimod.actRight M (N.tensorBimod P) ▷ Q.X) ((α_ (TensorBimod.X M (N.tensorBimod P)) Y.X Q.X).hom ≫ TensorBimod.X M (N.tensorBimod P) ◁ Q.actLeft)) WalkingParallelPair.one) ≫ coequalizer.desc (AssociatorBimod.homAux M (N.tensorBimod P) Q) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) = coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X) ((α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X).hom ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft) ≫ coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯ ≫ coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫ AssociatorBimod.homAux M (N.tensorBimod P) Q ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) = coequalizer.π (TensorBimod.actRight (M.tensorBimod N) P ▷ Q.X) ((α_ (TensorBimod.X (M.tensorBimod N) P) Y.X Q.X).hom ≫ TensorBimod.X (M.tensorBimod N) P ◁ Q.actLeft) ≫ coequalizer.desc (AssociatorBimod.homAux (M.tensorBimod N) P Q) ⋯ ≫ coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>coequalizer.desc (AssociatorBimod.homAux M N P) ⋯ ▷ Q.X ≫ AssociatorBimod.homAux M (N.tensorBimod P) Q ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) (M.X ◁ coequalizer.desc (AssociatorBimod.homAux N P Q) ⋯) ⋯ ⋯) = AssociatorBimod.homAux (M.tensorBimod N) P Q ≫ coequalizer.desc (AssociatorBimod.homAux M N (P.tensorBimod Q)) ⋯
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>((((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X W.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 X.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)) ⋯) ▷ Q.X ≫ (PreservesCoequalizer.iso (tensorRight Q.X) (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)).inv) ≫ coequalizer.desc ((α_ M.X (TensorBimod.X N P) Q.X).hom ≫ M.X ◁ coequalizer.π (TensorBimod.actRight N P ▷ Q.X) ((α_ (TensorBimod.X N P) Y.X Q.X).hom ≫ TensorBimod.X N P ◁ Q.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) (M.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) ⋯ ⋯) = (α_ (TensorBimod.X M N) P.X Q.X).hom ≫ TensorBimod.X M N ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (PreservesCoequalizer.iso (tensorRight (TensorBimod.X P Q)) (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X (TensorBimod.X P Q)).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))) ⋯
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ▷ Q.X ≫ ((((PreservesCoequalizer.iso (tensorRight P.X) (M.actRight ▷ N.X) ((α_ M.X W.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 X.X P.X).hom ≫ N.X ◁ P.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)) ⋯) ▷ Q.X ≫ (PreservesCoequalizer.iso (tensorRight Q.X) (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)).inv) ≫ coequalizer.desc ((α_ M.X (TensorBimod.X N P) Q.X).hom ≫ M.X ◁ coequalizer.π (TensorBimod.actRight N P ▷ Q.X) ((α_ (TensorBimod.X N P) Y.X Q.X).hom ≫ TensorBimod.X N P ◁ Q.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) (M.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) ⋯ ⋯) = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ▷ Q.X ≫ (α_ (TensorBimod.X M N) P.X Q.X).hom ≫ TensorBimod.X M N ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (PreservesCoequalizer.iso (tensorRight (TensorBimod.X P Q)) (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X (TensorBimod.X P Q)).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))) ⋯
<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>V W X Y Z : Mon_ C<VAR>M : Bimod V W<VAR>N : Bimod W X<VAR>P : Bimod X Y<VAR>Q : Bimod Y Z<GOAL>((((α_ M.X N.X P.X).hom ▷ Q.X ≫ (M.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)) ▷ Q.X ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) ▷ Q.X) ≫ (PreservesCoequalizer.iso (tensorRight Q.X) (M.actRight ▷ TensorBimod.X N P) ((α_ M.X W.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P)).inv) ≫ coequalizer.desc ((α_ M.X (TensorBimod.X N P) Q.X).hom ≫ M.X ◁ coequalizer.π (TensorBimod.actRight N P ▷ Q.X) ((α_ (TensorBimod.X N P) Y.X Q.X).hom ≫ TensorBimod.X N P ◁ Q.actLeft) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q)) ⋯) ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X (N.tensorBimod P) Q) ((α_ M.X W.X (TensorBimod.X (N.tensorBimod P) Q)).hom ≫ M.X ◁ TensorBimod.actLeft (N.tensorBimod P) Q) (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q)) ((M.X ⊗ W.X) ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) (M.X ◁ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight Q.X) (N.actRight ▷ P.X) ((α_ N.X X.X P.X).hom ≫ N.X ◁ P.actLeft)).inv ≫ coequalizer.desc ((α_ N.X P.X Q.X).hom ≫ N.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q)) ⋯) ⋯) ⋯ ⋯) = coequalizer.π (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft) ▷ P.X ▷ Q.X ≫ (α_ (TensorBimod.X M N) P.X Q.X).hom ≫ TensorBimod.X M N ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X Y.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ (PreservesCoequalizer.iso (tensorRight (TensorBimod.X P Q)) (M.actRight ▷ N.X) ((α_ M.X W.X N.X).hom ≫ M.X ◁ N.actLeft)).inv ≫ coequalizer.desc ((α_ M.X N.X (TensorBimod.X P Q)).hom ≫ M.X ◁ coequalizer.π (N.actRight ▷ TensorBimod.X P Q) ((α_ N.X X.X (TensorBimod.X P Q)).hom ≫ N.X ◁ TensorBimod.actLeft P Q) ≫ coequalizer.π (M.actRight ▷ TensorBimod.X N (P.tensorBimod Q)) ((α_ M.X W.X (TensorBimod.X N (P.tensorBimod Q))).hom ≫ M.X ◁ TensorBimod.actLeft N (P.tensorBimod Q))) ⋯