ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)<GOAL>StrictConcaveOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)<GOAL>StrictConvexOn 𝕜 s (-f)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)<VAR>x✝ y✝ z✝ : 𝕜<VAR>hx : x✝ ∈ s<VAR>hz : z✝ ∈ s<VAR>hxy : x✝ < y✝<VAR>hyz : y✝ < z✝<GOAL>((-f) y✝ - (-f) x✝) / (y✝ - x✝) < ((-f) z✝ - (-f) y✝) / (z✝ - y✝)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)<VAR>x✝ y✝ z✝ : 𝕜<VAR>hx : x✝ ∈ s<VAR>hz : z✝ ∈ s<VAR>hxy : x✝ < y✝<VAR>hyz : y✝ < z✝<GOAL>-(((-f) z✝ - (-f) y✝) / (z✝ - y✝)) < -(((-f) y✝ - (-f) x✝) / (y✝ - x✝))
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)<VAR>x✝ y✝ z✝ : 𝕜<VAR>hx : x✝ ∈ s<VAR>hz : z✝ ∈ s<VAR>hxy : x✝ < y✝<VAR>hyz : y✝ < z✝<GOAL>(f z✝ - f y✝) / (z✝ - y✝) < (f y✝ - f x✝) / (y✝ - x✝)
<GOAL>SurjOn cos (Icc 0 π) (Icc (-1) 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β → F<VAR>hf : ∀ (i : α), Continuous (f i)<VAR>hu : Summable u<VAR>hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n<GOAL>Continuous fun x => ∑' (n : α), f n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β → F<VAR>hu : Summable u<VAR>hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n<VAR>hf : ∀ (i : α), ContinuousOn (f i) univ<GOAL>ContinuousOn (fun x => ∑' (n : α), f n x) univ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>h : a ≤ b<GOAL>b⁻¹ ≤ a⁻¹
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.55818, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝³ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<VAR>inst✝ : ReflectsFiniteLimits s<VAR>hF : IsSheaf (coherentTopology C) (F ⋙ s)<GOAL>IsSheaf (coherentTopology C) F
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.55818, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝³ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<VAR>inst✝ : ReflectsFiniteLimits s<VAR>hF : Nonempty (PreservesFiniteProducts (F ⋙ s)) ∧ EqualizerCondition (F ⋙ s)<GOAL>Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<GOAL>(M.map f hf).Basis (f '' I) (f '' X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<GOAL>∀ e ∈ f '' X \ f '' I, (M.map f hf).Dep (insert e (f '' I))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<GOAL>(M.map f hf).Dep (insert (f e) (f '' I))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<VAR>hss : insert e I ⊆ M.E<GOAL>(M.map f hf).Dep (insert (f e) (f '' I))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<VAR>hss : insert e I ⊆ M.E<GOAL>¬(M.map f hf).Indep (insert (f e) (f '' I))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<VAR>hss : insert e I ⊆ M.E<GOAL>∀ (x : Set α), M.Indep x → ¬insert (f e) (f '' I) = f '' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<VAR>hss : insert e I ⊆ M.E<VAR>J : Set α<VAR>hJ : M.Indep J<VAR>hins : insert (f e) (f '' I) = f '' J<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<VAR>hss : insert e I ⊆ M.E<VAR>J : Set α<VAR>hJ : M.Indep J<VAR>hins : insert e I = J<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>X : Set α<VAR>hIX : M.Basis I X<VAR>f : α → β<VAR>hf : InjOn f M.E<VAR>e : α<VAR>he : e ∈ X<VAR>he' : f e ∉ f '' I<VAR>hss : insert e I ⊆ M.E<VAR>hJ : M.Indep (insert e I)<GOAL>False
<VAR>α : Sort u_1<VAR>a : α<VAR>motive : (a' : α) → a = a' → Sort u_2<VAR>x : motive a ⋯<VAR>β : Sort u_2<VAR>y : β<GOAL>HEq y (⋯ ▸ x) ↔ HEq y x
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J✝ : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<VAR>hI : I.IsPrimary<VAR>J : Ideal R<GOAL>J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {I.radical}
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J✝ : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<VAR>hI : I.IsPrimary<VAR>J : Ideal R<GOAL>J ∈ associatedPrimes R (R ⧸ I) ↔ J = I.radical
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J✝ : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<VAR>hI : I.IsPrimary<VAR>J : Ideal R<GOAL>J = I.radical → J ∈ associatedPrimes R (R ⧸ I)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<VAR>hI : I.IsPrimary<GOAL>I.radical ∈ associatedPrimes R (R ⧸ I)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<VAR>hI : I.IsPrimary<VAR>this : Nontrivial (R ⧸ I)<GOAL>I.radical ∈ associatedPrimes R (R ⧸ I)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<VAR>hI : I.IsPrimary<VAR>this : Nontrivial (R ⧸ I)<VAR>a : Ideal R<VAR>ha : a ∈ associatedPrimes R (R ⧸ I)<GOAL>I.radical ∈ associatedPrimes R (R ⧸ I)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b : α<GOAL>|a - b| ≤ |a| + |b|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b : α<GOAL>|a + -b| ≤ |a| + |(-b)|
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<GOAL>atTop ×ˢ atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>h✝ : IsEmpty α<GOAL>atTop ×ˢ atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>h✝ : Nonempty α<GOAL>atTop ×ˢ atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>h✝¹ : Nonempty α<VAR>h✝ : IsEmpty β<GOAL>atTop ×ˢ atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>h✝¹ : Nonempty α<VAR>h✝ : Nonempty β<GOAL>atTop ×ˢ atTop = atTop
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.natTrailingDegree = 0 ↔ p = 0 ∨ p.coeff 0 ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>(partialSups f) n = ⨆ i, ⨆ (_ : i ≤ n), f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>a : α<VAR>h : range f ∈ 𝓝 (f a)<GOAL>map f (𝓝 a) = 𝓝 (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : FloorRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>n : ℤ<GOAL>Tendsto floor (𝓝[<] ↑n) (pure (n - 1))
<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>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<GOAL>Subalgebra.toSubmodule (integralClosure A L) ≤ Submodule.span A (Set.range ⇑((traceForm K L).dualBasis ⋯ b))
<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>inst✝¹⁶ : IsDomain A<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : IsFractionRing A K<VAR>L : Type u_4<VAR>inst✝¹³ : Field L<VAR>C : Type u_5<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : Algebra C L<VAR>inst✝⁷ : IsIntegralClosure C A L<VAR>inst✝⁶ : Algebra A C<VAR>inst✝⁵ : IsScalarTower A C L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>inst✝ : IsIntegrallyClosed A<GOAL>Subalgebra.toSubmodule (integralClosure A L) ≤ LinearMap.range (↑A (Algebra.linearMap (↥(integralClosure A L)) L))
<VAR>R S : Type u<VAR>M✝ : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η✝ : Type u₁'<VAR>φ : η✝ → Type u_1<VAR>inst✝¹⁷ : Ring R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : AddCommGroup M✝<VAR>inst✝¹⁴ : AddCommGroup M'<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R M✝<VAR>inst✝¹¹ : Module R M'<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : Module.Free R M✝<VAR>inst✝⁷ : (i : η✝) → AddCommGroup (φ i)<VAR>inst✝⁶ : (i : η✝) → Module R (φ i)<VAR>inst✝⁵ : ∀ (i : η✝), Module.Free R (φ i)<VAR>inst✝⁴ : Fintype η✝<VAR>M η : Type u<VAR>inst✝³ : Fintype η<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module.Free R M<GOAL>Module.rank R (η → M) = ↑(Fintype.card η) * Module.rank R M
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Infinite α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Nontrivial β<GOAL>#(α →₀ β) = max (lift.{v, u} #α) (lift.{u, v} #β)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Infinite α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Nontrivial β<GOAL>#(α →₀ β) ≤ max (lift.{v, u} #α) (lift.{u, v} #β)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Infinite α<VAR>inst✝¹ : Zero β<VAR>inst✝ : Nontrivial β<GOAL>max (lift.{v, u} #α) (lift.{u, v} #β) ≤ #(α →₀ β)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>m : MeasurableSpace α<VAR>T : Set α → F →L[ℝ] F'<GOAL>setToSimpleFunc T 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>n : ℕ<VAR>f : List α → β<VAR>r : List β<GOAL>sublistsLenAux n l f r = map f (sublistsLen n l) ++ r
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<VAR>n : ℕ<VAR>f : List α → β<VAR>r : List β<GOAL>sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x✝ : ℕ<GOAL>4 * 0 * x✝ ≤ (0 + x✝) * (0 + x✝)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x✝ : ℕ<GOAL>0 ≤ (0 + x✝) * (0 + x✝)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x✝ : ℕ<GOAL>4 * x✝ * 0 ≤ (x✝ + 0) * (x✝ + 0)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>x✝ : ℕ<GOAL>0 ≤ (x✝ + 0) * (x✝ + 0)
<VAR>a✝ b✝ c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a b : ℕ<GOAL>4 * (a + 1) * (b + 1) ≤ (a + 1 + (b + 1)) * (a + 1 + (b + 1))
<VAR>A : Type u_1<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ antidiagonal n<GOAL>kl.2 ≤ n
<VAR>A : Type u_1<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ antidiagonal n<GOAL>∃ c, n = kl.2 + c
<VAR>A : Type u_1<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>kl : A × A<VAR>hlk : kl ∈ antidiagonal n<GOAL>n = kl.2 + kl.1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f : X → Y → E<VAR>s : Set X<VAR>k : Set Y<VAR>inst✝ : IsFiniteMeasureOnCompacts μ<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<GOAL>ContinuousOn (fun x => ∫ (y : Y), f x y ∂μ) s
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<GOAL>0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<GOAL>¬(¬(0 ≤ a ∧ 0 ≤ b) ∧ ¬(a ≤ 0 ∧ b ≤ 0))
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<GOAL>(0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<GOAL>False
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<GOAL>a * b < 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<VAR>ha : 0 < a<GOAL>a * b < 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ 0 * b<VAR>ab : 0 ≤ 0 → b < 0<VAR>nab : 0 ≤ 0 → 0 < b<GOAL>0 * b < 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : LinearOrder α<VAR>a b c d : α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : PosMulStrictMono α<VAR>hab : 0 ≤ a * b<VAR>ab : 0 ≤ a → b < 0<VAR>nab : a ≤ 0 → 0 < b<VAR>ha : a < 0<GOAL>a * b < 0
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>M✝ : ModuleCat R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↥(LinearMap.ker f)<GOAL>(⇑(kernelSubobject f).arrow ∘ ⇑(kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = ↑x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>M✝ : ModuleCat R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↥(LinearMap.ker f)<GOAL>((kernelIsoKer f).inv ≫ (kernelSubobjectIso f).inv ≫ (kernelSubobject f).arrow) x = ↑x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>M✝ : ModuleCat R<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>x : ↥(LinearMap.ker f)<GOAL>(LinearMap.ker f).subtype x = ↑x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>0 < count a l ↔ a ∈ l
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x✝ x : E<GOAL>gauge (closure 0) x = 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x✝ x : E<GOAL>sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x✝ x : E<VAR>hx : ‖x‖ = 0<GOAL>sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x✝ x : E<VAR>hx : 0 < ‖x‖<GOAL>sInf {r | r ∈ Ioi 0 ∧ (r = 0 ∨ ‖x‖ = 0)} = 0 x
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Monoid G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulAction G M<VAR>f : G × G → M<VAR>hf : IsMulTwoCocycle f<VAR>g : G<GOAL>f (g, 1) = g • f (1, 1)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>0 < minkowskiBound K I
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>2 ^ finrank ℝ (({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)) ≠ 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>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>hV : IsHilbertSum 𝕜 G V<VAR>w : ↥(lp G 2)<GOAL>hV.linearIsometryEquiv.symm w = ∑' (i : ι), (V i) (↑w i)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<GOAL>count K v (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<GOAL>count K v 1 = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<GOAL>∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>exps : HeightOneSpectrum R → ℤ<GOAL>∀ x ∈ fun i => i = v → False, count K v (↑x.asIdeal ^ exps x) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x val✝ : α<VAR>property✝ : val✝ ∈ Ici a<GOAL>projIci a ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a (b - p) = toIocMod hp a b
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>c * b < a * b⁻¹ * b ↔ c * b < a
<VAR>o : Ordinal.{u_1}<GOAL>Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
<GOAL>Principal (fun x x_1 => x + x_1) 0 ↔ 0 = 0 ∨ ∃ a, 0 = ω ^ a
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>Principal (fun x x_1 => x + x_1) o ↔ o = 0 ∨ ∃ a, o = ω ^ a
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>f : Ω →ᵇ ℝ≥0<VAR>h_mass : ¬μ.mass = 0<GOAL>Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>f : Ω →ᵇ ℝ≥0<VAR>h_mass : ¬μ.mass = 0<GOAL>Tendsto (fun i => (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : Tendsto (ProbabilityMeasure.toFiniteMeasure ∘ fun i => (μs i).normalize) F (𝓝 μ.normalize.toFiniteMeasure)<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>f : Ω →ᵇ ℝ≥0<VAR>h_mass : ¬μ.mass = 0<GOAL>Tendsto (fun i => (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => (μs i).normalize) i).testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>f : Ω →ᵇ ℝ≥0<VAR>h_mass : ¬μ.mass = 0<GOAL>Tendsto (fun i => (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))