ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J<VAR>this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0<GOAL>I ⊔ J ≤ (normalizedFactors I ∩ normalizedFactors J).prod
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing A<VAR>inst✝² : Field K<VAR>T : Type u_4<VAR>inst✝¹ : CommRing T<VAR>inst✝ : IsDedekindDomain T<VAR>I J : Ideal T<VAR>hI : I ≠ ⊥<VAR>hJ : J ≠ ⊥<VAR>H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J<VAR>this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0<GOAL>(normalizedFactors I ∩ normalizedFactors J).prod ≤ I ⊔ J
<VAR>R : Type u_1<VAR>inst✝⁸ : StrictOrderedCommRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : DecidableEq ι'<VAR>e : Basis ι R M<VAR>f : M ≃ₗ[R] N<GOAL>(e.map f).orientation = (Orientation.map ι f) e.orientation
<VAR>z : ℂ<VAR>x : ℝ<GOAL>(z / ↑x).im = z.im / x
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<GOAL>AntilipschitzWith 2 ⇑(addEquiv 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x‖ ≤ ↑2 * ‖(addEquiv 𝕜 A) x‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x.fst‖ ⊔ ‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖x.fst‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : NonUnitalNormedRing A<VAR>inst✝³ : NormedSpace 𝕜 A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : RegularNormedAlgebra 𝕜 A<VAR>x : Unitization 𝕜 A<GOAL>‖(algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd‖ ≤ 2 * max ‖((addEquiv 𝕜 A) x).1‖ ‖((addEquiv 𝕜 A) x).2‖
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s₁ s₂ : Stream' α<GOAL>(corec (fun x => match x with | (s₁, snd) => s₁.head) (fun x => match x with | (s₁, s₂) => (s₂, s₁.tail)) (s₁, s₂)).tail = corec (fun x => match x with | (s₁, snd) => s₁.head) (fun x => match x with | (s₁, s₂) => (s₂, s₁.tail)) (s₂, s₁.tail)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s₁ s₂ : Stream' α<GOAL>((match (s₁, s₂) with | (s₁, snd) => s₁.head) :: corec (fun x => match x with | (s₁, snd) => s₁.head) (fun x => match x with | (s₁, s₂) => (s₂, s₁.tail)) (match (s₁, s₂) with | (s₁, s₂) => (s₂, s₁.tail))).tail = corec (fun x => match x with | (s₁, snd) => s₁.head) (fun x => match x with | (s₁, s₂) => (s₂, s₁.tail)) (s₂, s₁.tail)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>g✝ : σ → S₁<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(eval₂Hom f g) ((monomial d) r) = f r * d.prod fun i k => g i ^ k
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x : ℕ<GOAL>(∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>{a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>t t' : TopologicalSpace γ<VAR>ht : PolishSpace γ<VAR>ht' : PolishSpace γ<VAR>hle : t ≤ t'<GOAL>borel γ = borel γ
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>s : Set γ<VAR>f : γ → β<VAR>t t' : TopologicalSpace γ<VAR>ht : PolishSpace γ<VAR>ht' : PolishSpace γ<VAR>hle : t ≤ t'<GOAL>borel γ ≤ borel γ
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>s✝ : Set γ<VAR>f : γ → β<VAR>t t' : TopologicalSpace γ<VAR>ht : PolishSpace γ<VAR>ht' : PolishSpace γ<VAR>hle : t ≤ t'<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>s✝ : Set γ<VAR>f : γ → β<VAR>t t' : TopologicalSpace γ<VAR>ht : PolishSpace γ<VAR>ht' : PolishSpace γ<VAR>hle : t ≤ t'<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>e : MeasurableEmbedding id<GOAL>MeasurableSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝² : T2Space β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>s✝ : Set γ<VAR>f : γ → β<VAR>t t' : TopologicalSpace γ<VAR>ht : PolishSpace γ<VAR>ht' : PolishSpace γ<VAR>hle : t ≤ t'<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>e : MeasurableEmbedding id<GOAL>s = id '' s
<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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>M₁.actRight ▷ N.X ≫ f.hom ▷ N.X = f.hom ▷ Y.X ▷ N.X ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ≫ f.hom ▷ N.X = f.hom ▷ Y.X ▷ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ M₁.X Y.X N.X).hom ≫ f.hom ▷ (Y.X ⊗ N.X) ≫ M₂.X ◁ N.actLeft = f.hom ▷ Y.X ▷ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫ (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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = (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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫ (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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ X.X M₁.X N.X).inv ≫ M₁.actLeft ▷ N.X ≫ f.hom ▷ N.X ≫ 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ X.X M₁.X N.X).inv ≫ (X.X ◁ f.hom ≫ M₂.actLeft) ▷ N.X ≫ 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ X.X M₁.X N.X).inv ≫ (X.X ◁ f.hom ≫ M₂.actLeft) ▷ N.X ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one = (X.X ◁ f.hom ▷ N.X ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ X.X M₁.X N.X).inv ≫ (X.X ◁ f.hom ≫ M₂.actLeft) ▷ N.X ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ▷ N.X ≫ (α_ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ X.X M₁.X N.X).inv ≫ (X.X ◁ f.hom ≫ M₂.actLeft) ▷ N.X ≫ 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 ◁ f.hom) ▷ N.X) ≫ 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Z.X ≫ (M₂.tensorBimod N).actRight
<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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(tensorRight Z.X).map (coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft)) ≫ (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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = (tensorRight Z.X).map (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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Z.X ≫ (M₂.tensorBimod N).actRight
<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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.X ≫ TensorBimod.actRight 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>((α_ M₁.X N.X Z.X).hom ≫ M₁.X ◁ N.actRight ≫ 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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) = coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ M₁.X N.X Z.X).hom ≫ M₁.X ◁ N.actRight ≫ f.hom ▷ N.X ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one = coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ M₁.X N.X Z.X).hom ≫ (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one = coequalizer.π (M₁.actRight ▷ N.X) ((α_ M₁.X Y.X N.X).hom ≫ M₁.X ◁ N.actLeft) ▷ Z.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) (f.hom ▷ Y.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Z.X ≫ TensorBimod.actRight 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ M₁.X N.X Z.X).hom ≫ (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one = (f.hom ▷ N.X ▷ Z.X ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one ▷ Z.X) ≫ TensorBimod.actRight 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₁ M₂ : Bimod X Y<VAR>f : M₁ ⟶ M₂<VAR>N : Bimod Y Z<GOAL>(α_ M₁.X N.X Z.X).hom ≫ (f.hom ▷ (N.X ⊗ Z.X) ≫ M₂.X ◁ N.actRight) ≫ colimit.ι (parallelPair (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)) WalkingParallelPair.one = f.hom ▷ N.X ▷ Z.X ≫ (α_ M₂.X N.X Z.X).hom ≫ M₂.X ◁ N.actRight ≫ coequalizer.π (M₂.actRight ▷ N.X) ((α_ M₂.X Y.X N.X).hom ≫ M₂.X ◁ N.actLeft)
<VAR>α : Type u<VAR>C : FreeCommRing α → Prop<VAR>z : FreeCommRing α<VAR>hn1 : C (-1)<VAR>hb : ∀ (b : α), C (of b)<VAR>ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)<VAR>hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)<VAR>hn : ∀ (x : FreeCommRing α), C x → C (-x)<VAR>h1 : C 1<VAR>m✝ : Multiplicative (Multiset α)<VAR>a : α<VAR>m : Multiset α<VAR>ih : C (FreeAbelianGroup.of m)<GOAL>FreeAbelianGroup.of (a ::ₘ m) = of a * FreeAbelianGroup.of m
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>y : Y<VAR>h : e.IsImage s t<VAR>hx : x ∈ e.source<GOAL>map (↑e) (𝓝[s] x) = 𝓝[t] ↑e x
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>X Y Z : TopCat<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>z - (starRingEnd K) z = ↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<GOAL>↑(re z) + ↑(im z) * I - (↑(re z) - ↑(im z) * I) = 2 * ↑(im z) * I