ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>y : ℝ*<VAR>r s : ℝ<VAR>hys : y.IsSt s<VAR>hrs : r < s<VAR>f : ℕ → ℝ<VAR>hxr : (ofSeq f).IsSt r<GOAL>ofSeq f < y
<VAR>r s : ℝ<VAR>hrs : r < s<VAR>f : ℕ → ℝ<VAR>hxr : (ofSeq f).IsSt r<VAR>g : ℕ → ℝ<VAR>hys : (ofSeq g).IsSt s<GOAL>ofSeq f < ofSeq g
<VAR>r s : ℝ<VAR>hrs : r < s<VAR>f : ℕ → ℝ<VAR>hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)<VAR>g : ℕ → ℝ<VAR>hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)<GOAL>ofSeq f < ofSeq g
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w u' : V<VAR>p : G.Walk u' u'<GOAL>(p.copy ⋯ ⋯).IsCycle ↔ p.IsCycle
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : Nontrivial R<VAR>G : Type u_3<VAR>inst✝ : AddCommGroup G<VAR>x : G<GOAL>x ∈ (torsion ℤ G).toAddSubgroup ↔ x ∈ AddCommGroup.torsion G
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : Nontrivial R<VAR>G : Type u_3<VAR>inst✝ : AddCommGroup G<VAR>x : G<GOAL>(∃ n, n ≠ 0 ∧ n • x = 0) ↔ x ∈ (torsion ℤ G).toAddSubgroup
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>f : (i : I) → Y i ⟶ X<VAR>W : C<VAR>g : W ⟶ X<VAR>hg : (ofArrows Y f).arrows g<GOAL>(ofObjects Y X).arrows g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z : C<VAR>f✝ : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>I : Type u_1<VAR>Y : I → C<VAR>X : C<VAR>f : (i : I) → Y i ⟶ X<VAR>W : C<VAR>g : W ⟶ X<VAR>hg : ∃ i a, g = a ≫ f i<GOAL>(ofObjects Y X).arrows g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<GOAL>‖((splitMul 𝕜 E) x).2‖ ^ 2 ≤ ‖((splitMul 𝕜 E) (x⋆ * x)).2‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<GOAL>‖((splitMul 𝕜 E) x).2‖ ≤ √‖((splitMul 𝕜 E) (x⋆ * x)).2‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<GOAL>‖(algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd‖ ≤ √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<GOAL>sSup ((fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) x_1‖) '' Metric.closedBall 0 1) ≤ √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<GOAL>∀ b ∈ (fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) x_1‖) '' Metric.closedBall 0 1, b ≤ √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<VAR>b : E<VAR>hb : b ∈ Metric.closedBall 0 1<GOAL>‖((algebraMap 𝕜 (E →L[𝕜] E)) x.fst + (mul 𝕜 E) x.snd) b‖ ≤ √‖(algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<VAR>b : E<VAR>hb : b ∈ Metric.closedBall 0 1<GOAL>‖b⋆ * (x.fst⋆ • (x.fst • b + x.snd * b) + x.snd⋆ * (x.fst • b + x.snd * b))‖ ≤ sSup ((fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) x_1‖) '' Metric.closedBall 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<VAR>b : E<VAR>hb : b ∈ Metric.closedBall 0 1<GOAL>‖b⋆‖ * ‖x.fst⋆ • (x.fst • b + x.snd * b) + x.snd⋆ * (x.fst • b + x.snd * b)‖ ≤ sSup ((fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) x_1‖) '' Metric.closedBall 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<VAR>b : E<VAR>hb : b ∈ Metric.closedBall 0 1<GOAL>BddAbove ((fun x_1 => ‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) x_1‖) '' Metric.closedBall 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁹ : DenselyNormedField 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing E<VAR>inst✝⁷ : StarRing E<VAR>inst✝⁶ : CstarRing E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : IsScalarTower 𝕜 E E<VAR>inst✝³ : SMulCommClass 𝕜 E E<VAR>inst✝² : StarRing 𝕜<VAR>inst✝¹ : CstarRing 𝕜<VAR>inst✝ : StarModule 𝕜 E<VAR>x : Unitization 𝕜 E<VAR>b : E<VAR>hb : b ∈ Metric.closedBall 0 1<GOAL>‖((algebraMap 𝕜 (E →L[𝕜] E)) (x⋆ * x).fst + (mul 𝕜 E) (x⋆ * x).snd) b‖ = ‖x.fst⋆ • (x.fst • b + x.snd * b) + x.snd⋆ * (x.fst • b + x.snd * b)‖
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x + Int.negSucc n • a) = f x + Int.negSucc n • b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommGroup G<VAR>x : G<VAR>xs : List G<GOAL>(x :: xs).prod⁻¹ = (map (fun x => x⁻¹) (x :: xs)).prod
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>U : Set X := f ⁻¹' {f y}<GOAL>f x = f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>U : Set X := f ⁻¹' {f y}<GOAL>x ∉ Uᶜ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<GOAL>Function.Injective ⇑(splitMul 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<GOAL>∀ (a : Unitization 𝕜 A), (splitMul 𝕜 A) a = 0 → a = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<VAR>r✝ : 𝕜<VAR>a✝ : A<VAR>hx : (splitMul 𝕜 A) (inl r✝ + ↑a✝) = 0<GOAL>inl r✝ + ↑a✝ = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<VAR>r✝ : 𝕜<VAR>a✝ : A<VAR>hx : (splitMul 𝕜 A) (inl r✝) + (splitMul 𝕜 A) ↑a✝ = 0<GOAL>inl r✝ + ↑a✝ = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<VAR>r✝ : 𝕜<VAR>a✝ : A<VAR>hx : r✝ = 0 ∧ (algebraMap 𝕜 (A →L[𝕜] A)) r✝ + (mul 𝕜 A) a✝ = 0<GOAL>inl r✝ + ↑a✝ = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<VAR>a✝ : A<VAR>hx : (algebraMap 𝕜 (A →L[𝕜] A)) 0 + (mul 𝕜 A) a✝ = 0<GOAL>inl 0 + ↑a✝ = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<VAR>a✝ : A<VAR>hx : (mul 𝕜 A) a✝ = 0<GOAL>↑a✝ = 0
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>h : Function.Injective ⇑(mul 𝕜 A)<VAR>a✝ : A<VAR>hx : (mul 𝕜 A) a✝ = (mul 𝕜 A) 0<GOAL>↑a✝ = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty<GOAL>StrictConvex 𝕜 s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty<VAR>x : E<VAR>hx : x ∈ s \ interior s<VAR>y : E<VAR>hy : y ∈ s \ interior s<VAR>x✝ : x ≠ y<GOAL>fun ⦃a b⦄ => ([a-[𝕜]b] \ frontier s).Nonempty → ∃ c, (lineMap a b) c ∈ interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty<VAR>x : E<VAR>hx : x ∈ s \ interior s<VAR>y : E<VAR>hy : y ∈ s \ interior s<VAR>x✝ : x ≠ y<GOAL>(⇑(lineMap x y) '' Icc 0 1 \ frontier s).Nonempty → ∃ c, (lineMap x y) c ∈ s \ frontier s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty<VAR>x : E<VAR>hx : x ∈ s \ interior s<VAR>y : E<VAR>hy : y ∈ s \ interior s<VAR>x✝ : x ≠ y<VAR>c : 𝕜<VAR>hc : c ∈ Icc 0 1<VAR>hcs : (lineMap x y) c ∉ frontier s<GOAL>∃ c, (lineMap x y) c ∈ s \ frontier s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty<VAR>x : E<VAR>hx : x ∈ s \ interior s<VAR>y : E<VAR>hy : y ∈ s \ interior s<VAR>x✝ : x ≠ y<VAR>c : 𝕜<VAR>hc : c ∈ Icc 0 1<VAR>hcs : (lineMap x y) c ∉ frontier s<GOAL>(lineMap x y) c ∈ [x-[𝕜]y]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>g ≤ f ⊔ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>↑g ≤ᶠ[ae μ] ↑(f ⊔ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<VAR>a✝ : α<VAR>ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝<GOAL>↑g a✝ ≤ ↑(f ⊔ g) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<VAR>a✝ : α<VAR>ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝<GOAL>↑g a✝ ≤ ↑f a✝ ⊔ ↑g a✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y X₁ Y₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>f : X ⟶ Y<GOAL>α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y X₁ Y₁ : C<VAR>α : X ≅ X₁<VAR>β : Y ≅ Y₁<VAR>f : X₁ ⟶ Y₁<GOAL>α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>inst✝ : Reflective i<VAR>A B B' : C<VAR>h : B ⟶ B'<VAR>hB : B ∈ i.essImage<VAR>hB' : B' ∈ i.essImage<VAR>f : A ⟶ B<GOAL>(unitCompPartialBijective A hB') (f ≫ h) = (unitCompPartialBijective A hB) f ≫ h
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>f : F<GOAL>↑(map f ⊥) = ↑⊥
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>h : (g.comp f).FiniteType<VAR>x✝⁴ : Algebra A B := f.toAlgebra<VAR>x✝³ : Algebra B C := g.toAlgebra<VAR>x✝² : Algebra A C := (g.comp f).toAlgebra<VAR>x✝¹ : IsScalarTower A B C := RestrictScalars.isScalarTower A B C<VAR>x✝ : Algebra.FiniteType A C := h<GOAL>g.FiniteType
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddCommMonoid M<VAR>v v₁✝ v₂✝ : α →₀ M<VAR>f : α → β<VAR>hf : Injective f<VAR>v₁ v₂ : α →₀ M<VAR>eq : mapDomain f v₁ = mapDomain f v₂<VAR>a : α<VAR>this : (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)<GOAL>v₁ a = v₂ a
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>C : Type v<VAR>inst✝ : CommMonoid C<VAR>n : ℕ<VAR>ψ : AddChar (ZMod n) C<VAR>hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0<VAR>a : ZMod n<VAR>ha : a ≠ 0<VAR>hf : ψ.mulShift a = 1<VAR>h : (ψ.mulShift a) 1 = 1 1<GOAL>False
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>R' : Type v<VAR>inst✝¹ : CommMonoid R'<VAR>C : Type v<VAR>inst✝ : CommMonoid C<VAR>n : ℕ<VAR>ψ : AddChar (ZMod n) C<VAR>hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0<VAR>a : ZMod n<VAR>ha : a ≠ 0<VAR>hf : ψ.mulShift a = 1<VAR>h : ψ a = 1 1<GOAL>False
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsTriangularizable R L M<VAR>x : L<GOAL>⨆ φ, weightSpaceOf M φ x = ⊤
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsTriangularizable R L M<VAR>x : L<GOAL>⨆ i, ↑(weightSpaceOf M i x) = ⊤
<VAR>σ : Type u_1<VAR>inst✝¹ : Fintype σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>↑k * esymm σ R k = (-1) ^ (k + 1) * ∑ a ∈ filter (fun a => a.1 < k) (antidiagonal k), (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>σ ≫ f = prod.map f f ≫ σ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y<VAR>hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ<GOAL>σ ≫ f = prod.map f f ≫ σ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y<VAR>hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ<GOAL>f = g
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁵ : NormedField 𝕜<VAR>inst✝²⁴ : SeminormedAddCommGroup V<VAR>inst✝²³ : NormedSpace 𝕜 V<VAR>inst✝²² : PseudoMetricSpace P<VAR>inst✝²¹ : NormedAddTorsor V P<VAR>inst✝²⁰ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁹ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁸ : PseudoMetricSpace P₁<VAR>inst✝¹⁷ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁶ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁵ : NormedSpace 𝕜 V₁'<VAR>inst✝¹⁴ : MetricSpace P₁'<VAR>inst✝¹³ : NormedAddTorsor V₁' P₁'<VAR>inst✝¹² : SeminormedAddCommGroup V₂<VAR>inst✝¹¹ : NormedSpace 𝕜 V₂<VAR>inst✝¹⁰ : PseudoMetricSpace P₂<VAR>inst✝⁹ : NormedAddTorsor V₂ P₂<VAR>inst✝⁸ : SeminormedAddCommGroup V₃<VAR>inst✝⁷ : NormedSpace 𝕜 V₃<VAR>inst✝⁶ : PseudoMetricSpace P₃<VAR>inst✝⁵ : NormedAddTorsor V₃ P₃<VAR>inst✝⁴ : SeminormedAddCommGroup V₄<VAR>inst✝³ : NormedSpace 𝕜 V₄<VAR>inst✝² : PseudoMetricSpace P₄<VAR>inst✝¹ : NormedAddTorsor V₄ P₄<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>inst✝ : TopologicalSpace α<VAR>f : P → P₂<VAR>hf : Isometry f<VAR>p : P<VAR>g : V → V₂<VAR>hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p<GOAL>Isometry g
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁵ : NormedField 𝕜<VAR>inst✝²⁴ : SeminormedAddCommGroup V<VAR>inst✝²³ : NormedSpace 𝕜 V<VAR>inst✝²² : PseudoMetricSpace P<VAR>inst✝²¹ : NormedAddTorsor V P<VAR>inst✝²⁰ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁹ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁸ : PseudoMetricSpace P₁<VAR>inst✝¹⁷ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁶ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁵ : NormedSpace 𝕜 V₁'<VAR>inst✝¹⁴ : MetricSpace P₁'<VAR>inst✝¹³ : NormedAddTorsor V₁' P₁'<VAR>inst✝¹² : SeminormedAddCommGroup V₂<VAR>inst✝¹¹ : NormedSpace 𝕜 V₂<VAR>inst✝¹⁰ : PseudoMetricSpace P₂<VAR>inst✝⁹ : NormedAddTorsor V₂ P₂<VAR>inst✝⁸ : SeminormedAddCommGroup V₃<VAR>inst✝⁷ : NormedSpace 𝕜 V₃<VAR>inst✝⁶ : PseudoMetricSpace P₃<VAR>inst✝⁵ : NormedAddTorsor V₃ P₃<VAR>inst✝⁴ : SeminormedAddCommGroup V₄<VAR>inst✝³ : NormedSpace 𝕜 V₄<VAR>inst✝² : PseudoMetricSpace P₄<VAR>inst✝¹ : NormedAddTorsor V₄ P₄<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>inst✝ : TopologicalSpace α<VAR>f : P → P₂<VAR>hf : Isometry f<VAR>p : P<VAR>g : V → V₂<VAR>hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p<GOAL>g = ⇑(vaddConst 𝕜 (f p)).symm ∘ f ∘ ⇑(vaddConst 𝕜 p)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : NormedGroup E<VAR>inst✝ : NormedGroup F<VAR>a b : E<GOAL>‖a‖₊ = 0 ↔ a = 1
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<VAR>n : ℕ<GOAL>List.take 0 (take n s) = take (min n 0) s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<VAR>m : ℕ<GOAL>List.take m (take 0 s) = take (min 0 m) s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<VAR>m n : ℕ<GOAL>List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : ¬M ≤ 0<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<GOAL>∃ δ, ∃ (_ : 0 < δ), ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<GOAL>eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<VAR>hp : ¬p = 0<GOAL>eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hp_top : p ≠ ⊤<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>M : ℝ<VAR>hf : ∀ (x : α), ‖f x‖ < M<VAR>hM : 0 < M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ : μ s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)<VAR>hp : ¬p = 0<GOAL>eLpNorm f p (μ.restrict s) ≤ ENNReal.ofReal ε