ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>hn : x₁.Numeric<VAR>h : IH24 x₁ x₂ y<VAR>he : x₁ ≈ x₂<VAR>i : x₁.LeftMoves<VAR>j : y.LeftMoves<GOAL>x₁.moveLeft i < x₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>E : Type u_4<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f : β → E<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>inst✝¹ : MeasurableSingletonClass β<VAR>s : Set β<VAR>inst✝ : Decidable (g a ∈ s)<GOAL>∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : x ∉ closure s<GOAL>derivWithin f s x = 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>hurwitzZetaEven (-a) s = hurwitzZetaEven a s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<GOAL>LocallyCompactSpace X ↔ LocallyCompactSpace Y
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<GOAL>0 < logb b x ↔ x < 1
<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>i : ι<VAR>a : α<VAR>f✝ g✝ : ι → α<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>m n : ℕ<VAR>f g : ℕ → α<GOAL>(∑ i ∈ range (m + 1), f i) * ∑ i ∈ range (n + 1), g i = (∑ i ∈ range m, f i) * ∑ i ∈ range n, g i + f m * ∑ i ∈ range n, g i + (∑ i ∈ range m, f i) * g n + f m * g n
<VAR>a✝ b✝ m n p✝ p a b : ℕ<VAR>hab : a.Coprime b<GOAL>(a * b).factorization p = a.factorization p + b.factorization p
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Finite σ<GOAL>ker (evalᵢ σ K) = ⊥
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Finite σ<VAR>val✝ : Fintype σ<GOAL>ker (evalᵢ σ K) = ⊥
<VAR>σ K : Type u<VAR>inst✝² : Fintype K<VAR>inst✝¹ : Field K<VAR>inst✝ : Finite σ<VAR>val✝ : Fintype σ<GOAL>FiniteDimensional.finrank K (R σ K) = FiniteDimensional.finrank K ((σ → K) → K)
<VAR>p : ℕ<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : CompatibleRing K<GOAL>K ⊨ Theory.fieldOfChar p ↔ CharP K p
<VAR>p : ℕ<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : CompatibleRing K<GOAL>(K ⊨ if p = 0 then (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥}) ↔ CharP K p
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b c : α<VAR>hab : Disjoint a b<VAR>hbc : Codisjoint b c<GOAL>a ≤ c
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b c : α<VAR>hab : Disjoint a b<VAR>hbc : Codisjoint b c<GOAL>a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n ν : ℕ<VAR>h : n < ν<GOAL>bernsteinPolynomial R n ν = 0
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>f : α → β<VAR>hcf : Continuous f<VAR>h : stoneCechUnit a = stoneCechUnit b<GOAL>f a = f b
<VAR>α : Type u<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type v<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : CompactSpace β<VAR>g : α → β<VAR>hg : Continuous g<VAR>a b : α<VAR>f : α → β<VAR>hcf : Continuous f<VAR>h : stoneCechUnit a = stoneCechUnit b<GOAL>(stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b
<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 x y t u v : V<VAR>p : G.Walk u v<VAR>h : G.Adj t u<GOAL>notNilRec (fun {u v w} x q => q) (cons h p) ⋯ = p
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>diam (s ∪ t) ≤ diam s + edist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<VAR>A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t<GOAL>diam (s ∪ t) ≤ diam s + edist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<VAR>A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t<VAR>a : α<VAR>ha : a ∈ s ∪ t<VAR>b : α<VAR>hb : b ∈ s ∪ t<GOAL>edist a b ≤ diam s + edist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<VAR>A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t<VAR>a : α<VAR>ha : a ∈ s ∪ t<VAR>b : α<VAR>hb : b ∈ s ∪ t<VAR>h'a : a ∈ s<VAR>h'b : b ∈ s<GOAL>edist a b ≤ diam s + edist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<VAR>A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t<VAR>a : α<VAR>ha : a ∈ s ∪ t<VAR>b : α<VAR>hb : b ∈ s ∪ t<VAR>h'a : a ∈ s<VAR>h'b : b ∈ t<GOAL>edist a b ≤ diam s + edist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<VAR>A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t<VAR>a : α<VAR>ha : a ∈ s ∪ t<VAR>b : α<VAR>hb : b ∈ s ∪ t<VAR>h'a : a ∈ t<VAR>h'b : b ∈ s<GOAL>edist a b ≤ diam s + edist x y + diam t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<VAR>A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t<VAR>a : α<VAR>ha : a ∈ s ∪ t<VAR>b : α<VAR>hb : b ∈ s ∪ t<VAR>h'a : a ∈ t<VAR>h'b : b ∈ t<GOAL>edist a b ≤ diam s + edist x y + diam t
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<VAR>X : C<GOAL>a₁ + a₂₃ = a₁₂₃
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A<VAR>h₁₂ : a₁ + a₂ = a₁₂<VAR>h₂₃ : a₂ + a₃ = a₂₃<VAR>h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃<VAR>X : C<GOAL>(shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X) ≫ (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X = (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((shiftFunctor C a₁).obj X) ≫ (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Multiset { a // Irreducible a }<GOAL>↑a ⊔ ↑b + ↑a ⊓ ↑b = ↑a + ↑b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : DecidableEq (Associates α)<VAR>a b : Multiset { a // Irreducible a }<GOAL>a ⊔ b + a ⊓ b = a + b
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>Lagrange.basis {i, j} v j = basisDivisor (v j) (v i)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>Lagrange.basis {j, i} v j = basisDivisor (v j) (v i)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>X₁ : C₁<VAR>a : X₂ ⟶ T.obj X₁<VAR>b : L.obj X₁ ⟶ X₃<VAR>comm : R.map a ≫ w.app X₁ ≫ B.map b = g<VAR>f : w.CostructuredArrowDownwards g<GOAL>∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g), f = mk w g X₁ a b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g✝ : R.obj X₂ ⟶ B.obj X₃<VAR>X₁ : C₁<VAR>a : X₂ ⟶ T.obj X₁<VAR>b : L.obj X₁ ⟶ X₃<VAR>comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝<VAR>g : StructuredArrow X₂ T<VAR>φ : (w.structuredArrowDownwards X₂).obj g ⟶ StructuredArrow.mk g✝<GOAL>∃ X₁ a b, ∃ (comm : R.map a ≫ w.app X₁ ≫ B.map b = g✝), CostructuredArrow.mk φ = mk w g✝ X₁ a b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>X₁✝ : C₁<VAR>a✝ : X₂ ⟶ T.obj X₁✝<VAR>b : L.obj X₁✝ ⟶ X₃<VAR>comm : R.map a✝ ≫ w.app X₁✝ ≫ B.map b = g<VAR>X₁ : C₁<VAR>a : X₂ ⟶ T.obj X₁<VAR>φ : (w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a) ⟶ StructuredArrow.mk g<GOAL>∃ X₁_1 a_1 b, ∃ (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b = g), CostructuredArrow.mk φ = mk w g X₁_1 a_1 b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>X₁✝ : C₁<VAR>a✝ : X₂ ⟶ T.obj X₁✝<VAR>b✝ : L.obj X₁✝ ⟶ X₃<VAR>comm : R.map a✝ ≫ w.app X₁✝ ≫ B.map b✝ = g<VAR>X₁ : C₁<VAR>a : X₂ ⟶ T.obj X₁<VAR>b : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).right ⟶ (StructuredArrow.mk g).right<VAR>hb : ((w.structuredArrowDownwards X₂).obj (StructuredArrow.mk a)).hom ≫ B.map b = (StructuredArrow.mk g).hom<GOAL>∃ X₁_1 a_1 b_1, ∃ (comm : R.map a_1 ≫ w.app X₁_1 ≫ B.map b_1 = g), CostructuredArrow.mk (StructuredArrow.homMk b hb) = mk w g X₁_1 a_1 b_1 comm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<VAR>this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ<GOAL>⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<VAR>this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ<GOAL>⟪x, x⟫_ℝ + ⟪x, y⟫_ℝ + ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Iio a ∩ Ioo b c = Ioo b (min a c)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ fract ⁻¹' s ↔ x ∈ ⋃ m, (fun x => x - ↑m) ⁻¹' (s ∩ Ico 0 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<GOAL>fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<GOAL>(∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1) → fract x ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<VAR>m : ℤ<VAR>hms : x - ↑m ∈ s<VAR>hm0 : 0 ≤ x - ↑m<VAR>hm1 : x - ↑m < 1<GOAL>fract x ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>s : Set α<VAR>x : α<VAR>hms : x - ↑⌊x⌋ ∈ s<VAR>hm0 : 0 ≤ x - ↑⌊x⌋<VAR>hm1 : x - ↑⌊x⌋ < 1<GOAL>fract x ∈ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<GOAL>∑ i : I, (⇑f ∘ e) i = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>x✝ x : E<GOAL>x ∈ K.vertices ↔ x ∈ ⋃ k ∈ K.faces, ↑k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s t : Finset E<VAR>x✝ x : E<VAR>h : x ∈ ⋃ k ∈ K.faces, ↑k<GOAL>x ∈ K.vertices
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>K : SimplicialComplex 𝕜 E<VAR>s✝ t : Finset E<VAR>x✝ x : E<VAR>h : x ∈ ⋃ k ∈ K.faces, ↑k<VAR>s : Finset E<VAR>hs : s ∈ K.faces<VAR>hx : x ∈ ↑s<GOAL>x ∈ K.vertices
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>x : α<GOAL>x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>x : α<GOAL>infEdist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G : OplaxFunctor B C<VAR>η θ ι : F ⟶ G<VAR>Γ : Modification η θ<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ F.obj b<VAR>g : b ⟶ c<GOAL>f ◁ F.map g ◁ Γ.app c ≫ f ◁ θ.naturality g = f ◁ η.naturality g ≫ f ◁ Γ.app b ▷ G.map g
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (0 ≤ a) _auto✝<GOAL>‖a‖₊ ∈ spectrum ℝ≥0 a
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (0 ≤ a) _auto✝<VAR>this : IsSelfAdjoint a<GOAL>‖a‖₊ ∈ spectrum ℝ≥0 a
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (0 ≤ a) _auto✝<VAR>this : IsSelfAdjoint a<GOAL>‖a‖₊ = (spectralRadius ℝ a).toNNReal
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (0 ≤ a) _auto✝<VAR>this : IsSelfAdjoint a<GOAL>(spectrum ℝ a).Nonempty
<VAR>x y : ℂ<VAR>n : ℤ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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 g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r' : ℝ≥0∞<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>(fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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 g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ : ℝ≥0∞<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>r'0 : 0 < ↑r'<VAR>h : ↑r' < r<GOAL>(fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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 g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ : ℝ≥0∞<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>r'0 : 0 < ↑r'<VAR>h : ↑r' < r<VAR>a C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<GOAL>(fun y => f (x + y) - p.partialSum n y) =O[𝓝 0] fun y => ‖y‖ ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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 g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ : ℝ≥0∞<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>r'0 : 0 < ↑r'<VAR>h : ↑r' < r<VAR>a C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - p.partialSum n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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 g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ : ℝ≥0∞<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>h : ↑r' < r<VAR>a C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<VAR>r'0 : 0 < ↑r'<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - p.partialSum n x_1‖ ≤ C * (a / ↑r') ^ n * ‖‖x_1‖ ^ n‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<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 g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ : ℝ≥0∞<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>h : ↑r' < r<VAR>a C : ℝ<VAR>hp : ∀ y ∈ Metric.ball 0 ↑r', ∀ (n : ℕ), ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n<VAR>r'0 : 0 < ↑r'<VAR>y : E<VAR>hy : y ∈ Metric.ball 0 ↑r'<GOAL>‖f (x + y) - p.partialSum n y‖ ≤ C * (a / ↑r') ^ n * ‖‖y‖ ^ n‖
<VAR>a : ℤ<VAR>b ab' : ℕ<VAR>ab r b' : ℤ<VAR>hb' : ↑b = b'<VAR>hab : a % b' = ab<VAR>h : ↑ab' = ab<VAR>hr : jacobiSymNat ab' b = r<GOAL>jacobiSym a b = r
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>Continuous fun ν => ν.map f
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : MeasurableSpace Ω'<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω'<VAR>inst✝ : BorelSpace Ω'<VAR>f : Ω → Ω'<VAR>f_cont : Continuous f<GOAL>∀ (x : FiniteMeasure Ω), ContinuousAt (fun ν => ν.map f) x
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<GOAL>p ^ n.factorization p ∣ n
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<GOAL>p ^ count p n.primeFactorsList ∣ n
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<GOAL>(p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<GOAL>∀ x ∈ replicate (count p n.primeFactorsList) p, count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<VAR>q : ℕ<VAR>hq : q ∈ replicate (count p n.primeFactorsList) p<GOAL>count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁶ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>𝕜' : Type u_4<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : (i : α) → Module 𝕜' (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)<VAR>hp : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝⁶ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>𝕜' : Type u_4<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : (i : α) → Module 𝕜' (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)<VAR>c : 𝕜<VAR>hp : 0 ≠ 0<VAR>f : ↥(lp E 0)<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝⁶ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>𝕜' : Type u_4<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : (i : α) → Module 𝕜' (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)<VAR>c : 𝕜<VAR>hp : ⊤ ≠ 0<VAR>f : ↥(lp E ⊤)<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁶ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>𝕜' : Type u_4<VAR>inst✝⁵ : NormedRing 𝕜<VAR>inst✝⁴ : NormedRing 𝕜'<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : (i : α) → Module 𝕜' (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)<VAR>hp✝ : p ≠ 0<VAR>c : 𝕜<VAR>f : ↥(lp E p)<VAR>hp : 0 < p.toReal<GOAL>‖c • f‖ ≤ ‖c‖ * ‖f‖
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>x : M<VAR>h : v x = 0<VAR>t : ℝ<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (fun x_1 => x) t (ContinuousLinearMap.smulRight 1 (v ((fun x_1 => x) t)))
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>x : M<VAR>h : v x = 0<VAR>t : ℝ<GOAL>HasMFDerivAt 𝓘(ℝ, ℝ) I (fun x_1 => x) t 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌈a⌉₊ = ⌈a⌉