ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<VAR>w : { w // w ≠ w₀ }<GOAL>∑ x ∈ univ.erase w, |v w x| < |v w w|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<VAR>w : { w // w ≠ w₀ }<GOAL>0 < |v w w| - v w w + ∑ x : { w // w ≠ w₀ }, v w x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B✝ : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B✝<VAR>B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }<VAR>v : { w // w ≠ w₀ } → { w // w ≠ w₀ } → ℝ := fun w => (logEmbedding K) ⋯.choose<VAR>w x : { w // w ≠ w₀ }<VAR>hx : x ∈ univ.erase w<GOAL>v w x < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>s : Set α<VAR>a : α<VAR>di : DenseInducing i<VAR>hs : s ∈ 𝓝 a<GOAL>closure (i '' s) ∈ 𝓝 (i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>s : Set α<VAR>a : α<VAR>di : DenseInducing i<VAR>hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen i_1) ∧ i ⁻¹' i_1 ⊆ s<GOAL>closure (i '' s) ∈ 𝓝 (i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>s : Set α<VAR>a : α<VAR>di : DenseInducing i<VAR>U : Set β<VAR>sub : i ⁻¹' U ⊆ s<VAR>haU : i a ∈ U<VAR>hUo : IsOpen U<GOAL>closure (i '' s) ∈ 𝓝 (i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>s : Set α<VAR>a : α<VAR>di : DenseInducing i<VAR>U : Set β<VAR>sub : i ⁻¹' U ⊆ s<VAR>haU : i a ∈ U<VAR>hUo : IsOpen U<GOAL>U ⊆ closure (i '' s)
<VAR>α : Type u_1<VAR>inst✝¹ : Lattice α<VAR>inst✝ : IsModularLattice α<VAR>x y z : α<VAR>h : z ≤ x<GOAL>x ⊓ y ⊔ z = x ⊓ (y ⊔ z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (f ∘ Subtype.val) a₁<GOAL>HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (f ∘ Subtype.val) a₁<VAR>h : HasProd f (a₁ * a₂)<GOAL>HasProd (f ∘ Subtype.val) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (s.mulIndicator f) a₁<VAR>h : HasProd f (a₁ * a₂)<GOAL>HasProd (sᶜ.mulIndicator f) a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (s.mulIndicator f) a₁<VAR>h : HasProd f (a₁ * a₂)<GOAL>HasProd (f * (s.mulIndicator f)⁻¹) a₂
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.ι j) ⁻¹' (⇑(D.ι i) '' U) = ⇑(D.t i j ≫ D.f j i) '' (⇑(D.f i j) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.t i j ≫ D.f j i) '' (⇑(D.f i j) ⁻¹' U) = ⇑(D.f j i) '' (⇑(D.t j i ≫ D.f i j) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.f j i) ∘ ⇑(D.t i j) '' (⇑(D.f i j) ⁻¹' U) = ⇑(D.f j i) '' (⇑(D.f i j) ∘ ⇑(D.t j i) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>(fun x => (forget TopCat).map (D.f j i) ((forget TopCat).map (D.t i j) x)) '' (⇑(D.f i j) ⁻¹' U) = ⇑(D.f j i) '' (⇑(D.f i j) ∘ ⇑(D.t j i) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>(forget TopCat).map (D.f j i) '' ((forget TopCat).map (D.t i j) '' (⇑(D.f i j) ⁻¹' U)) = ⇑(D.f j i) '' (⇑(D.f i j) ∘ ⇑(D.t j i) ⁻¹' U)
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>(forget TopCat).map (D.t i j) '' (⇑(D.f i j) ⁻¹' U) = ⇑(D.f i j) ∘ ⇑(D.t j i) ⁻¹' U
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>⇑(D.f i j) ⁻¹' U = (fun x => (⇑(D.f i j) ∘ ⇑(D.t j i)) ((forget TopCat).map (D.t i j) x)) ⁻¹' U
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>Function.Bijective ((forget TopCat).map (D.t i j))
<VAR>D : GlueData<VAR>i j : D.J<VAR>U : Set ↑(D.U i)<GOAL>IsIso ((forget TopCat).map (D.t i j))
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<GOAL>X✝ ◁ 0 = 0
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<GOAL>F.map (X✝ ◁ 0) = F.map 0
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<GOAL>0 ▷ X✝ = 0
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<GOAL>F.map (0 ▷ X✝) = F.map 0
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<VAR>f✝ g✝ : Y✝ ⟶ Z✝<GOAL>X✝ ◁ (f✝ + g✝) = X✝ ◁ f✝ + X✝ ◁ g✝
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<VAR>f✝ g✝ : Y✝ ⟶ Z✝<GOAL>F.map (X✝ ◁ (f✝ + g✝)) = F.map (X✝ ◁ f✝ + X✝ ◁ g✝)
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<VAR>f✝ g✝ : Y✝ ⟶ Z✝<GOAL>(f✝ + g✝) ▷ X✝ = f✝ ▷ X✝ + g✝ ▷ X✝
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_4, u_1} C<VAR>inst✝⁷ : Preadditive C<VAR>inst✝⁶ : MonoidalCategory C<VAR>inst✝⁵ : MonoidalPreadditive C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>inst✝³ : Preadditive D<VAR>inst✝² : MonoidalCategory D<VAR>F : MonoidalFunctor D C<VAR>inst✝¹ : F.Faithful<VAR>inst✝ : F.Additive<VAR>X✝ Y✝ Z✝ : D<VAR>f✝ g✝ : Y✝ ⟶ Z✝<GOAL>F.map ((f✝ + g✝) ▷ X✝) = F.map (f✝ ▷ X✝ + g✝ ▷ X✝)
<VAR>m n : Nat<GOAL>range m <+ range n ↔ m ≤ n
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>x✝ : I ^ 2 = ⊥<VAR>f₁ f₂ : Rₘ →ₐ[R] Q<VAR>a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>f₁ = f₂
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>x✝ : I ^ 2 = ⊥<VAR>f₁ f₂ : Rₘ →ₐ[R] Q<VAR>a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>↑f₁ = ↑f₂
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : CommRing Rₘ<VAR>inst✝¹¹ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝¹⁰ : Algebra R S<VAR>inst✝⁹ : Algebra R Sₘ<VAR>inst✝⁸ : Algebra S Sₘ<VAR>inst✝⁷ : Algebra R Rₘ<VAR>inst✝⁶ : Algebra Rₘ Sₘ<VAR>inst✝⁵ : IsScalarTower R Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R S Sₘ<VAR>inst✝³ : IsLocalization M Rₘ<VAR>inst✝² : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra R Q<VAR>I : Ideal Q<VAR>x✝ : I ^ 2 = ⊥<VAR>f₁ f₂ : Rₘ →ₐ[R] Q<VAR>a✝ : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂<GOAL>(↑f₁).comp (algebraMap R Rₘ) = (↑f₂).comp (algebraMap R Rₘ)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hg : UniformConvexOn s ψ g<GOAL>UniformConcaveOn s (φ + ψ) (f - g)
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>(∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f) ↔ ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset S), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b), (∀ (s : Set b), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e) ↔ ∀ (s : Finset b), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e
<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>({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.whiskerLeft f).hom = ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ M.whiskerLeft (N.whiskerLeft f) ≫ (isoOfIso { hom := AssociatorBimod.hom M N P', inv := AssociatorBimod.inv M N P', hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv).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>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.π ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ P.X) ((α_ { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X Y.X P.X).hom ≫ { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ P.actLeft) ≫ ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.whiskerLeft f).hom = coequalizer.π ({ X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ P.X) ((α_ { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X Y.X P.X).hom ≫ { X := TensorBimod.X M N, actLeft := TensorBimod.actLeft M N, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight M N, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ P.actLeft) ≫ ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ M.whiskerLeft (N.whiskerLeft f) ≫ (isoOfIso { hom := AssociatorBimod.hom M N P', inv := AssociatorBimod.inv M N P', hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv).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>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.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft) ((TensorBimod.X M N ⊗ Y.X) ◁ f.hom) (TensorBimod.X M N ◁ f.hom) ⋯ ⋯) = coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫ AssociatorBimod.hom M N P ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ TensorBimod.X N P') ((α_ M.X X.X (TensorBimod.X N P')).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) ⋯ ⋯)) ⋯ ⋯) ≫ AssociatorBimod.inv 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>TensorBimod.X M N ◁ f.hom ≫ colimit.ι (parallelPair (TensorBimod.actRight M N ▷ P'.X) ((α_ (TensorBimod.X M N) Y.X P'.X).hom ≫ TensorBimod.X M N ◁ P'.actLeft)) WalkingParallelPair.one = coequalizer.π (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) ≫ AssociatorBimod.hom M N P ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M.actRight ▷ TensorBimod.X N P') ((α_ M.X X.X (TensorBimod.X N P')).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) ⋯ ⋯)) ⋯ ⋯) ≫ AssociatorBimod.inv 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) ◁ 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.π (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) ≫ coequalizer.desc (AssociatorBimod.homAux M 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) ⋯ ⋯)) ⋯ ⋯) ≫ AssociatorBimod.inv 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) ◁ 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 = (AssociatorBimod.homAux M 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) ⋯ ⋯)) ⋯ ⋯)) ≫ AssociatorBimod.inv 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) ◁ 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 = (((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') ⋯