ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set X<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hX : (𝓝 x₀).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
<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>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set X<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hX : (𝓝 x₀).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>(∀ (ib : κ₂), p₂ ib → ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s₂ ib)}) ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>m : ℕ<VAR>l : List ℕ<VAR>n : ℕ<VAR>h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)<GOAL>raise (lower (m :: l) n) n = m :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>m : ℕ<VAR>l : List ℕ<VAR>n : ℕ<VAR>h : Sorted (fun x x_1 => x ≤ x_1) (n :: m :: l)<VAR>this : n ≤ m<GOAL>raise (lower (m :: l) n) n = m :: l
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>m : OuterMeasure α<VAR>s : Set α<VAR>h : MeasurableSet s<VAR>t : Set α<GOAL>(a • m) t = (a • m) (t ∩ s) + (a • m) (t \ s)
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>m : OuterMeasure α<VAR>s : Set α<VAR>h : MeasurableSet s<VAR>t : Set α<GOAL>a * m t = a * m (t ∩ s) + a * m (t \ s)
<VAR>α : Type u_1<VAR>a : ℝ≥0∞<VAR>m : OuterMeasure α<VAR>s : Set α<VAR>h : MeasurableSet s<VAR>t : Set α<GOAL>a * (m (t ∩ s) + m (t \ s)) = a * m (t ∩ s) + a * m (t \ s)
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<VAR>c d : C<GOAL>X c d ⊆ ⋂ S ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, S.arrows c d
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>X : (c d : C) → Set (c ⟶ d)<VAR>c d : C<GOAL>∀ i ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, X c d ⊆ i.arrows c d
<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>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>hl : HasFDerivAt l l' (f x)<VAR>hf : HasDerivWithinAt f f' s x<VAR>hy : y = f x<GOAL>HasDerivWithinAt (l ∘ f) (l' f') s x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>W.addX P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q - W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2 - Q x * P z ^ 2 * addZ P Q ^ 2) / (P z * Q z) ^ 2
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>ι : Type u_1<VAR>f : ι → F<VAR>s : Finset ι<VAR>H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y<GOAL>(∏ i ∈ s, (X - C (f i))).Separable
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>ι : Type u_1<VAR>f : ι → F<VAR>s : Finset ι<VAR>H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y<GOAL>(∏ x ∈ s.attach, (X - C (f ↑x))).Separable
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α✝ → Type u_5<VAR>fa : α✝ → α✝<VAR>fb : β✝ → β✝<VAR>f : α✝ → β✝<VAR>g : β✝ → γ<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LinearOrder β<VAR>φ : β → α<VAR>ψ : α → β<VAR>t : Set β<VAR>s : Set α<VAR>hφ : MonotoneOn φ t<VAR>φψs : RightInvOn ψ φ s<VAR>ψts : MapsTo ψ s t<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>ys : y ∈ s<VAR>l : x ≤ y<GOAL>ψ x ≤ ψ y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α✝ → Type u_5<VAR>fa : α✝ → α✝<VAR>fb : β✝ → β✝<VAR>f : α✝ → β✝<VAR>g : β✝ → γ<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LinearOrder β<VAR>φ : β → α<VAR>ψ : α → β<VAR>t : Set β<VAR>s : Set α<VAR>hφ : MonotoneOn φ t<VAR>φψs : RightInvOn ψ φ s<VAR>ψts : MapsTo ψ s t<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>ys : y ∈ s<VAR>l : x ≤ y<VAR>ψxy : ψ x ≤ ψ y<GOAL>ψ x ≤ ψ y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α✝ → Type u_5<VAR>fa : α✝ → α✝<VAR>fb : β✝ → β✝<VAR>f : α✝ → β✝<VAR>g : β✝ → γ<VAR>s✝ t✝ : Set α✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LinearOrder β<VAR>φ : β → α<VAR>ψ : α → β<VAR>t : Set β<VAR>s : Set α<VAR>hφ : MonotoneOn φ t<VAR>φψs : RightInvOn ψ φ s<VAR>ψts : MapsTo ψ s t<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>ys : y ∈ s<VAR>l : x ≤ y<VAR>ψyx : ψ y ≤ ψ x<GOAL>ψ x ≤ ψ y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Group G<VAR>g h : G<GOAL>h ∈ orbit (ConjAct G) g ↔ h ∈ (ConjClasses.mk g).carrier
<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝ : T2Space M<GOAL>(𝓝 c).HasBasis (fun x => True) fun f => tsupport ↑f
<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁴ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝ : T2Space M<VAR>this : (𝓝 c).HasBasis (fun x => True) fun f => ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)<GOAL>(𝓝 c).HasBasis (fun x => True) fun f => tsupport ↑f
<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>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>(adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) 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>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X' ⟶ X<VAR>g : F.obj X ⟶ Y<GOAL>F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)
<VAR>a b : Ordinal.{u}<VAR>ha : a ≠ 0<VAR>hb : Principal (fun x x_1 => x * x_1) b<VAR>hb₂ : 2 < b<GOAL>a * b = b ^ succ (log b a)
<VAR>a b : Ordinal.{u}<VAR>ha : a ≠ 0<VAR>hb : Principal (fun x x_1 => x * x_1) b<VAR>hb₂ : 2 < b<GOAL>a * b ≤ b ^ succ (log b a)
<VAR>a b : Ordinal.{u}<VAR>ha : a ≠ 0<VAR>hb : Principal (fun x x_1 => x * x_1) b<VAR>hb₂ : 2 < b<GOAL>b ^ succ (log b a) ≤ a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν = μ s
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f g : K[X]<GOAL>IsCoprime f g ↔ ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f g : K[X]<VAR>h : ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0<GOAL>¬(f = 0 ∧ g = 0)
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>f g : K[X]<VAR>h : ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A), (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0<VAR>x : K[X]<VAR>hx : x ∈ nonunits K[X]<VAR>x✝ : x ≠ 0<GOAL>x ∣ f → ¬x ∣ g
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<VAR>x y : X<VAR>δx_eq_δy : (fun x => diracProba x) x = (fun x => diracProba x) y<GOAL>x = y
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>inst✝ : T0Space X<VAR>x y : X<VAR>δx_eq_δy : (fun x => diracProba x) x = (fun x => diracProba x) y<VAR>x_ne_y : ¬x = y<GOAL>False
<VAR>f : Code → ℕ →. ℕ<VAR>hf : Partrec₂ f<VAR>cf : Code<VAR>ef : cf.eval = fun n => (↑(decode n)).bind fun a => Part.map encode ((fun p => f p.1 p.2) a)<VAR>c : Code<VAR>e : (cf.curry (encode c)).eval = c.eval<VAR>n : ℕ<GOAL>c.eval n = f c n
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<GOAL>x ≡ 0 [SMOD U] ↔ x ∈ U
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α✝<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α✝ → β<VAR>α : Type u_3<VAR>inst✝ : TopologicalSpace α<GOAL>IsQuasiSeparated Set.univ ↔ QuasiSeparatedSpace α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α✝<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α✝ → β<VAR>α : Type u_3<VAR>inst✝ : TopologicalSpace α<GOAL>IsQuasiSeparated Set.univ ↔ ∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>p : α → Prop<VAR>this : Fintype α<GOAL>Nat.card { x // p x } ≤ Nat.card α
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Fintype ι<VAR>m : E<VAR>i : ι<GOAL>(b.repr ↑(floor b m)) i = ↑⌊(b.repr m) i⌋
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>a : α<VAR>ha : a ∉ s<GOAL>(ofMultiset s hs) a = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁵ : NonUnitalNonAssocSemiring α<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Monoid R<VAR>inst✝² : NonUnitalNonAssocSemiring S<VAR>inst✝¹ : DistribMulAction R S<VAR>inst✝ : SMulCommClass R S S<VAR>M : Matrix m n S<VAR>b : R<VAR>v : n → S<VAR>i : m<GOAL>(M *ᵥ b • v) i = (b • M *ᵥ v) i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>hpq : q.degree < p.degree<GOAL>(p + q).Monic
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>a + (b - a) = max a b
<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>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivAt h₂ h₂' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hy : y = h x<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π
<VAR>a b m n✝ p✝ p k n : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<GOAL>p ^ k ∣ n ↔ p ^ k ∣ p ^ n.factorization p
<VAR>n : ℕ∞<VAR>x : Cardinal.{u_1}<GOAL>↑n ≤ x ↔ n ≤ x.toENatAux
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>𝓝 ∞ = map some (coclosedCompact X) ⊔ pure ∞
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<VAR>f : ℝ → A := Function.update (u * v) a a'<GOAL>∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<VAR>f : ℝ → A := Function.update (u * v) a a'<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x<GOAL>∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<VAR>f : ℝ → A := Function.update (u * v) a a'<VAR>hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x<VAR>htendsto : Tendsto f atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Iic a, u' x * v x + u x * v' x = a' - b'
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<VAR>Φ : FreeGroupoid V ⥤ V'<VAR>hΦ : of V ⋙q Φ.toPrefunctor = φ<GOAL>Φ = lift φ
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<VAR>Φ : FreeGroupoid V ⥤ V'<VAR>hΦ : of V ⋙q Φ.toPrefunctor = φ<GOAL>Quotient.functor redStep ⋙ Φ = Paths.lift (Quiver.Symmetrify.lift φ)
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<VAR>Φ : FreeGroupoid V ⥤ V'<VAR>hΦ : of V ⋙q Φ.toPrefunctor = φ<GOAL>Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor = Quiver.Symmetrify.lift φ
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<VAR>Φ : FreeGroupoid V ⥤ V'<VAR>hΦ : of V ⋙q Φ.toPrefunctor = φ<GOAL>Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor) = φ
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<VAR>Φ : FreeGroupoid V ⥤ V'<VAR>hΦ : of V ⋙q Φ.toPrefunctor = φ<GOAL>∀ {X Y : Quiver.Symmetrify V} (f : X ⟶ Y), (Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map (Quiver.reverse f) = Quiver.reverse ((Paths.of ⋙q (Quotient.functor redStep ⋙ Φ).toPrefunctor).map f)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝¹⁸ : SeminormedRing 𝕜<VAR>inst✝¹⁷ : SeminormedRing 𝕜₂<VAR>inst✝¹⁶ : SeminormedRing 𝕜₃<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹⁵ : RingHomIsometric σ₁₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>inst✝¹⁴ : RingHomIsometric σ₂₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹³ : RingHomIsometric σ₁₃<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : AddCommGroup E₂<VAR>inst✝¹⁰ : AddCommGroup E₃<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : AddCommGroup G<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜₂ E₂<VAR>inst✝⁵ : Module 𝕜₃ E₃<VAR>inst✝⁴ : Module 𝕜 F<VAR>inst✝³ : Module 𝕜 G<VAR>inst✝² : SMul R ℝ<VAR>inst✝¹ : SMul R ℝ≥0<VAR>inst✝ : IsScalarTower R ℝ≥0 ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<GOAL>s.sup p ≤ ∑ i ∈ s, p i
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : 𝒜.Shatters s<VAR>t : Finset α<GOAL>t ∈ image (fun t => s ∩ t) 𝒜 ↔ t ∈ s.powerset
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : image (fun t => s ∩ t) 𝒜 = s.powerset<VAR>t : Finset α<VAR>ht : t ⊆ s<GOAL>∃ u ∈ 𝒜, s ∩ u = t
<VAR>C : Type u_1<VAR>D : Type u_4<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{u_3, u_4} D<VAR>K : Coverage C<VAR>P : Cᵒᵖ ⥤ D<GOAL>IsSheaf (toGrothendieck C K) P ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, Nonempty (IsLimit (P.mapCone (Sieve.generate R).arrows.cocone.op))
<VAR>C : Type u_1<VAR>D : Type u_4<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Category.{u_3, u_4} D<VAR>K : Coverage C<VAR>P : Cᵒᵖ ⥤ D<GOAL>(∀ (E : D) {X : C}, ∀ R ∈ K.covering X, Presieve.IsSheafFor (P ⋙ coyoneda.obj (Opposite.op E)) R) ↔ ∀ ⦃X : C⦄, ∀ R ∈ K.covering X, ∀ (E : Dᵒᵖ), Presieve.IsSheafFor (P ⋙ coyoneda.obj E) R
<VAR>α : Type u_1<VAR>l : List α<VAR>x : α<VAR>inst✝ : DecidableEq α<GOAL>x ∈+ l ↔ 2 ≤ count x l
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<VAR>n : ℕ<VAR>hn : q.degree ≤ ↑n<VAR>a✝ : Nontrivial R<GOAL>∑ i : Fin n, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
<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>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hα : (𝓤 α).HasBasis p s<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
<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>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hα : (𝓤 α).HasBasis p s<GOAL>(∀ (i : κ), p i → ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑UniformFun.ofFun ∘ swap F) x ∈ {g | ((⇑UniformFun.ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α (s i)}) ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>ha : ¬IsMax a<GOAL>Icc (succ a) b = Ioc a b
<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>F G : C ⥤ D<VAR>X Y : C<VAR>e : X ≅ Y<VAR>hX : F.obj X = G.obj X<VAR>hY : F.obj Y = G.obj Y<VAR>h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯<GOAL>F.map e.inv = eqToHom ⋯ ≫ G.map e.inv ≫ eqToHom ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<GOAL>Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (ball x δ) (closedBall y ε)<VAR>hxy : dist x y < δ + ε<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (ball x δ) (closedBall y ε)<VAR>hxy : dist x y < ε + δ<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (ball x δ) (closedBall y ε)<VAR>hxy : dist x y < ε + δ<VAR>z : E<VAR>hxz : dist x z < δ<VAR>hzy : dist z y ≤ ε<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z✝ : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 ≤ ε<VAR>h : Disjoint (ball x δ) (closedBall y ε)<VAR>hxy : dist x y < ε + δ<VAR>z : E<VAR>hxz : dist z x < δ<VAR>hzy : dist z y ≤ ε<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : GroupWithZero α<VAR>s✝ t s : Finset α<GOAL>s / 0 ⊆ 0
<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 v✝ : V<VAR>h : G.Adj u v✝<VAR>p' : G.Walk v✝ v<VAR>d : G.Dart<VAR>hd : d ∈ (cons h p').darts<GOAL>d.toProd.1 ∈ (cons h p').support
<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 v✝ : V<VAR>h : G.Adj u v✝<VAR>p' : G.Walk v✝ v<VAR>d : G.Dart<VAR>hd : d = { toProd := (u, v✝), adj := h } ∨ d ∈ p'.darts<GOAL>d.toProd.1 = u ∨ d.toProd.1 ∈ p'.support
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<VAR>c₁ : ℝ<VAR>left✝ : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂ : c₂ > 0<VAR>h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c₂ * f x
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : GrowsPolynomially f<VAR>c₁ : ℝ<VAR>left✝ : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂ : c₂ > 0<VAR>h : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<GOAL>∀ (a : ℝ), (∀ u ∈ Set.Icc (b * a) a, f u ∈ Set.Icc (c₁ * f a) (c₂ * f a)) → ∀ u ∈ Set.Icc (b * a) a, f u ≤ c₂ * f a
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : BoundarylessManifold I M<GOAL>I.boundary M = ∅
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log (abs z)) + ↑π * I))