ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁✝ a₂✝ b b₁✝ b₂✝ : E<VAR>r r₁ r₂ : ℝ<VAR>a₁ a₂ b₁ b₂ : E<GOAL>|dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>h : ContinuousWithinAt f s x<VAR>hg : Tendsto g p (𝓝[s] x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<GOAL>Tendsto (fun n => F n (g n)) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>h : ContinuousWithinAt f s x<VAR>hg : Tendsto g p (𝓝[s] x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<GOAL>u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>h : ContinuousWithinAt f s x<VAR>hg : Tendsto g p (𝓝[s] x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<GOAL>u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s✝ s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>h : ContinuousWithinAt f s✝ x<VAR>hg : Tendsto g p (𝓝[s✝] x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s✝] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>s : Set α<VAR>sx : s ∈ 𝓝[s✝] x<VAR>hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁<VAR>A : ∀ᶠ (n : ι) in p, g n ∈ s<GOAL>u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s✝ s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>h : ContinuousWithinAt f s✝ x<VAR>hg : Tendsto g p (𝓝[s✝] x)<VAR>hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s✝] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>s : Set α<VAR>sx : s ∈ 𝓝[s✝] x<VAR>hs : ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u₁<VAR>A : ∀ᶠ (n : ι) in p, g n ∈ s<VAR>B : ∀ᶠ (n : ι) in p, (f x, f (g n)) ∈ u₁<GOAL>u₀ ∈ map (fun x_1 => (f x, F x_1 (g x_1))) p
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>hs : MeasurableSet s<GOAL>s ∈ ae (μ.restrict s)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>hs : MeasurableSet s<GOAL>∃ t₁ ∈ ae μ, ∃ t₂, s ⊆ t₂ ∧ s = t₁ ∩ t₂
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>s : Stream' α<VAR>x✝ : a ∈ s.even<VAR>n : ℕ<VAR>h : (fun b => a = b) (s.even.get n)<GOAL>(fun b => a = b) (s.get (2 * n))
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>a : L<VAR>h : map i f = C a<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>ha : ¬a = 0<VAR>g✝ : L[X]<VAR>hg : Irreducible g✝<VAR>x✝ : g✝ ∣ map i f<VAR>p : L[X]<VAR>hp : map i f = g✝ * p<VAR>this : (map i f).degree = (g✝ * p).degree<GOAL>g✝.degree = 0
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>a : L<VAR>h : map i f = C a<VAR>this✝ : DecidableEq L := Classical.decEq L<VAR>ha : ¬a = 0<VAR>g✝ : L[X]<VAR>hg : Irreducible g✝<VAR>x✝ : g✝ ∣ map i f<VAR>p : L[X]<VAR>hp : map i f = g✝ * p<VAR>this : g✝.degree = 0 ∧ p.degree = 0<GOAL>g✝.degree = 0
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>c : ComplexShape ι<VAR>K✝ L✝ : HomologicalComplex C c<VAR>e✝ : HomotopyEquiv K✝ L✝<VAR>inst✝² : ∀ (i : ι), K✝.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L✝.HasHomology i<VAR>inst✝ : CategoryWithHomology C<VAR>K L : HomologicalComplex C c<VAR>e : HomotopyEquiv K L<GOAL>quasiIso C c e.hom
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : Preadditive C<VAR>c : ComplexShape ι<VAR>K✝ L✝ : HomologicalComplex C c<VAR>e✝ : HomotopyEquiv K✝ L✝<VAR>inst✝² : ∀ (i : ι), K✝.HasHomology i<VAR>inst✝¹ : ∀ (i : ι), L✝.HasHomology i<VAR>inst✝ : CategoryWithHomology C<VAR>K L : HomologicalComplex C c<VAR>e : HomotopyEquiv K L<GOAL>QuasiIso e.hom
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>m : ℤ<VAR>a : α<GOAL>fract (↑m + a) = fract a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Ring R₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<GOAL>comap p.mkQ (map p.mkQ p') = p ⊔ p'
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>_l₁ _l₂ : List α<GOAL>_l₁ ≈ _l₂ ↔ ∀ (a : α), count a ⟦_l₁⟧ = count a ⟦_l₂⟧
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>_l₁ _l₂ : List α<GOAL>_l₁ ≈ _l₂ ↔ ∀ (a : α), List.count a _l₁ = List.count a _l₂
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIcoMod hp a (b - c) = toIcoMod hp (a + c) b - c
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>2 * ↑(WeierstrassCurve.expDegree n) = ↑n ^ 2 - if Even n then 4 else 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>hn : 2 * n ≠ 0<GOAL>2 * ↑(WeierstrassCurve.expDegree (2 * n)) = ↑(2 * n) ^ 2 - if Even (2 * n) then 4 else 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<VAR>hn : 2 * n + 1 ≠ 0<GOAL>2 * ↑(WeierstrassCurve.expDegree (2 * n + 1)) = ↑(2 * n + 1) ^ 2 - if Even (2 * n + 1) then 4 else 1
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>(pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) = ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>(pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫ pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) = ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>(((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫ pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫ pullback.snd g (Scheme.Opens.ι U) = (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv) ≫ pullback.snd g (Scheme.Opens.ι U)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫ pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) = ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>(((pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv) ≫ pullback.snd f (pullback.fst g (Scheme.Opens.ι U))) ≫ pullback.fst g (Scheme.Opens.ι U) = (((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫ (pullbackRestrictIsoRestrict g U).inv) ≫ pullback.fst g (Scheme.Opens.ι U)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>(pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫ pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.fst g (Scheme.Opens.ι U) = (pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι ≫ (pullbackRestrictIsoRestrict g U).inv ≫ pullback.fst g (Scheme.Opens.ι U)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>U : Opens ↑↑Z.toPresheafedSpace<GOAL>((f ≫ g) ⁻¹ᵁ U).ι ≫ f = (f ⁻¹ᵁ g ⁻¹ᵁ U).ι ≫ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>n : ℕ<GOAL>1 ^ ↑n = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>n : ℕ<GOAL>1 ^ Int.negSucc n = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Finite α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : p x<GOAL>q (e.extendSubtype x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Finite α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : { x // p x } ≃ { x // q x }<VAR>x : α<VAR>hx : p x<GOAL>e.extendSubtype x = ↑(e ⟨x, hx⟩)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : F.obj X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>(adj.homEquiv X Y') (f ≫ g) = (adj.homEquiv X Y) f ≫ G.map g
<VAR>p q : GHSpace<GOAL>dist p q = ghDist p.Rep q.Rep
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<VAR>a✝ : ι<GOAL>a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → CanonicallyLinearOrderedAddCommMonoid (α i)<VAR>inst✝ : DecidableEq ι<VAR>f g : Π₀ (i : ι), α i<VAR>a✝ : ι<GOAL>¬f a✝ ⊔ g a✝ = ⊥ ↔ ¬f a✝ = ⊥ ∨ ¬g a✝ = ⊥
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q✝ : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<VAR>q : ℕ[X]<GOAL>∀ (n : ℕ), q.smeval ↑n = ↑(q.smeval n)
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn : n ≠ 0<VAR>hp : Prime p<VAR>h : p ^ (n.factorization p + 1) ∣ n<GOAL>False
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hn : n ≠ 0<VAR>hp : Prime p<VAR>h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : GeneralizedBooleanAlgebra α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<GOAL>c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c
<VAR>α : Type u_1<VAR>inst✝¹ : GeneralizedBooleanAlgebra α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<GOAL>(∃ x ∈ P.parts, ¬c = ⊥ ∧ x \ b = c) ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c
<VAR>α : Type u_1<VAR>inst✝¹ : GeneralizedBooleanAlgebra α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>d : α<GOAL>d \ b = c → (¬c = ⊥ ↔ ¬d ≤ b)
<VAR>α : Type u_1<VAR>inst✝¹ : GeneralizedBooleanAlgebra α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>P : Finpartition a<VAR>d : α<GOAL>¬d \ b = ⊥ ↔ ¬d ≤ b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S S₁ S₂ S₃ : SnakeInput C<VAR>f : S₁ ⟶ S₂<GOAL>(pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂ = pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯ ≫ pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂
<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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>M.actRight ▷ N₁.X ≫ M.X ◁ f.hom = (M.X ⊗ Y.X) ◁ f.hom ≫ M.actRight ▷ N₂.X
<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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ M.X ◁ f.hom = (M.X ⊗ Y.X) ◁ f.hom ≫ (α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>M.X ◁ N₁.actLeft ≫ M.X ◁ f.hom = M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>M.X ◁ (Y.X ◁ f.hom ≫ N₂.actLeft) = M.X ◁ Y.X ◁ f.hom ≫ M.X ◁ N₂.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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(M.tensorBimod N₁).actLeft ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = X.X ◁ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫ (M.tensorBimod N₂).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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(tensorLeft X.X).map (coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫ (M.tensorBimod N₁).actLeft ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = (tensorLeft X.X).map (coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫ X.X ◁ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫ (M.tensorBimod N₂).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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ TensorBimod.actLeft M N₁ ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ X.X ◁ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫ TensorBimod.actLeft M N₂
<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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>((α_ X.X M.X N₁.X).inv ≫ M.actLeft ▷ N₁.X ≫ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft)) ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ X.X ◁ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫ TensorBimod.actLeft M N₂
<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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ X.X M.X N₁.X).inv ≫ M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = X.X ◁ coequalizer.π (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) ≫ X.X ◁ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ≫ TensorBimod.actLeft M N₂
<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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ X.X M.X N₁.X).inv ≫ M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = (X.X ◁ M.X ◁ f.hom ≫ X.X ◁ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one) ≫ TensorBimod.actLeft M N₂
<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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ X.X M.X N₁.X).inv ≫ M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = X.X ◁ M.X ◁ f.hom ≫ (α_ X.X M.X N₂.X).inv ≫ M.actLeft ▷ N₂.X ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ X.X M.X N₁.X).inv ≫ M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = (((α_ X.X M.X N₁.X).inv ≫ (X.X ⊗ M.X) ◁ f.hom) ≫ M.actLeft ▷ N₂.X) ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(α_ X.X M.X N₁.X).inv ≫ M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom ≫ colimit.ι (parallelPair (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft)) WalkingParallelPair.one = (α_ X.X M.X N₁.X).inv ≫ (M.actLeft ▷ N₁.X ≫ M.X ◁ f.hom) ≫ coequalizer.π (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.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>X Y Z : Mon_ C<VAR>M : Bimod X Y<VAR>N₁ N₂ : Bimod Y Z<VAR>f : N₁ ⟶ N₂<GOAL>(M.tensorBimod N₁).actRight ≫ colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) = colimMap (parallelPairHom (M.actRight ▷ N₁.X) ((α_ M.X Y.X N₁.X).hom ≫ M.X ◁ N₁.actLeft) (M.actRight ▷ N₂.X) ((α_ M.X Y.X N₂.X).hom ≫ M.X ◁ N₂.actLeft) ((M.X ⊗ Y.X) ◁ f.hom) (M.X ◁ f.hom) ⋯ ⋯) ▷ Z.X ≫ (M.tensorBimod N₂).actRight