ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>j : Fin (n + 1) →₀ ℕ<VAR>r : R<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<GOAL>coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>r : R<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<GOAL>coeff m (if i = (cons i m) 0 then ∏ x : Fin n, X x ^ (cons i m) x.succ else 0) = if cons i m = cons i m then 1 else 0
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>j : Fin (n + 1) →₀ ℕ<VAR>r : R<VAR>m : Fin n →₀ ℕ<VAR>i : ℕ<VAR>hjmi : j ≠ cons i m<GOAL>coeff m (if i = j 0 then ∏ x : Fin n, X x ^ j x.succ else 0) = if j = cons i m then 1 else 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>p.divX.coeff n = p.coeff (n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>p.divX.coeff n = p.coeff (1 + n)
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I : Box ι<VAR>i : ι<GOAL>dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>inst✝ : Fintype ι<VAR>I : Box ι<VAR>i : ι<VAR>A : I.lower i - I.upper i < 0<GOAL>dist I.lower I.upper ≤ ↑I.distortion * (I.upper i - I.lower i)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : Mono (terminal.from A)<VAR>Z : C<VAR>f g : Z ⟶ A<GOAL>f = g
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A : C<VAR>inst✝¹ : HasTerminal C<VAR>inst✝ : Mono (terminal.from A)<VAR>Z : C<VAR>f g : Z ⟶ A<GOAL>f ≫ terminal.from A = g ≫ terminal.from A
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>↑(p / r) ≤ ↑p / ↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i✝ j : Set α<VAR>hs : VectorMeasure.restrict s univ ≤ VectorMeasure.restrict 0 univ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure i = ↑(-s) i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<GOAL>h.coeff z i = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<GOAL>{ toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>z : S<VAR>i : ℕ<VAR>hi : f.natDegree ≤ i<VAR>a✝ : Nontrivial R<GOAL>{ toFun := Polynomial.coeff, map_add' := ⋯ } (h.modByMonicHom z) i = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>n : ℕ<VAR>a : α<VAR>h : replicate n a ≠ []<GOAL>(replicate n a).head h = a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a b : α<VAR>inst✝ : SemilatticeSup γ<VAR>s : Set γ<VAR>x₀ : γ<GOAL>BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a b : α<VAR>inst✝ : SemilatticeSup γ<VAR>s : Set γ<VAR>x₀ : γ<GOAL>Monotone fun x => ∀ y ∈ s, y ≤ 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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>coequalizer.desc ((PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ⋯) ⋯ ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ⋯) ⋯ ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>((PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ⋯) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(tensorLeft P.X).map (coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫ ((PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ⋯) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = (tensorLeft P.X).map (coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ ((PreservesCoequalizer.iso (tensorLeft P.X) (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ⋯) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>((α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ coequalizer.π (TensorBimod.actRight P Q ▷ L.X) ((α_ (TensorBimod.X P Q) T.X L.X).hom ≫ TensorBimod.X P Q ◁ L.actLeft)) ≫ coequalizer.desc ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯) ⋯ = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(α_ P.X Q.X L.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫ (PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫ coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L)) ⋯ = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>(α_ P.X Q.X L.X).inv ≫ (α_ P.X Q.X L.X).hom ≫ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ TensorBimod.X Q L) ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (TensorBimod.X P (Q.tensorBimod L))
<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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft) ≫ 𝟙 (coequalizer (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).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>R S T U : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>L : Bimod T U<GOAL>P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)) ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫ P.X ◁ TensorBimod.actLeft Q L) = P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫ coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X) ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<GOAL>∀ (s : Multiset α), (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<GOAL>(∀ a ∈ 0, p a) → f (prod 0) ≤ (map f 0).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<GOAL>∀ (a : α) (s : Multiset α), ((∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod) → (∀ a_2 ∈ a ::ₘ s, p a_2) → f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hpsa : ∀ a_1 ∈ a ::ₘ s, p a_1<GOAL>f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hpsa : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hps : ∀ x ∈ s, p x<GOAL>f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hpsa : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hps : ∀ x ∈ s, p x<VAR>hp_prod : p s.prod<GOAL>f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : OrderedCommMonoid β<VAR>f : α → β<VAR>p : α → Prop<VAR>h_one : f 1 = 1<VAR>hp_one : p 1<VAR>h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b<VAR>hp_mul : ∀ (a b : α), p a → p b → p (a * b)<VAR>a : α<VAR>s : Multiset α<VAR>hs : (∀ a ∈ s, p a) → f s.prod ≤ (map f s).prod<VAR>hpsa : ∀ a_1 ∈ a ::ₘ s, p a_1<VAR>hps : ∀ x ∈ s, p x<VAR>hp_prod : p s.prod<GOAL>f (a * s.prod) ≤ f a * (map f s).prod
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>x✝¹ : 0 ≤ as.size<VAR>x✝ : β<GOAL>forIn.loop as f 0 x✝¹ x✝ = forIn (List.drop as.data.length as.data) x✝ f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>x✝¹ : 0 ≤ as.size<VAR>x✝ : β<GOAL>forIn.loop as f 0 x✝¹ x✝ = forIn [] x✝ f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<GOAL>(do let __do_lift ← f as[as.size - 1 - i] x✝ match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = forIn (List.drop j as.data) x✝ f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<GOAL>(do let __do_lift ← f as[as.size - 1 - i] x✝ match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = forIn (List.drop j as.data) x✝ f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this : as.size - 1 - i < as.size<GOAL>(do let __do_lift ← f as[as.size - 1 - i] x✝ match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = forIn (List.drop j as.data) x✝ f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<GOAL>(do let __do_lift ← f as[as.size - 1 - i] x✝ match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = forIn (List.drop j as.data) x✝ f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<GOAL>(do let __do_lift ← f as[as.size - 1 - i] x✝ match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = do let x ← f as[as.size - 1 - i] x✝ match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn (List.drop (j + 1) as.data) b f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<GOAL>(fun __do_lift => match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = fun x => match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn (List.drop (j + 1) as.data) b f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<VAR>x : ForInStep β<GOAL>(match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn.loop as f i ⋯ b) = match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn (List.drop (j + 1) as.data) b f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<VAR>x : ForInStep β<GOAL>(fun b => forIn.loop as f i ⋯ b) = fun b => forIn (List.drop (j + 1) as.data) b f