ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>g g' : δ → α<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>s : Set δ<VAR>hs : MeasurableSet s<VAR>hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)<VAR>hg' : EqOn g g' sᶜ<VAR>g'_meas : Measurable g'<VAR>i : ι<GOAL>Measurable g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f g : α → β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>s.piecewise f g =ᶠ[ae (μ.restrict sᶜ)] g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f g : α → β<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>hs : MeasurableSet s<GOAL>s.piecewise f g =ᶠ[ae μ ⊓ 𝓟 sᶜ] g
<VAR>o : Ordinal.{u_1}<VAR>l : o.IsLimit<VAR>c : Cardinal.{u_1}<VAR>h : ∀ o' < o, aleph' o' ≤ c<GOAL>aleph' o ≤ c
<VAR>o : Ordinal.{u_1}<VAR>l : o.IsLimit<VAR>c : Cardinal.{u_1}<VAR>h : ∀ o' < o, aleph' o' ≤ c<GOAL>∀ x < o, x ≤ c.alephIdx
<VAR>o : Ordinal.{u_1}<VAR>l : o.IsLimit<VAR>c : Cardinal.{u_1}<VAR>h : ∀ o' < o, aleph' o' ≤ c<VAR>x : Ordinal.{u_1}<VAR>h' : x < o<GOAL>x ≤ c.alephIdx
<VAR>o : Ordinal.{u_1}<VAR>l : o.IsLimit<VAR>c : Cardinal.{u_1}<VAR>h : ∀ o' < o, aleph' o' ≤ c<VAR>x : Ordinal.{u_1}<VAR>h' : x < o<GOAL>aleph' x ≤ c
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a⁻¹ < b / c ↔ c < a * b
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>z : ℂ<GOAL>(Complex.orientation.rotation θ) z = ↑θ.expMapCircle * z
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>z : ℂ<GOAL>↑θ.cos * z + ↑θ.sin * (I * z) = (↑θ.cos + ↑θ.sin * I) * z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<VAR>h : yᶜ ≤ xᶜ<GOAL>x ≤ y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<VAR>h✝ : yᶜ ≤ xᶜ<VAR>h : xᶜᶜ ≤ yᶜᶜ<GOAL>x ≤ y
<VAR>n : ℤ<GOAL>↑(T ^ n) = !![1, n; 0, 1]
<GOAL>↑(T ^ 0) = !![1, 0; 0, 1]
<VAR>n : ℕ<VAR>h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]<GOAL>↑(T ^ (↑n + 1)) = !![1, ↑n + 1; 0, 1]
<VAR>n : ℕ<VAR>h : ↑(T ^ (-↑n)) = !![1, -↑n; 0, 1]<GOAL>↑(T ^ (-↑n - 1)) = !![1, -↑n - 1; 0, 1]
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : ℕ → R<VAR>a : R<VAR>n✝ : ℕ<GOAL>(coeff R n✝) ((rescale a) (mk f)) = (coeff R n✝) (mk fun n => a ^ n * f n)
<VAR>F : 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>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>a < EquivLike.inv f b ↔ f a < b
<VAR>F : 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>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>f a < f (EquivLike.inv f b) ↔ f a < b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>v : V<GOAL>Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>f : G →g G'<VAR>v : V<VAR>x✝¹ x✝ : W<GOAL>⊥ → ∃ x, f x = x✝¹ ∧ ∃ x, f x = x✝
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ<VAR>n : ℕ<VAR>hn : ↑n ≤ N<GOAL>fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w => fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ℵ₀<VAR>hb : ↑n < ℵ₀<GOAL>↑m * ↑n < ℵ₀
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ℵ₀<VAR>hb : ↑n < ℵ₀<GOAL>↑(m * n) < ℵ₀
<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 α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>(a :: l₁ ++ l₂).alternatingProd = (a :: l₁).alternatingProd * l₂.alternatingProd ^ (-1) ^ (a :: l₁).length
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝³ : Fact (1 ≤ p)<VAR>f g : α →ᵇ E<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>(toLp p μ 𝕜) f = (toLp p μ 𝕜) g ↔ f = g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝³ : Fact (1 ≤ p)<VAR>f g : α →ᵇ E<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g<GOAL>f = g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝³ : Fact (1 ≤ p)<VAR>f g : α →ᵇ E<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g<GOAL>⇑f =ᶠ[ae μ] ⇑g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : BorelSpace α<VAR>inst✝⁵ : SecondCountableTopologyEither α E<VAR>inst✝⁴ : IsFiniteMeasure μ<VAR>𝕜 : Type u_5<VAR>inst✝³ : Fact (1 ≤ p)<VAR>f g : α →ᵇ E<VAR>inst✝² : μ.IsOpenPosMeasure<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>h : (toLp p μ 𝕜) f = (toLp p μ 𝕜) g<GOAL>↑↑((toLp p μ 𝕜) f) =ᶠ[ae μ] ↑↑((toLp p μ 𝕜) g)
<VAR>A : Type u_1<VAR>inst✝¹⁰ : NonUnitalNormedRing A<VAR>inst✝⁹ : CompleteSpace A<VAR>inst✝⁸ : Nontrivial A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a b : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>hb : autoParam (IsSelfAdjoint b) _auto✝<GOAL>↑a ≤ ↑b ↔ a ≤ b
<VAR>A : Type u_1<VAR>inst✝¹⁰ : NonUnitalNormedRing A<VAR>inst✝⁹ : CompleteSpace A<VAR>inst✝⁸ : Nontrivial A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : CstarRing A<VAR>inst✝³ : NormedSpace ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : SMulCommClass ℂ A A<VAR>inst✝ : IsScalarTower ℂ A A<VAR>a b : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>hb : autoParam (IsSelfAdjoint b) _auto✝<GOAL>(∀ x ∈ quasispectrum ℝ (b - a), 0 ≤ x) ↔ 0 ≤ b - a
<VAR>a b c : ℕ<VAR>h : a ≤ b + 1<VAR>x : ℕ<GOAL>x ∈ insert (b + 1) (Icc a b) ↔ x ∈ Icc a (b + 1)
<VAR>a b c : ℕ<VAR>h : a ≤ b + 1<VAR>x : ℕ<GOAL>x = b + 1 ∨ a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b + 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>derivative (p ^ Nat.zero) = C ↑Nat.zero * p ^ (Nat.zero - 1) * derivative p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝¹ : ℕ<VAR>inst✝ : CommSemiring R<VAR>p : R[X]<VAR>n✝ n : ℕ<GOAL>derivative (p ^ n.succ) = C ↑n.succ * p ^ (n.succ - 1) * derivative p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>insert a l = if a ∈ l then l else a :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ l₃ : List α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>insert a l = if elem a l = true then l else a :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>L : List α<GOAL>L ⊆ [a] ↔ ∃ n, L = replicate n a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ g✝ : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>f : Ultrafilter α<VAR>g : Filter α<VAR>hg : (g ⊓ ↑f).NeBot<GOAL>(↑f ⊓ g).NeBot
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : b ≤ z<GOAL>(z + 1).inductionOn' b H0 Hs Hp = Hs z hz (z.inductionOn' b H0 Hs Hp)
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : b ≤ z<GOAL>HEq (match z + 1 - b with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n) (Hs z hz (z.inductionOn' b H0 Hs Hp))
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : b ≤ z<VAR>zb : ℕ<VAR>hzb : ↑zb = z - b<GOAL>HEq (match z + 1 - b with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n) (Hs z hz (z.inductionOn' b H0 Hs Hp))
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>zb : ℕ<VAR>hz : b ≤ b + ↑zb<VAR>hzb : ↑zb = b + ↑zb - b<GOAL>HEq (match ↑zb + 1 with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n) (Hs (b + ↑zb) hz ((b + ↑zb).inductionOn' b H0 Hs Hp))
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>zb : ℕ<VAR>hz : b ≤ b + ↑zb<VAR>hzb : ↑zb = b + ↑zb - b<GOAL>(b + ↑zb).inductionOn' b H0 Hs Hp = inductionOn'.pos b H0 Hs zb
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>s✝ : Set α<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>h : ofSet s = PEquiv.refl α<GOAL>s = Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>s✝ : Set α<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>h : ofSet s = PEquiv.refl α<GOAL>∀ (x : α), x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>s✝ : Set α<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>h : ofSet s = PEquiv.refl α<VAR>x✝ : α<GOAL>x✝ ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>s✝ : Set α<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>h : ofSet s = PEquiv.refl α<VAR>x✝ : α<GOAL>x✝ ∈ (PEquiv.refl α) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>s✝ : Set α<VAR>inst✝¹ : DecidablePred fun x => x ∈ s✝<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>h : s = Set.univ<GOAL>ofSet s = PEquiv.refl α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIciTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : Tendsto f (𝓝[s] x) (𝓝 z)<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : x ∈ closure s<GOAL>Tendsto (fun x_1 => F x_1 x) l (𝓝 z)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : x ∈ closure s<GOAL>∀ i ∈ 𝓤 α, ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id i}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : x ∈ closure s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : x ∈ closure s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVs : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<GOAL>∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : (𝓝[s] x).NeBot<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVs : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<GOAL>∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : (𝓝[s] x).NeBot<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVs : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<VAR>this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V<GOAL>∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : (𝓝[s] x).NeBot<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVs : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<VAR>this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V<VAR>y : X<VAR>hys : y ∈ s<VAR>hFy : ∀ (i : ι), (F i x, F i y) ∈ V<VAR>hfy : (f y, z) ∈ V<GOAL>∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}<VAR>hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))<VAR>hx : (𝓝[s] x).NeBot<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<VAR>hVs : SymmetricRel V<VAR>hVU : V ○ V ○ V ⊆ U<VAR>this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V<VAR>y : X<VAR>hys : y ∈ s<VAR>hFy : ∀ (i : ι), (F i x, F i y) ∈ V<VAR>hfy : (f y, z) ∈ V<VAR>i : ι<VAR>hi : i ∈ (fun x => F x y) ⁻¹' ball (f y) V<GOAL>(F i x, z) ∈ id U
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hx : F.obj X = G.obj X<VAR>hy : F.obj Y = G.obj Y<VAR>hz : F.obj Z = G.obj Z<VAR>hf : HEq (F.map f) (G.map f)<VAR>hg : HEq (F.map g) (G.map g)<GOAL>HEq (F.map (f ≫ g)) (G.map (f ≫ g))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hx : F.obj X = G.obj X<VAR>hy : F.obj Y = G.obj Y<VAR>hz : F.obj Z = G.obj Z<VAR>hf : HEq (F.map f) (G.map f)<VAR>hg : HEq (F.map g) (G.map g)<GOAL>HEq (F.map f ≫ F.map g) (G.map f ≫ G.map g)
<VAR>p q✝ q : ℚ≥0<GOAL>(↑q).num = ↑q.num
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁷ : Fintype ι<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁴ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹³ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝¹⁰ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁹ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁸ : SeminormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace 𝕜 G<VAR>inst✝⁶ : SeminormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f✝ g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedSpace 𝕜' G<VAR>inst✝² : SMulCommClass 𝕜 𝕜' G<VAR>inst✝¹ : (i' : ι') → SeminormedAddCommGroup (E' i')<VAR>inst✝ : (i' : ι') → NormedSpace 𝕜 (E' i')<VAR>f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')<VAR>x✝ : ℝ≥0<GOAL>‖pi f‖₊ ≤ x✝ ↔ ‖f‖₊ ≤ x✝
<VAR>E : Type u_1<VAR>f✝ f'✝ : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>hf : ContDiff ℝ 1 f<VAR>h'f : HasCompactSupport f<VAR>x : ℝ<VAR>I : F →L[ℝ] Completion F := Completion.toComplL<VAR>f' : ℝ → Completion F := ⇑I ∘ f<GOAL>↑‖f x‖₊ ≤ ∫⁻ (y : ℝ) in Iic x, ↑‖deriv f y‖₊
<VAR>E : Type u_1<VAR>f✝ f'✝ : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>hf : ContDiff ℝ 1 f<VAR>h'f : HasCompactSupport f<VAR>x : ℝ<VAR>I : F →L[ℝ] Completion F := Completion.toComplL<VAR>f' : ℝ → Completion F := ⇑I ∘ f<VAR>hf' : ContDiff ℝ 1 f'<GOAL>↑‖f x‖₊ ≤ ∫⁻ (y : ℝ) in Iic x, ↑‖deriv f y‖₊
<VAR>E : Type u_1<VAR>f✝ f'✝ : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>hf : ContDiff ℝ 1 f<VAR>h'f : HasCompactSupport f<VAR>x : ℝ<VAR>I : F →L[ℝ] Completion F := Completion.toComplL<VAR>f' : ℝ → Completion F := ⇑I ∘ f<VAR>hf' : ContDiff ℝ 1 f'<VAR>h'f' : HasCompactSupport f'<GOAL>↑‖f x‖₊ ≤ ∫⁻ (y : ℝ) in Iic x, ↑‖deriv f y‖₊
<VAR>E : Type u_1<VAR>f✝ f'✝ : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>hf : ContDiff ℝ 1 f<VAR>h'f : HasCompactSupport f<VAR>x : ℝ<VAR>I : F →L[ℝ] Completion F := Completion.toComplL<VAR>f' : ℝ → Completion F := ⇑I ∘ f<VAR>hf' : ContDiff ℝ 1 f'<VAR>h'f' : HasCompactSupport f'<VAR>this : ↑‖f' x‖₊ ≤ ∫⁻ (y : ℝ) in Iic x, ↑‖deriv f' y‖₊<GOAL>↑‖f x‖₊ ≤ ∫⁻ (y : ℝ) in Iic x, ↑‖deriv f y‖₊
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>h : Pairwise (Disjoint on fun i => (M i).E)<VAR>I X : Set α<GOAL>(Matroid.disjointSigma M h).Basis I X ↔ (∀ (i : ι), (M i).Basis (I ∩ (M i).E) (X ∩ (M i).E)) ∧ I ⊆ X ∧ X ⊆ ⋃ i, (M i).E
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f + g) ≫ h = f ≫ h + g ≫ h