ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hg : ∀ (b : δ), IsLUB (range fun i => f i b) (g b)<GOAL>∀ t ∈ range Ioi, MeasurableSet (g ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hg : ∀ (b : δ), IsLUB (range fun i => f i b) (g b)<VAR>a : α<GOAL>MeasurableSet (g ⁻¹' Ioi a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>hg : ∀ (b : δ), IsLUB (range fun i => f i b) (g b)<VAR>a : α<GOAL>MeasurableSet (⋃ i, {x | a < f i x})
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_1} C<VAR>inst✝³ : Category.{u_7, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E✝ : Type u_3<VAR>inst✝² : Category.{?u.62184, u_3} E✝<VAR>E : Type u_4<VAR>inst✝¹ : Category.{u_5, u_4} E<VAR>L' : C ⥤ E<VAR>eq : D ≌ E<VAR>inst✝ : L.IsLocalization W<VAR>e : L ⋙ eq.functor ≅ L'<GOAL>L'.IsLocalization W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_1} C<VAR>inst✝³ : Category.{u_7, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E✝ : Type u_3<VAR>inst✝² : Category.{?u.62184, u_3} E✝<VAR>E : Type u_4<VAR>inst✝¹ : Category.{u_5, u_4} E<VAR>L' : C ⥤ E<VAR>eq : D ≌ E<VAR>inst✝ : L.IsLocalization W<VAR>e : L ⋙ eq.functor ≅ L'<VAR>h : W.IsInvertedBy L'<GOAL>L'.IsLocalization W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_1} C<VAR>inst✝³ : Category.{u_7, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E✝ : Type u_3<VAR>inst✝² : Category.{?u.62184, u_3} E✝<VAR>E : Type u_4<VAR>inst✝¹ : Category.{u_5, u_4} E<VAR>L' : C ⥤ E<VAR>eq : D ≌ E<VAR>inst✝ : L.IsLocalization W<VAR>e : L ⋙ eq.functor ≅ L'<VAR>h : W.IsInvertedBy L'<VAR>F₁ : W.Localization ⥤ D := Construction.lift L ⋯<GOAL>L'.IsLocalization W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_1} C<VAR>inst✝³ : Category.{u_7, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E✝ : Type u_3<VAR>inst✝² : Category.{?u.62184, u_3} E✝<VAR>E : Type u_4<VAR>inst✝¹ : Category.{u_5, u_4} E<VAR>L' : C ⥤ E<VAR>eq : D ≌ E<VAR>inst✝ : L.IsLocalization W<VAR>e : L ⋙ eq.functor ≅ L'<VAR>h : W.IsInvertedBy L'<VAR>F₁ : W.Localization ⥤ D := Construction.lift L ⋯<VAR>F₂ : W.Localization ⥤ E := Construction.lift L' h<VAR>e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' (F₁ ⋙ eq.functor) F₂ e<GOAL>L'.IsLocalization W
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>x✝ : Cᵒᵖ<GOAL>(α.hom.app (unop x✝)).op ≫ (α.inv.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>x✝ : Cᵒᵖ<GOAL>(α.inv.app (unop x✝) ≫ α.hom.app (unop x✝)).op = 𝟙 (op (G.obj (unop x✝)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>x✝ : Cᵒᵖ<GOAL>(𝟙 (G.obj (unop x✝))).op = 𝟙 (op (G.obj (unop x✝)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>x✝ : Cᵒᵖ<GOAL>(α.inv.app (unop x✝)).op ≫ (α.hom.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>x✝ : Cᵒᵖ<GOAL>(α.hom.app (unop x✝) ≫ α.inv.app (unop x✝)).op = 𝟙 (op (F.obj (unop x✝)))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>x✝ : Cᵒᵖ<GOAL>(𝟙 (F.obj (unop x✝))).op = 𝟙 (op (F.obj (unop x✝)))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<GOAL>trivial G ⊆ Group.closure ∅
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<VAR>h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<VAR>h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp : 0 ≤ p<VAR>hp1 : p ≤ 1<VAR>hp_pos : 0 < p<VAR>h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹<GOAL>(a + b) ^ p ≤ a ^ p + b ^ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommGroup α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝¹ : T2Space α<VAR>inst✝ : DecidableEq β<VAR>hf : Multipliable f<VAR>b : β<GOAL>∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommGroup α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝¹ : T2Space α<VAR>inst✝ : DecidableEq β<VAR>hf : Multipliable f<VAR>b : β<GOAL>∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁸ : Category.{?u.62618, u_1} C<VAR>inst✝⁷ : Category.{?u.62622, u_2} D<VAR>inst✝⁶ : Category.{?u.62626, u_3} E<VAR>inst✝⁵ : Category.{?u.62630, u_4} E'<VAR>A : Type u_5<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : HasShift E' A<VAR>F G✝ H : SingleFunctors C D A<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift A<VAR>a : A<VAR>X : C<GOAL>𝟙 ((shiftFunctor E 0).obj (G.obj ((F.functor a).obj X))) ≫ (G.commShiftIso 0).inv.app ((F.functor a).obj X) ≫ 𝟙 (G.obj ((shiftFunctor D 0).obj ((F.functor a).obj X))) ≫ G.map ((F.shiftIso 0 a a ⋯).hom.app X) = (shiftFunctorZero E A).hom.app (G.obj ((F.functor a).obj X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁸ : Category.{?u.62618, u_1} C<VAR>inst✝⁷ : Category.{?u.62622, u_2} D<VAR>inst✝⁶ : Category.{?u.62626, u_3} E<VAR>inst✝⁵ : Category.{?u.62630, u_4} E'<VAR>A : Type u_5<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : HasShift E' A<VAR>F G✝ H : SingleFunctors C D A<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>𝟙 ((shiftFunctor E (m + n)).obj (G.obj ((F.functor a'').obj X))) ≫ (G.commShiftIso (m + n)).inv.app ((F.functor a'').obj X) ≫ 𝟙 (G.obj ((shiftFunctor D (m + n)).obj ((F.functor a'').obj X))) ≫ G.map ((F.shiftIso (m + n) a a'' ⋯).hom.app X) = (shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫ 𝟙 ((shiftFunctor E n).obj ((shiftFunctor E m).obj (G.obj ((F.functor a'').obj X)))) ≫ (shiftFunctor E n).map (𝟙 ((shiftFunctor E m).obj (G.obj ((F.functor a'').obj X))) ≫ (G.commShiftIso m).inv.app ((F.functor a'').obj X) ≫ 𝟙 (G.obj ((shiftFunctor D m).obj ((F.functor a'').obj X))) ≫ G.map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫ 𝟙 ((shiftFunctor E n).obj (G.obj ((F.functor a').obj X))) ≫ (G.commShiftIso n).inv.app ((F.functor a').obj X) ≫ 𝟙 (G.obj ((shiftFunctor D n).obj ((F.functor a').obj X))) ≫ G.map ((F.shiftIso n a a' ha').hom.app X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁸ : Category.{?u.62618, u_1} C<VAR>inst✝⁷ : Category.{?u.62622, u_2} D<VAR>inst✝⁶ : Category.{?u.62626, u_3} E<VAR>inst✝⁵ : Category.{?u.62630, u_4} E'<VAR>A : Type u_5<VAR>inst✝⁴ : AddMonoid A<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : HasShift E' A<VAR>F G✝ H : SingleFunctors C D A<VAR>G : D ⥤ E<VAR>inst✝ : G.CommShift A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫ (shiftFunctor E n).map ((G.commShiftIso m).inv.app ((F.functor a'').obj X)) ≫ (G.commShiftIso n).inv.app ((shiftFunctor D m).obj ((F.functor a'').obj X)) ≫ G.map ((shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)) ≫ G.map ((shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X)) ≫ G.map ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫ G.map ((F.shiftIso n a a' ha').hom.app X) = (shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫ (shiftFunctor E n).map ((G.commShiftIso m).inv.app ((F.functor a'').obj X)) ≫ (G.commShiftIso n).inv.app ((shiftFunctor D m).obj ((F.functor a'').obj X)) ≫ G.map ((shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫ G.map ((F.shiftIso n a a' ha').hom.app X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Semigroup α<VAR>x y z : α<GOAL>((fun x_1 => x_1 * x) ∘ fun x => x * y) z = z * (y * x)
<VAR>α : Type u_1<VAR>a✝ : PosNum<GOAL>-(neg a✝).succ = (-neg a✝).pred
<VAR>α : Type u_1<VAR>a✝ : PosNum<GOAL>a✝.pred'.toZNum = (-neg a✝).pred
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>inst✝¹ : Inhabited α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>l : List α<VAR>h : Sorted (fun x x_1 => x < x_1) l<VAR>ha : a ∈ l<GOAL>l.head! ≤ a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a✝ : α<VAR>l✝ : List α<VAR>inst✝¹ : Inhabited α<VAR>inst✝ : Preorder α<VAR>a : α<VAR>l : List α<VAR>h : Sorted (fun x x_1 => x < x_1) (l.head! :: l.tail)<VAR>ha : a ∈ l.head! :: l.tail<GOAL>l.head! ≤ a
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type w<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M : Matrix n n R<GOAL>f M.det = (f.mapMatrix M).det
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>y : ℕ<GOAL>2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ yz a1 0 * (↑a - ↑y) + ↑(y ^ 0) - xz a1 0
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>y : ℕ<GOAL>2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ yz a1 1 * (↑a - ↑y) + ↑(y ^ 1) - xz a1 1
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>y n : ℕ<GOAL>2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ yz a1 (n + 2) * (↑a - ↑y) + ↑(y ^ (n + 2)) - xz a1 (n + 2)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>y n : ℕ<VAR>this : 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n)<GOAL>2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ yz a1 (n + 2) * (↑a - ↑y) + ↑(y ^ (n + 2)) - xz a1 (n + 2)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>y n : ℕ<VAR>this : 2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n)<GOAL>2 * ↑a * ↑y - ↑y * ↑y - 1 ∣ ↑(y ^ (n + 2)) - ↑(2 * a) * ↑(y ^ (n + 1)) + ↑(y ^ n) + ↑(2 * a) * (yz a1 (n + 1) * (↑a - ↑y) + ↑(y ^ (n + 1)) - xz a1 (n + 1)) - (yz a1 n * (↑a - ↑y) + ↑(y ^ n) - xz a1 n)
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderBot α<VAR>a b c d : α<GOAL>Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>a✝ : Nontrivial R<GOAL>p %ₘ (X - C a) = C (eval a p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>a✝ : Nontrivial R<VAR>h : eval a (p %ₘ (X - C a)) = eval a p<GOAL>p %ₘ (X - C a) = C (eval a p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>a✝ : Nontrivial R<VAR>h : eval a (p %ₘ (X - C a)) = eval a p<VAR>this : (p %ₘ (X - C a)).degree < 1<GOAL>p %ₘ (X - C a) = C (eval a p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>a✝ : Nontrivial R<VAR>h : eval a (p %ₘ (X - C a)) = eval a p<VAR>this✝ : (p %ₘ (X - C a)).degree < 1<VAR>this : (p %ₘ (X - C a)).degree ≤ 0<GOAL>p %ₘ (X - C a) = C (eval a p)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝¹ b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>a✝ : Nontrivial R<VAR>h : (p %ₘ (X - C a)).coeff 0 = eval a p<VAR>this✝ : (p %ₘ (X - C a)).degree < 1<VAR>this : (p %ₘ (X - C a)).degree ≤ 0<GOAL>p %ₘ (X - C a) = C (eval a p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a - c ≤ a - b + (b - c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a ≤ c + (b - c) + (a - b)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<GOAL>∀ (x y : A), (↑{ toFun := fun a => a ᵍ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯ }).toFun (x + y) = (↑{ toFun := fun a => a ᵍ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯ }).toFun x + (↑{ toFun := fun a => a ᵍ⊗ₜ[R] 1, map_one' := ⋯, map_mul' := ⋯ }).toFun y
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>a₁ a₂ : A<GOAL>(a₁ * a₂) ᵍ⊗ₜ[R] 1 = a₁ ᵍ⊗ₜ[R] 1 * a₂ ᵍ⊗ₜ[R] 1
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.99905, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ✝ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>A : C<VAR>k : L.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : L.d j i ≫ k = 0<VAR>φ : K ⟶ L<GOAL>K.d j i ≫ φ.f i ≫ k = 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ✝ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>A : C<VAR>k : L.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>hk : L.d j i ≫ k = 0<VAR>φ : K ⟶ L<GOAL>opcyclesMap φ i ≫ L.descOpcycles k j hj hk = K.descOpcycles (φ.f i ≫ k) j hj ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<GOAL>(Computation.pure none).bind (aux n) = Computation.pure none
<VAR>x y : ℕ∞<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>h₀ : 0 ∈ s<GOAL>Absorbs 𝕜 s t ↔ ∀ᶠ (c : 𝕜) in 𝓝 0, MapsTo (fun x => c • x) t s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x : E<VAR>a b : 𝕜<VAR>h₀ : 0 ∈ s<GOAL>MapsTo (fun x => 0 • x) t s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>x✝ : E<VAR>a b : 𝕜<VAR>h₀ : 0 ∈ s<VAR>x : E<VAR>a✝ : x ∈ t<GOAL>(fun x => 0 • x) x ∈ s
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hf : Adapted ℱ f<VAR>hab : a < b<GOAL>Measurable (upcrossingsBefore a b f N)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hf : Adapted ℱ f<VAR>hab : a < b<VAR>this : upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i<GOAL>Measurable (upcrossingsBefore a b f N)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>hf : Adapted ℱ f<VAR>hab : a < b<VAR>this : upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i<GOAL>Measurable fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addRightEmbedding c) (Ico a b) = Ico (a + c) (b + c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addRightEmbedding c) '' Set.Ico a b = Set.Ico (a + c) (b + c)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>s ⊆ interior s ↔ IsOpen s
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>v : M<VAR>h : P.pairing i j = 0 ∧ P.pairing j i = 0<GOAL>(P.reflection i * P.reflection j) v = (P.reflection j * P.reflection i) v
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>v : M<VAR>h : P.pairing i j = 0 ∧ P.pairing j i = 0<GOAL>↑(P.reflection i) (↑(P.reflection j) v) = ↑(P.reflection j) (↑(P.reflection i) v)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>v : M<VAR>h : P.pairing i j = 0 ∧ P.pairing j i = 0<GOAL>v - (P.toLin v) (P.coroot i) • P.root i - (P.toLin v) (P.coroot j) • P.root j = v - (P.toLin v) (P.coroot j) • P.root j - (P.toLin v) (P.coroot i) • P.root i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype ↑s<GOAL>s.einfsep = s.offDiag.toFinset.inf (uncurry edist)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype ↑s<VAR>x✝ : ℝ≥0∞<GOAL>x✝ ≤ s.einfsep ↔ x✝ ≤ s.offDiag.toFinset.inf (uncurry edist)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun x => ↑(Real.sin (2 * π * a * ↑x))) s (sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>LSeries.term (fun x => ↑(Real.sin (2 * π * a * ↑x))) s n = ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeries.term (fun x => ↑(Real.sin (2 * π * a * ↑x))) s 0 = ↑(Real.sin (2 * π * a * ↑0)) / ↑0 ^ s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LSeries.term (fun x => ↑(Real.sin (2 * π * a * ↑x))) s n = ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<GOAL>((resolution k G).d (n + 1) n).hom = d k G (n + 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<GOAL>(((resolution k G).d (n + 1) n).hom ∘ₗ Finsupp.lsingle x) 1 = (d k G (n + 1) ∘ₗ Finsupp.lsingle x) 1
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<GOAL>(((alternatingFaceMapComplex (Rep k G)).obj (classifyingSpaceUniversalCover G ⋙ (Rep.linearization k G).toFunctor)).d (n + 1) n).hom (Finsupp.single x 1) = (d k G (n + 1)) (Finsupp.single x 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<GOAL>(∑ x : Fin (n + 2), (-1) ^ ↑x • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x).op).hom) (Finsupp.single x 1) = (d k G (n + 1)) (Finsupp.single x 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<GOAL>∑ c : Fin (n + 2), ((-1) ^ ↑c • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom) (Finsupp.single x 1) = (d k G (n + 1)) (Finsupp.single x 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<GOAL>∑ c : Fin (n + 2), ((-1) ^ ↑c • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ c).op).hom) (Finsupp.single x 1) = ∑ p : Fin ((Opposite.unop (Opposite.op (SimplexCategory.mk (n + 1)))).len + 1), Finsupp.single (x ∘ p.succAbove) ((-1) ^ ↑p)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<VAR>x✝¹ : Fin (n + 2)<VAR>x✝ : x✝¹ ∈ Finset.univ<GOAL>((-1) ^ ↑x✝¹ • Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom) (Finsupp.single x 1) = Finsupp.single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<VAR>x✝¹ : Fin (n + 2)<VAR>x✝ : x✝¹ ∈ Finset.univ<GOAL>(-1) ^ ↑x✝¹ • (Finsupp.lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom) (Finsupp.single x 1) = Finsupp.single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n✝ : ℕ<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V<VAR>x✝¹ : Fin (n + 2)<VAR>x✝ : x✝¹ ∈ Finset.univ<GOAL>Finsupp.single (((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom x) ((-1) ^ ↑x✝¹) = Finsupp.single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>init : α<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>Substring.foldr f init x✝ = List.foldr f init x✝.toString.data