ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableAt I I' f x<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>HasMFDerivWithinAt I I' f s x (mfderiv I I' f x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝ : Infinite α<VAR>f : α → β<VAR>hi : Injective f<GOAL>(range f).Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝ : Infinite α<VAR>f : α → β<VAR>hi : Injective f<GOAL>univ.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝³ : Ring α<VAR>a b : α<VAR>F : Type u_1<VAR>inst✝² : Ring β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>f : F<VAR>u : αˣ<GOAL>↑((map ↑f) (-u)) = ↑(-(map ↑f) u)
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>c : ℕ → ℝ<VAR>d : ℕ → E<VAR>hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s<VAR>hc : Tendsto c atTop atTop<VAR>hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)<VAR>hc' : Tendsto (fun x => ‖c x‖) atTop atTop<GOAL>f' y ≤ 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>c : ℕ → ℝ<VAR>d : ℕ → E<VAR>hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s<VAR>hc : Tendsto c atTop atTop<VAR>hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)<VAR>hc' : Tendsto (fun x => ‖c x‖) atTop atTop<GOAL>∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>c : ℕ → ℝ<VAR>d : ℕ → E<VAR>hc : Tendsto c atTop atTop<VAR>hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)<VAR>hc' : Tendsto (fun x => ‖c x‖) atTop atTop<VAR>hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))<GOAL>∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>c : ℕ → ℝ<VAR>d : ℕ → E<VAR>hc : Tendsto c atTop atTop<VAR>hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)<VAR>hc' : Tendsto (fun x => ‖c x‖) atTop atTop<VAR>hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)<GOAL>∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMaxOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>c : ℕ → ℝ<VAR>d : ℕ → E<VAR>hc : Tendsto c atTop atTop<VAR>hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)<VAR>hc' : Tendsto (fun x => ‖c x‖) atTop atTop<VAR>hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)<VAR>n : ℕ<VAR>hfn : f (a + d n) ≤ f a<VAR>hcn : 0 ≤ c n<GOAL>c n • (f (a + d n) - f a) ≤ 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : 0 < c<GOAL>(fun x => c * x) ⁻¹' Icc a b = Icc (a / c) (b / c)
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>f g : K[X]<VAR>hg : g ≠ 0<GOAL>RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩
<VAR>n k : ℕ<VAR>hnk : Even (n + k)<GOAL>(hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)
<VAR>n k : ℕ<VAR>hnk : Even (n + k)<VAR>h_le : k ≤ n<GOAL>(hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)
<VAR>n k : ℕ<VAR>hnk : Even (n + k)<VAR>h_lt : n < k<GOAL>(hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1)‼ * ↑(n.choose k)
<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>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<GOAL>Tendsto (fun n => c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 (f' v))
<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>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<GOAL>Tendsto (fun n => c n • (c n)⁻¹ • v) l (𝓝 v)
<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>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>U : Set E<VAR>hU : U ∈ 𝓝 v<GOAL>U ∈ map (fun n => c n • (c n)⁻¹ • v) l
<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>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>U : Set E<VAR>hU : U ∈ 𝓝 v<VAR>y : α<VAR>hy : c y ≠ 0<GOAL>(fun n => c n • (c n)⁻¹ • v) y ∈ U
<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>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>U : Set E<VAR>hU : U ∈ 𝓝 v<VAR>y : α<VAR>hy : c y ≠ 0<GOAL>(fun n => c n • (c n)⁻¹ • v) y = v
<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>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Tendsto (fun n => ‖c n‖) l atTop<VAR>U : Set E<VAR>hU : U ∈ 𝓝 v<VAR>y : α<VAR>hy : c y ≠ 0<GOAL>c y • (c y)⁻¹ • v = v
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>inst✝¹ : HasImages V<VAR>inst✝ : HasEqualizers V<VAR>i i' j : ι<VAR>r : c.Rel i j<VAR>r' : c.Rel i' j<GOAL>imageSubobject (C.d i j) = imageSubobject (C.d i' j)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>inst✝¹ : HasImages V<VAR>inst✝ : HasEqualizers V<VAR>i i' j : ι<VAR>r : c.Rel i j<VAR>r' : c.Rel i' j<GOAL>imageSubobject (eqToHom ⋯ ≫ C.d i' j) = imageSubobject (C.d i' j)
<VAR>X : Scheme<VAR>U : Opens (PrimeSpectrum ↑Γ(X, ⊤))<GOAL>adjunction.unit.app X ⁻¹ᵁ U ≤ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p : α<GOAL>Prime (Associates.mk p) ↔ Prime p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>p : α<GOAL>(Associates.mk p ≠ 0 ∧ ¬IsUnit (Associates.mk p) ∧ ∀ (a : α) (b : Associates α), Associates.mk p ∣ Associates.mk a * b → Associates.mk p ∣ Associates.mk a ∨ Associates.mk p ∣ b) ↔ p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<GOAL>frontier (s ×ˢ univ) = frontier s ×ˢ univ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : x ∈ ball y ε<GOAL>∃ ε' < ε, x ∈ ball y ε'
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : dist x y < ε<GOAL>∃ ε' < ε, dist x y < ε'
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>s t : Multiset α<GOAL>s.Disjoint (a ::ₘ t) ↔ a ∉ s ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>s t : Multiset α<GOAL>a ∉ s ∧ t.Disjoint s ↔ a ∉ s ∧ s.Disjoint t
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>h₁ : IsAddSubgroup s<VAR>h₂ : ∀ n ∈ s, ∀ (g : Additive G), g + n + -g ∈ s<GOAL>IsNormalSubgroup s
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>hx✝ : x ∈ H0 A<VAR>g : G<VAR>hx : (A.ρ g) x = x<GOAL>(dZero A ∘ₗ (H0 A).subtype) ⟨x, hx✝⟩ g = 0 ⟨x, hx✝⟩ g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>hx✝ : x ∈ H0 A<VAR>g : G<VAR>hx : (A.ρ g) x - x = 0<GOAL>(dZero A ∘ₗ (H0 A).subtype) ⟨x, hx✝⟩ g = 0 ⟨x, hx✝⟩ g
<VAR>x : ℝ<GOAL>↑(sign ↑x) * ↑(↑x).abs = ↑x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>a : R<GOAL>(vandermonde fun i => v i + a).det = (vandermonde v).det
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n k : ℕ<GOAL>↑(eval k (ascPochhammer ℕ n)) = eval (↑k) (ascPochhammer S n)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : SetLike σ A<VAR>inst✝² : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>i j : ι<VAR>inst✝¹ : AddLeftCancelMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>b : A<VAR>a : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (↑a * b)) (i + j)) = ↑a * ↑(((decompose 𝒜) b) j)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b : α<GOAL>|b| - |a| ≤ |a - b|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a✝ b✝ c d a b : α<GOAL>|b| - |a| ≤ |b - a|
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>cs.IsRightInversion w⁻¹ t ↔ cs.IsLeftInversion w t
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<GOAL>cs.IsReflection t → (cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w t : W<VAR>ht : cs.IsReflection t<GOAL>cs.length (w⁻¹ * t) < cs.length w⁻¹ ↔ cs.length (t * w) < cs.length w
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>W X X' Y Y' Z : D<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y'<VAR>h' : Y' ⟶ Z<GOAL>f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'
<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✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s<VAR>S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}<GOAL>borel α = MeasurableSpace.generateFrom S
<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✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s<VAR>S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}<GOAL>borel α ≤ MeasurableSpace.generateFrom S
<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✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s<VAR>S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}<VAR>this : MeasurableSpace α := MeasurableSpace.generateFrom S<GOAL>borel α ≤ MeasurableSpace.generateFrom S
<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✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s<VAR>S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}<VAR>this : MeasurableSpace α := MeasurableSpace.generateFrom S<GOAL>MeasurableSpace.generateFrom (range Iio) ≤ MeasurableSpace.generateFrom S
<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✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a✝ b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s<VAR>S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}<VAR>this : MeasurableSpace α := MeasurableSpace.generateFrom S<VAR>a : α<GOAL>MeasurableSet (Iio a)
<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✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a✝ b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → y ∈ s<VAR>S : Set (Set α) := {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ico l u = S}<VAR>this : MeasurableSpace α := MeasurableSpace.generateFrom S<VAR>a : α<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>hc : t.Countable<VAR>htd : Dense t<VAR>htb : ∀ (x : α), IsBot x → x ∈ s → x ∈ t<GOAL>MeasurableSet (Iio a)
<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>x y : V<GOAL>(o.oangle x (x - y)).sign = -(o.oangle x y).sign
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ : α<VAR>hl : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.formPerm x ≠ x ↔ 2 ≤ l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ : α<VAR>hl : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>1 < l.length ↔ 2 ≤ l.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : ι → α<VAR>s : Set α<VAR>h : ∀ (x : ι), f x ∈ s<GOAL>Injective (codRestrict f s h) ↔ Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → ℕ<GOAL>s.EquitableOn f ↔ ∃ b, f '' s ⊆ Icc b (b + 1)
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>H : ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>hP : IsLocalAtTarget P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : Y.OpenCover<VAR>H : ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)<GOAL>∀ (i : 𝒰.J), P (f ∣_ Scheme.Hom.opensRange (𝒰.map i))
<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✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>S : Multiset R<VAR>r : R<VAR>hr : r ∈ S<GOAL>eval r (derivative (Multiset.map (fun a => X - C a) S).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod
<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✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>S : Multiset R<VAR>r : R<VAR>hr : r ∈ S<GOAL>eval r (derivative (Multiset.map (fun a => X - C a) (r ::ₘ S.erase r)).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod
<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✝¹ : CommRing R<VAR>inst✝ : DecidableEq R<VAR>S : Multiset R<VAR>r : R<VAR>hr : r ∈ S<VAR>this : ↑(evalRingHom r) (Multiset.map (fun a => X - C a) (S.erase r)).prod = (Multiset.map (⇑↑(evalRingHom r)) (Multiset.map (fun a => X - C a) (S.erase r))).prod<GOAL>eval r (derivative (Multiset.map (fun a => X - C a) (r ::ₘ S.erase r)).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>n : Type u_8<VAR>inst✝ : Fintype n<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>x✝ : EuclideanSpace ℝ n<GOAL>x✝ ∈ Metric.closedBall 0 r ↔ x✝ ∈ {x | ∑ i : n, x i ^ 2 ≤ r ^ 2}
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>P Q R : C<VAR>f✝ f' : P ⟶ Q<VAR>g✝ g' : Q ⟶ R<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>hc : IsLimit c<VAR>h : IsZero c.pt<VAR>P✝ : C<VAR>g : P✝ ⟶ X<VAR>hg : g ≫ f = 0<VAR>a : P✝ ⟶ c.pt<VAR>ha : a ≫ Fork.ι c = g<GOAL>g = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c p : P<VAR>h : ∠ b p c = π<GOAL>dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b c p : P<VAR>h : ∠ b p c = π<GOAL>(dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p + (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p = (dist b p + dist c p) * (dist a p ^ 2 + dist b p * dist c p)
<VAR>n : ℕ<GOAL>n.divisors.sum φ = n
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>n.divisors.sum φ = n
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>∑ d ∈ n.divisors, φ (n / d) = n
<VAR>n : ℕ<VAR>hn : n > 0<VAR>this : n = ∑ d ∈ n.divisors, (filter (fun k => n.gcd k = d) (range n)).card<GOAL>∑ d ∈ n.divisors, φ (n / d) = n
<VAR>n : ℕ<VAR>hn : n > 0<VAR>this : n = ∑ d ∈ n.divisors, (filter (fun k => n.gcd k = d) (range n)).card<GOAL>∑ d ∈ n.divisors, φ (n / d) = ∑ d ∈ n.divisors, (filter (fun k => n.gcd k = d) (range n)).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>t : Set β<GOAL>univ ×ˢ t = Prod.snd ⁻¹' t
<GOAL>Tendsto (fun s => riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)
<GOAL>Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
<GOAL>Tendsto (fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
<GOAL>?f₁ =ᶠ[𝓝[>] 1] fun s => ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)
<GOAL>Tendsto ?f₁ (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
<VAR>α : Type u_1<VAR>m n : Num<VAR>h : m = n<GOAL>↑m < ↑n ↔ Ordering.eq = Ordering.lt
<VAR>α : Type u_1<VAR>m n : Num<VAR>h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)<GOAL>↑m < ↑n ↔ Ordering.gt = Ordering.lt
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S<VAR>S' : Type u_1<VAR>inst✝² : CommSemiring S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R S<VAR>M : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>Z : Set (PrimeSpectrum S)<GOAL>IsClosed Z ↔ IsClosed Z