ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>c : Cardinal.{u}<VAR>h✝¹ : Cardinal.lift.{max (u + 1) v, u} c < Cardinal.univ.{u, v}<VAR>S : Set Ordinal.{u}<VAR>H : Unbounded (fun x x_1 => x < x_1) S<VAR>Se : #↑S = (type fun x x_1 => x < x_1).cof<VAR>h✝ : Cardinal.lift.{u + 1, u} c ≥ #↑S<VAR>a : Cardinal.{u}<VAR>e✝ : Cardinal.lift.{u + 1, u} a = #↑S<VAR>α : Type u<VAR>e : Cardinal.lift.{u + 1, u} ⟦α⟧ = #↑S<VAR>f✝ : ULift.{u + 1, u} α ≃ ↑S<VAR>f : α ≃ ↑S<VAR>g : α → Ordinal.{u} := fun a => ↑(f a)<VAR>o : Ordinal.{u} := succ (sup g)<VAR>b : Ordinal.{u}<VAR>h : b ∈ S<VAR>l : ¬(fun x x_1 => x < x_1) b o<GOAL>g (f.symm ⟨b, h⟩) ≤ sup g
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>P X Y Z : C<VAR>f : P ⟶ X<VAR>g : P ⟶ Y<VAR>inst✝² : HasBinaryProduct X Y<VAR>inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)<VAR>inst✝ : PreservesLimit (pair X Y) G<GOAL>(iso G X Y).inv ≫ G.map prod.snd = prod.snd
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>P X Y Z : C<VAR>f : P ⟶ X<VAR>g : P ⟶ Y<VAR>inst✝² : HasBinaryProduct X Y<VAR>inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)<VAR>inst✝ : PreservesLimit (pair X Y) G<GOAL>𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>i : σ<VAR>c : R<GOAL>Multiset.count i (C c * p).degrees ≤ Multiset.count i p.degrees
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>i : σ<VAR>c : R<GOAL>p.degrees = (C c).degrees + p.degrees
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>j : R<VAR>inst✝¹ : Invertible j<VAR>inst✝ : Invertible (j - 1728)<GOAL>(ofJ' j).j = j
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>j : R<VAR>inst✝¹ : Invertible j<VAR>inst✝ : Invertible (j - 1728)<GOAL>j * (j ^ 2 * (j - 1728) ^ 9) = (j * (j - 1728) ^ 3) ^ 3
<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.foldl f init x✝ = List.foldl f init x✝.toString.data
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<GOAL>¬cd 0 ^ 2 + (-cd 1) ^ 2 = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<GOAL>¬cd 0 ^ 2 + cd 1 ^ 2 = 0
<VAR>n : ℕ<VAR>a✝ : ℕ × ℕ<GOAL>a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}
<VAR>n : ℕ<GOAL>eulerMascheroniSeq n < eulerMascheroniConstant
<VAR>n : ℕ<GOAL>eulerMascheroniSeq n.succ ≤ eulerMascheroniConstant
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s<GOAL>infDist x (s ∩ closedBall x (dist y x)) = infDist x s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s ∩ closedBall x (dist y x)<GOAL>infDist x (s ∩ closedBall x (dist y x)) = infDist x s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s ∩ closedBall x (dist y x)<GOAL>infDist x (s ∩ closedBall x (dist y x)) ≤ infDist x s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s ∩ closedBall x (dist y x)<VAR>hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s ∩ closedBall x (dist y x)<VAR>hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))<VAR>z : α<VAR>hzs : z ∈ s<VAR>hz : dist x z < infDist x (s ∩ closedBall x (dist y x))<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s ∩ closedBall x (dist y x)<VAR>hlt : infDist x s < infDist x (s ∩ closedBall x (dist y x))<VAR>z : α<VAR>hzs : z ∈ s<VAR>hz : dist x z < infDist x (s ∩ closedBall x (dist y x))<VAR>hle : dist z x ≤ dist y x<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>h : y ∈ s ∩ closedBall x (dist y x)<VAR>hlt✝ : infDist x s < infDist x (s ∩ closedBall x (dist y x))<VAR>z : α<VAR>hzs : z ∈ s<VAR>hz : dist x z < infDist x (s ∩ closedBall x (dist y x))<VAR>hlt : dist y x < dist z x<GOAL>False
<VAR>α : Type u<VAR>lt : α → α → Prop<VAR>inst✝ : DecidableRel lt<VAR>a b : α<GOAL>(cmpUsing lt a b = Ordering.lt) = lt a b
<VAR>n : ℕ<GOAL>n.choose n = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>h : p ≠ 0<GOAL>(swap dslope z₀)^[p.order] f z₀ ≠ 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>h : p ≠ 0<GOAL>(fslope^[p.order] p 0) 1 ≠ 0
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁷ : TopologicalSpace G✝<VAR>inst✝⁶ : Group G✝<VAR>inst✝⁵ : TopologicalGroup G✝<VAR>inst✝⁴ : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>n : G<VAR>hn : n ∈ N.topologicalClosure<VAR>g : G<GOAL>g * n * g⁻¹ ∈ N.topologicalClosure
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁷ : TopologicalSpace G✝<VAR>inst✝⁶ : Group G✝<VAR>inst✝⁵ : TopologicalGroup G✝<VAR>inst✝⁴ : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>n : G<VAR>hn : n ∈ N.topologicalClosure<VAR>g : G<GOAL>MapsTo (fun h => g * h * g⁻¹) ↑N ↑N
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝² : CommMonoid β<VAR>inst✝¹ : DecidableEq α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>l : List α<GOAL>∑ x ∈ filter p l.toFinset, count x l = countP (fun b => decide (p b)) l
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>S : IntermediateField F K := separableClosure F K<GOAL>sepDegree F K = Module.rank E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>S : IntermediateField F K := separableClosure F K<VAR>h : Module.rank E ↥(adjoin E ↑S) ≤ Module.rank F ↥S<GOAL>sepDegree F K = Module.rank E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>S : IntermediateField F K := separableClosure F K<VAR>h : Module.rank E K ≤ Module.rank F ↥S<GOAL>sepDegree F K = Module.rank E K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁸ : Field F<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F E<VAR>K : Type w<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra E K<VAR>inst✝² : IsScalarTower F E K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>inst✝ : Algebra.IsSeparable E K<VAR>S : IntermediateField F K := separableClosure F K<VAR>h : Module.rank E K ≤ Module.rank F ↥S<VAR>ι : Set ↥S<VAR>b : Basis (↑ι) F ↥S<GOAL>sepDegree F K = Module.rank E K
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>m✝ : OuterMeasure α<VAR>β : Type u_3<VAR>ι : Sort u_4<VAR>f : α → β<VAR>m : ι → OuterMeasure β<VAR>s : Set α<GOAL>((comap f) (⨆ i, m i)) s = (⨆ i, (comap f) (m i)) s
<VAR>u₁ u₂ : ℤˣ<GOAL>u₁ / u₂ = u₁ * u₂
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>P✝ : α → Sort w<VAR>e✝ : α ≃ β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>g : (b : β) → P (e.symm b)<VAR>b : β<GOAL>∀ (hZa : e.symm (e (e.symm b)) = e.symm b), hZa ▸ g (e (e.symm b)) = g b
<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>P✝ : α → Sort w<VAR>e✝ : α ≃ β<VAR>P : α → Sort u_1<VAR>e : α ≃ β<VAR>g : (b : β) → P (e.symm b)<VAR>b : β<GOAL>∀ (hZa : e.symm b = e.symm b), hZa ▸ g b = g b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l✝ : ℝ≥0<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>hs : s.Subsingleton<VAR>l : ℝ≥0<VAR>x : ℝ<VAR>hx hy : x ∈ s<GOAL>eVariationOn f (s ∩ Icc x x) = ENNReal.ofReal (↑l * (x - x))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f✝ : ℝ → E<VAR>s✝ : Set ℝ<VAR>l✝ : ℝ≥0<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>hs : s.Subsingleton<VAR>l : ℝ≥0<VAR>x : ℝ<VAR>hx hy : x ∈ s<GOAL>0 = ENNReal.ofReal (↑l * (x - x))
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>s : Set α<VAR>x : α<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction H α<VAR>inst✝ : SMulCommClass H G α<VAR>g : H<GOAL>fundamentalInterior G (g • s) = g • fundamentalInterior G s
<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>(fun n => ↑n / log ↑n ^ 2) =o[atTop] fun n => ↑n
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : ↑d < dimH s<GOAL>μH[↑d] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d : ℝ≥0<VAR>h : ∃ i, ∃ (_ : μH[↑i] s = ⊤), ↑d < ↑i<GOAL>μH[↑d] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d d' : ℝ≥0<VAR>hsd' : μH[↑d'] s = ⊤<VAR>hdd' : ↑d < ↑d'<GOAL>μH[↑d] s = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>d d' : ℝ≥0<VAR>hsd' : μH[↑d'] s = ⊤<VAR>hdd' : d < d'<GOAL>μH[↑d] s = ⊤
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : b < 0<GOAL>a * b < 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>Z : D<VAR>F : C ⥤ D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y<VAR>x : C<GOAL>(liftStar F M hM).hom ≫ (lift F M hM).map (starInitial.to (incl.obj x)) = M x ≫ (inclLift F M hM).hom.app x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>Z : D<VAR>F : C ⥤ D<VAR>M : (x : C) → Z ⟶ F.obj x<VAR>hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y<VAR>x : C<GOAL>(lift F M hM).map (starInitial.to (incl.obj x)) = M x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : AddCircle T → E<VAR>n : ℤ<VAR>a : ℝ<VAR>this : ∀ (x : ℝ), (fourier (-n)) ↑x • f ↑x = (fun z => (fourier (-n)) z • f z) ↑x<GOAL>fourierCoeff f n = (1 / T) • ∫ (x : ℝ) in a..a + T, (fun z => (fourier (-n)) z • f z) ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>inst✝ : CompleteSpace H<VAR>K : ConvexCone ℝ H<VAR>ne : (↑K).Nonempty<VAR>hc : IsClosed ↑K<VAR>b : H<VAR>disj : b ∉ K<GOAL>∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>inst✝ : CompleteSpace H<VAR>K : ConvexCone ℝ H<VAR>ne : (↑K).Nonempty<VAR>hc : IsClosed ↑K<VAR>b : H<VAR>disj : b ∉ K<VAR>z : H<VAR>hzK : z ∈ ↑K<VAR>infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖<GOAL>∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>inst✝ : CompleteSpace H<VAR>K : ConvexCone ℝ H<VAR>ne : (↑K).Nonempty<VAR>hc : IsClosed ↑K<VAR>b : H<VAR>disj : b ∉ K<VAR>z : H<VAR>hzK : z ∈ ↑K<VAR>infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖<VAR>hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0<GOAL>∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : InnerProductSpace ℝ H<VAR>s t : Set H<VAR>inst✝ : CompleteSpace H<VAR>K : ConvexCone ℝ H<VAR>ne : (↑K).Nonempty<VAR>hc : IsClosed ↑K<VAR>b : H<VAR>disj : b ∉ K<VAR>z : H<VAR>hzK : z ∈ ↑K<VAR>infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖<VAR>hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0<GOAL>(∀ x ∈ K, 0 ≤ ⟪x, z - b⟫_ℝ) ∧ ⟪z - b, b⟫_ℝ < 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : p = 0<GOAL>(p * q).degree = p.degree + q.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp0 : ¬p = 0<VAR>hq0 : q = 0<GOAL>(p * q).degree = p.degree + q.degree
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : CompleteSpace F<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup P<VAR>inst✝² : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : μ.IsNegInvariant<VAR>L : E' →L[𝕜] E →L[𝕜] F<VAR>s : Set P<VAR>n : ℕ∞<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<GOAL>ContDiffOn 𝕜 n (fun x => (g x ⋆[L, μ] f) (v x)) s
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : CompleteSpace F<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup P<VAR>inst✝² : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : μ.IsNegInvariant<VAR>L : E' →L[𝕜] E →L[𝕜] F<VAR>s : Set P<VAR>n : ℕ∞<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<GOAL>s ⊆ (fun x => (_root_.id x, v x)) ⁻¹' s ×ˢ univ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : RCLike 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace ℝ F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : CompleteSpace F<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>inst✝³ : NormedAddCommGroup P<VAR>inst✝² : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L✝ : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : μ.IsNegInvariant<VAR>L : E' →L[𝕜] E →L[𝕜] F<VAR>s : Set P<VAR>n : ℕ∞<VAR>v : P → G<VAR>hv : ContDiffOn 𝕜 n v s<VAR>f : G → E<VAR>g : P → G → E'<VAR>k : Set G<VAR>hs : IsOpen s<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiffOn 𝕜 n (↿g) (s ×ˢ univ)<VAR>x : P<VAR>hx : x ∈ s<GOAL>x ∈ (fun x => (_root_.id x, v x)) ⁻¹' s ×ˢ univ
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>x : ι → ℝ<GOAL>J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>G H : C<VAR>inst✝ : HasBinaryProduct G H<GOAL>IsCoseparator (G ⨯ H) ↔ IsCoseparating {G, H}
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>G H : C<VAR>inst✝ : HasBinaryProduct G H<VAR>h : IsCoseparator (G ⨯ H)<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ G_1 ∈ {G, H}, ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h<GOAL>u = v
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>G H : C<VAR>inst✝ : HasBinaryProduct G H<VAR>h : IsCoseparating {G, H}<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h<VAR>Z : C<VAR>hZ : Z ∈ {G, H}<VAR>g : Y ⟶ Z<GOAL>u ≫ g = v ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>inst✝ : NeZero m<VAR>i : Fin n<VAR>j : Fin m<GOAL>↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>inst✝ : NeZero m<VAR>i : Fin n<VAR>j : Fin m<GOAL>∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m n : ℕ<VAR>inst✝ : NeZero m<VAR>i : Fin n<VAR>j : Fin m<VAR>x : Fin n<VAR>hx : x ≠ i<GOAL>↑(Pi.single i j x) * m ^ ↑x = 0
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l : Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>a : α<VAR>e : η<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>C : (ι → α) → κ<VAR>hl : IsMono C l<GOAL>IsMono (fun x => C (⇑eα.symm ∘ x ∘ ⇑eι)) (l.reindex eη eα eι)
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>η : Type u_5<VAR>α : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>l : Subspace η α ι<VAR>x : η → α<VAR>i : ι<VAR>a : α<VAR>e : η<VAR>η' : Type u_9<VAR>α' : Type u_10<VAR>ι' : Type u_11<VAR>eη : η ≃ η'<VAR>eα : α ≃ α'<VAR>eι : ι ≃ ι'<VAR>C : (ι → α) → κ<VAR>hl : IsMono C l<GOAL>IsMono (fun x => C (⇑eα.symm ∘ ⇑eα ∘ x)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>hμf : μ {x | f x = ⊤} ≠ 0<GOAL>⊤ = ⊤ * μ {x | ⊤ ≤ f x}
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 < x<GOAL>x ^ y ≤ x ^ z ↔ y ≤ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 1 < x<VAR>x_pos : 0 < x<GOAL>x ^ y ≤ x ^ z ↔ y ≤ z
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<GOAL>∀ (x_1 : ℝ), ‖x_1 - x‖⁻¹ * ‖f x_1 - f x‖ < r → ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>z : ℝ<VAR>hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r<GOAL>‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<VAR>z : ℝ<VAR>hz : ‖z - x‖⁻¹ * ‖f z - f x‖ < r<GOAL>0 ≤ ‖z - x‖⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>t : ℚ<GOAL>(⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>t : ℚ<VAR>h_bdd : BddBelow (range fun r => if ↑r < 0 then 0 else 1)<GOAL>(⨅ r, if ↑r < 0 then 0 else 1) = if t < 0 then 0 else 1
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>g : G<VAR>p q : P<GOAL>g +ᵥ p -ᵥ q = g - (q -ᵥ p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>s : Set α<GOAL>f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0