ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x₁ x₂ y₁ y₂ : X<VAR>hsat₁ : IsMaximal (last s) x₁<VAR>hsat₂ : IsMaximal (last s) x₂<VAR>hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁<VAR>hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂<VAR>hr₁ : Iso (last s, x₁) (x₂, y₂)<VAR>hr₂ : Iso (x₁, y₁) (last s, x₂)<VAR>e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc<VAR>h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc<VAR>x✝ : Fin s.length<GOAL>x✝.castSucc.castSucc < Fin.last (s.length + 1)
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s<GOAL>riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : riemannZeta s = 1 / ↑0 ^ s + ∑' (b : ℕ), 1 / ↑(b + 1) ^ s<GOAL>riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>this : riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s<GOAL>Summable fun n => 1 / ↑n ^ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<GOAL>∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>this : L.mapArrow.EssSurj<GOAL>∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>this : L.mapArrow.EssSurj<VAR>φ : Arrow C<VAR>e : L.mapArrow.obj φ ≅ Arrow.mk f<GOAL>∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>this : L.mapArrow.EssSurj<VAR>φ : Arrow C<VAR>e : L.mapArrow.obj φ ≅ Arrow.mk f<VAR>Z : C<VAR>g : (𝟭 C).obj φ.right ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)<VAR>H : Triangle.mk φ.hom g h ∈ distinguishedTriangles<GOAL>∃ Z g h, Triangle.mk f g h ∈ L.essImageDistTriang
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>this : L.mapArrow.EssSurj<VAR>φ : Arrow C<VAR>e : L.mapArrow.obj φ ≅ Arrow.mk f<VAR>Z : C<VAR>g : (𝟭 C).obj φ.right ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)<VAR>H : Triangle.mk φ.hom g h ∈ distinguishedTriangles<GOAL>Triangle.mk f (e.inv.right ≫ L.map g) (L.map h ≫ (L.commShiftIso 1).hom.app ((𝟭 C).obj φ.left) ≫ (shiftFunctor D 1).map e.hom.left) ≅ L.mapTriangle.obj (Triangle.mk φ.hom g h)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>this : L.mapArrow.EssSurj<VAR>φ : Arrow C<VAR>e : L.mapArrow.obj φ ≅ Arrow.mk f<VAR>Z : C<VAR>g : (𝟭 C).obj φ.right ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)<VAR>H : Triangle.mk φ.hom g h ∈ distinguishedTriangles<GOAL>(Triangle.mk f (e.inv.right ≫ L.map g) (L.map h ≫ (L.commShiftIso 1).hom.app ((𝟭 C).obj φ.left) ≫ (shiftFunctor D 1).map e.hom.left)).mor₃ ≫ (shiftFunctor D 1).map (Arrow.leftFunc.mapIso e.symm).hom = (Iso.refl (Triangle.mk f (e.inv.right ≫ L.map g) (L.map h ≫ (L.commShiftIso 1).hom.app ((𝟭 C).obj φ.left) ≫ (shiftFunctor D 1).map e.hom.left)).obj₃).hom ≫ (L.mapTriangle.obj (Triangle.mk φ.hom g h)).mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁵ : Category.{u_4, u_1} C<VAR>inst✝¹⁴ : Category.{u_3, u_2} D<VAR>L : C ⥤ D<VAR>inst✝¹³ : HasShift C ℤ<VAR>inst✝¹² : Preadditive C<VAR>inst✝¹¹ : HasZeroObject C<VAR>inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝⁹ : Pretriangulated C<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : L.CommShift ℤ<VAR>W : MorphismProperty C<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : W.IsCompatibleWithTriangulation<VAR>inst✝⁴ : W.HasLeftCalculusOfFractions<VAR>inst✝³ : Preadditive D<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝ : L.Additive<VAR>X Y : D<VAR>f : X ⟶ Y<VAR>this : L.mapArrow.EssSurj<VAR>φ : Arrow C<VAR>e : L.mapArrow.obj φ ≅ Arrow.mk f<VAR>Z : C<VAR>g : (𝟭 C).obj φ.right ⟶ Z<VAR>h : Z ⟶ (shiftFunctor C 1).obj ((𝟭 C).obj φ.left)<VAR>H : Triangle.mk φ.hom g h ∈ distinguishedTriangles<GOAL>(L.map h ≫ (L.commShiftIso 1).hom.app φ.left ≫ (shiftFunctor D 1).map e.hom.left) ≫ (shiftFunctor D 1).map e.inv.left = 𝟙 (L.obj Z) ≫ L.map h ≫ (L.commShiftIso 1).hom.app φ.left
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>mapIdx.go f (l ++ [e]) #[] = mapIdx.go f l #[] ++ [f l.length e]
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<VAR>l : List α<VAR>e : α<GOAL>mapIdx.go f [e] (toArray (mapIdx.go f l #[])) = mapIdx.go f l #[] ++ [f l.length e]
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x : L<GOAL>∃ k, (toEnd R L M) x ^ k = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsNilpotent R L M<VAR>x : L<VAR>this : ∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0<GOAL>∃ k, (toEnd R L M) x ^ k = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>x y : E<GOAL>HasSum (fun i => ⟪x, (fun i => b.repr.symm (lp.single 2 i 1)) i⟫_𝕜 * ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, y⟫_𝕜) ⟪x, y⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>x y : E<GOAL>(fun i => ⟪x, (fun i => b.repr.symm (lp.single 2 i 1)) i⟫_𝕜 * ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, y⟫_𝕜) = fun b_1 => ((innerSL 𝕜) x) (↑(b.repr y) b_1 • (fun i => b.repr.symm (lp.single 2 i 1)) b_1)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<VAR>x y : E<VAR>i : ι<GOAL>⟪x, (fun i => b.repr.symm (lp.single 2 i 1)) i⟫_𝕜 * ⟪(fun i => b.repr.symm (lp.single 2 i 1)) i, y⟫_𝕜 = ((innerSL 𝕜) x) (↑(b.repr y) i • (fun i => b.repr.symm (lp.single 2 i 1)) i)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<GOAL>a.factors ≤ b.factors ↔ a ≤ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>h : a.factors ≤ b.factors<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>h : a.factors ≤ b.factors<VAR>this : a.factors.prod ≤ b.factors.prod<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<GOAL>BddBelow ↑(upperClosure s) ↔ BddBelow s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S T : Set R<GOAL>closure S * closure T = closure (S * T)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S T : Set R<GOAL>closure S * closure T ≤ closure (S * T)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>S T : Set R<GOAL>closure (S * T) ≤ closure S * closure T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>this✝ : Fintype β<VAR>this : Fintype α<GOAL>Nat.card α ≤ Nat.card β
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<GOAL>Continuous (f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})))
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<GOAL>Continuous (f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) ∘ CondensedSet.coinducingCoprod X)
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<GOAL>∀ (i : (S : CompHaus) × X.val.obj (Opposite.op S)), Continuous fun a => (f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) ∘ CondensedSet.coinducingCoprod X) ⟨i, a⟩
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous fun a => (f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) ∘ CondensedSet.coinducingCoprod X) ⟨⟨S, x⟩, a⟩
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous fun a => f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) (X.val.map (CompHaus.const S a).op x)
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<VAR>this : (fun a => f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) (X.val.map (CompHaus.const S a).op x)) = fun a => Y.val.map (CompHaus.const S a).op (f.val.app (Opposite.op S) x)<GOAL>Continuous fun a => f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) (X.val.map (CompHaus.const S a).op x)
<VAR>X Y : CondensedSet<VAR>f : X ⟶ Y<VAR>S : CompHaus<VAR>x : X.val.obj (Opposite.op S)<VAR>this : (fun a => f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1})) (X.val.map (CompHaus.const S a).op x)) = fun a => Y.val.map (CompHaus.const S a).op (f.val.app (Opposite.op S) x)<GOAL>Continuous fun a => Y.val.map (CompHaus.const S a).op (f.val.app (Opposite.op S) x)
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y✝ : (i : δ) → π i<VAR>i : δ<VAR>x y : (i : δ) → π i<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>h : ∀ i ∉ s, x i = y i<GOAL>(∫⋯∫⁻_s, f ∂μ) x = (∫⋯∫⁻_s, f ∂μ) y
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y✝ : (i : δ) → π i<VAR>i : δ<VAR>x y : (i : δ) → π i<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>h : ∀ i ∉ s, x i = y i<GOAL>(∫⁻ (y : (i : { x // x ∈ s }) → π ↑i), f fun i => if hi : i ∈ s then y ⟨i, hi⟩ else x i ∂Measure.pi fun i => μ ↑i) = ∫⁻ (y_1 : (i : { x // x ∈ s }) → π ↑i), f fun i => if hi : i ∈ s then y_1 ⟨i, hi⟩ else y i ∂Measure.pi fun i => μ ↑i
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.22117, u_1} C<VAR>inst✝ : Preadditive C<VAR>P Q : Karoubi C<VAR>f : P ⟶ Q<GOAL>-f.f = P.p ≫ (-f.f) ≫ Q.p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>y : Y<VAR>f : X → Y<VAR>h : Continuous f<VAR>h' : EqOn f (fun x => y) s<GOAL>Tendsto f (𝓝ˢ s) (𝓝 y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f✝ : Filter X<VAR>s t s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>y : Y<VAR>f : X → Y<VAR>h : Continuous f<VAR>h' : EqOn f (fun x => y) s<GOAL>Tendsto f (𝓝ˢ s) (𝓝ˢ {y})
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.172711, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.172711, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.172711, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.172711, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.172711, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.172711, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<GOAL>∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<GOAL>∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<GOAL>∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<GOAL>∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<GOAL>∀ᶠ (x : ℕ) in atTop, b i ^ p a b * ↑x ^ p a b * (1 + ε ↑x) ≤ ↑(r i x) ^ p a b * (1 + ε ↑(r i x))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<GOAL>b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)<GOAL>b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ ↑(r i n) ^ p a b * (1 + ε ↑(r i n))
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)<GOAL>b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n) ≤ q ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>q : ℝ → ℝ := fun x => x ^ p a b * (1 + ε x)<VAR>h_diff_q : DifferentiableOn ℝ q (Set.Ioi 1)<VAR>h_deriv_q : deriv q =O[atTop] fun x => x ^ (p a b - 1)<VAR>h_main_norm : (fun n => ‖q ↑(r i n) - q (b i * ↑n)‖) ≤ᶠ[atTop] fun n => ‖b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)‖<VAR>h_main : (fun n => q (b i * ↑n) - q ↑(r i n)) ≤ᶠ[atTop] fun n => b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>n : ℕ<VAR>hn : q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)<VAR>h₁ : q (b i * ↑n) - b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n) = b i ^ p a b * ↑n ^ p a b * (1 + ε ↑n)<GOAL>q (b i * ↑n) - q ↑(r i n) ≤ b i ^ p a b * ↑n ^ p a b * (ε (b i * ↑n) - ε ↑n)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.282116, u_1} D<VAR>F G : C ⥤ D<VAR>η : F ⟶ G<VAR>X Y : WithInitial C<VAR>f : X ⟶ Y<GOAL>(map F).map f ≫ (fun X => match X with | of x => η.app x | star => 𝟙 star) Y = (fun X => match X with | of x => η.app x | star => 𝟙 star) X ≫ (map G).map f
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>n✝¹ : μ<VAR>s : Finset ι<VAR>n✝ : μ<VAR>f : ι → μ<VAR>n x₁ x₂ : μ<GOAL>(x₁, x₂) ∈ (Equiv.boolArrowEquivProd μ).finsetCongr (univ.piAntidiag n) ↔ (x₁, x₂) ∈ antidiagonal n
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>n✝¹ : μ<VAR>s : Finset ι<VAR>n✝ : μ<VAR>f : ι → μ<VAR>n x₁ x₂ : μ<GOAL>(∃ a ∈ univ.piAntidiag n, a = (Equiv.boolArrowEquivProd μ).symm (x₁, x₂)) ↔ (x₁, x₂) ∈ antidiagonal n
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s✝ : Set (α → M)<VAR>s : Set (β → M)<VAR>h : A.Definable L s<VAR>f : α ≃ β<GOAL>A.Definable L ((fun g => g ∘ ⇑f) '' s)