ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>span R {x} * (M + span R {y}) ≤ M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>span R {x} * M + span R {x} * span R {y} ≤ M
<VAR>R✝ : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommSemiring R✝<VAR>inst✝⁵ : CommSemiring S<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsNoetherianRing R<VAR>A : Type u<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsNoetherianRing A<VAR>I M : Ideal R<VAR>hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J<VAR>h_prM : ¬M.IsPrime<VAR>htop : ¬M = ⊤<VAR>lt_add : ∀ z ∉ M, M < M + span R {z}<VAR>x : R<VAR>hx : x ∉ M<VAR>y : R<VAR>hy : y ∉ M<VAR>hxy : x * y ∈ M<VAR>Wx : Multiset (PrimeSpectrum R)<VAR>h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}<VAR>Wy : Multiset (PrimeSpectrum R)<VAR>h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}<GOAL>span R {x} * span R {y} ≤ M
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx' : IsIntegral R x<GOAL>minpoly R x = minpoly R (powerBasis' hx').gen
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx' : IsIntegral R x<VAR>this : IsDomain (AdjoinRoot (minpoly R x))<GOAL>minpoly R x = minpoly R (powerBasis' hx').gen
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx' : IsIntegral R x<VAR>this✝ : IsDomain (AdjoinRoot (minpoly R x))<VAR>this : NoZeroSMulDivisors R (AdjoinRoot (minpoly R x))<GOAL>minpoly R x = minpoly R (powerBasis' hx').gen
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx' : IsIntegral R x<VAR>this✝ : IsDomain (AdjoinRoot (minpoly R x))<VAR>this : NoZeroSMulDivisors R (AdjoinRoot (minpoly R x))<GOAL>Irreducible (minpoly R x)
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : w ∈ closedBall z r<GOAL>(norm ∘ f) w = Function.const E ‖f z‖ w
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : dist z w ≤ r<GOAL>(norm ∘ f) w = Function.const E ‖f z‖ w
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>hw : dist z z ≤ r<GOAL>(norm ∘ f) z = Function.const E ‖f z‖ z
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : dist z w ≤ r<VAR>hne : z ≠ w<GOAL>(norm ∘ f) w = Function.const E ‖f z‖ w
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : dist z w ≤ r<VAR>hne : z ≠ w<VAR>e : ℂ → E := ⇑(lineMap z w)<GOAL>(norm ∘ f) w = Function.const E ‖f z‖ w
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : dist z w ≤ r<VAR>hne : z ≠ w<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<GOAL>(norm ∘ f) w = Function.const E ‖f z‖ w
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : dist z w ≤ r<VAR>hne : z ≠ w<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<VAR>hr : dist 1 0 = 1<GOAL>‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : E → F<VAR>z : E<VAR>r : ℝ<VAR>hd : DiffContOnCl ℂ f (ball z r)<VAR>hz : IsMaxOn (norm ∘ f) (ball z r) z<VAR>w : E<VAR>hw : dist z w ≤ r<VAR>hne : z ≠ w<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<VAR>hr : dist 1 0 = 1<VAR>hball : MapsTo e (ball 0 1) (ball z r)<GOAL>‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Ring α<VAR>i j i✝ j✝ : n<GOAL>(Equiv.toPEquiv (Equiv.swap i j)).toMatrix i✝ j✝ = (1 - (single i i).toMatrix - (single j j).toMatrix + (single i j).toMatrix + (single j i).toMatrix) i✝ j✝
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Ring α<VAR>i j i✝ j✝ : n<GOAL>(if j✝ ∈ some (if i✝ = i then j else if i✝ = j then i else i✝) then 1 else 0) = ((((if i✝ = j✝ then 1 else 0) - if j✝ ∈ if i✝ = i then some i else none then 1 else 0) - if j✝ ∈ if i✝ = j then some j else none then 1 else 0) + if j✝ ∈ if i✝ = i then some j else none then 1 else 0) + if j✝ ∈ if i✝ = j then some i else none then 1 else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b c d : α<VAR>h : a * b ~ᵤ c * d<VAR>h₁ : a ~ᵤ c<VAR>ha : a ≠ 0<VAR>u : αˣ<VAR>hu : a * b * ↑u = c * d<VAR>v : αˣ<VAR>hv : c * ↑v = a<GOAL>a * (b * ↑(u * v)) = a * d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b c d : α<VAR>h : a * b ~ᵤ c * d<VAR>h₁ : a ~ᵤ c<VAR>ha : a ≠ 0<VAR>u : αˣ<VAR>hu : a * b * ↑u = c * d<VAR>v : αˣ<VAR>hv : c * ↑v = a<GOAL>c * ↑v * (b * ↑(u * v)) = ↑v * (a * b * ↑u)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : ℕ<VAR>x y : E<GOAL>inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>r : ℕ<VAR>x y : E<GOAL>inner_ 𝕜 (↑r • x) y = ↑r * inner_ 𝕜 x y
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.reverse.next x ⋯ = l.prev x hx
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>h : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l = l.reverse.reverse
<VAR>a b : Ordinal.{u}<VAR>a0 : a ≠ 0<VAR>h : b.IsLimit<GOAL>a ^ b = b.bsup fun c x => a ^ c
<VAR>a b : Ordinal.{u}<VAR>a0 : a ≠ 0<VAR>h : b.IsLimit<GOAL>(b.limitRecOn 1 (fun x IH => IH * a) fun b x => b.bsup) = b.bsup fun c x => c.limitRecOn 1 (fun x IH => IH * a) fun b x => b.bsup
<VAR>m✝ n : ℕ<VAR>x✝ : Even n<VAR>m : ℕ<VAR>hm : n = m + m<GOAL>n % 2 = 0
<VAR>m n : ℕ<VAR>h : n % 2 = 0<GOAL>n % 2 + 2 * (n / 2) = n / 2 + n / 2
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>⨆ x, T.rayleighQuotient ↑x = ⨆ x, T.rayleighQuotient ↑x
<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>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>(fderivWithin ℝ f s a) 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>hy : y ∈ posTangentConeAt s a<VAR>hy' : -y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>0 y = 0
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>p : Type u_6<VAR>S : Type u_7<VAR>R : Type u_8<VAR>m' : l → Type u_9<VAR>n' : l → Type u_10<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace R<VAR>A : X → Matrix n l R<VAR>B : X → Matrix n m R<VAR>C : X → Matrix p l R<VAR>D : X → Matrix p m R<VAR>hA : Continuous A<VAR>hB : Continuous B<VAR>hC : Continuous C<VAR>hD : Continuous D<GOAL>∀ (i : n ⊕ p) (j : l ⊕ m), Continuous fun a => fromBlocks (A a) (B a) (C a) (D a) i j
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>UniformSpace.toTopologicalSpace ≤ WeakDual.instTopologicalSpace
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<GOAL>WeakDual.instTopologicalSpace = TopologicalSpace.induced (fun x' => toWeakDual x') WeakDual.instTopologicalSpace
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : ℝ<VAR>f : ℕ → ℕ<VAR>hm : 1 < m<VAR>fi : ∀ (i : ℕ), i ≤ f i<GOAL>Summable fun i => 1 / m ^ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : ℝ<VAR>f : ℕ → ℕ<VAR>hm : 1 < m<VAR>fi : ∀ (i : ℕ), i ≤ f i<VAR>a : ℕ<GOAL>1 / m ^ f a ≤ (1 / m) ^ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : ℝ<VAR>f : ℕ → ℕ<VAR>hm : 1 < m<VAR>fi : ∀ (i : ℕ), i ≤ f i<VAR>a : ℕ<GOAL>1 / m ^ f a ≤ 1 / m ^ a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>p.divX.natDegree = p.natDegree - 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1
<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>inst✝¹ : T2Space M<VAR>a b : ℝ<VAR>inst✝ : BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<GOAL>Xor' (∃ T > 0, Periodic γ T) (Injective γ)
<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>inst✝¹ : T2Space M<VAR>a b : ℝ<VAR>inst✝ : BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<GOAL>(∃ T > 0, Periodic γ T) ↔ ¬Injective γ
<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>inst✝¹ : T2Space M<VAR>a b : ℝ<VAR>inst✝ : BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<GOAL>¬Injective γ → ∃ T > 0, Periodic γ T
<VAR>d : Nat<VAR>nz : d ≠ 0<GOAL>normalize 0 d nz = 0
<VAR>d : Nat<VAR>nz : d ≠ 0<GOAL>↑0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝³ : ConditionallyCompleteLinearOrder γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OpensMeasurableSpace γ<VAR>inst✝ : OrderClosedTopology γ<VAR>h : IdentDistrib f g μ ν<GOAL>essSup f μ = essSup g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝³ : ConditionallyCompleteLinearOrder γ<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : OpensMeasurableSpace γ<VAR>inst✝ : OrderClosedTopology γ<VAR>h : IdentDistrib f g μ ν<VAR>I : ∀ (a : γ), μ {x | a < f x} = ν {x | a < g x}<GOAL>essSup f μ = essSup g ν
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>M : Matroid α<GOAL>M ↾ M.E = M
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R I J X Y : Set α<VAR>M : Matroid α<GOAL>∀ I ⊆ (M ↾ M.E).E, (M ↾ M.E).Indep I ↔ M.Indep I
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b : G₀<VAR>p : G₀ → Prop<GOAL>(∃ u, p ↑u) ↔ ∃ x, x ≠ 0 ∧ p x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>F : Filter X<GOAL>(map f F).lift' closure = map f (F.lift' closure)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>F : Filter X<GOAL>F.lift' (closure ∘ image f) = F.lift' (image f ∘ closure)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f_closed : IsClosedMap f<VAR>f_cont : Continuous f<VAR>F : Filter X<VAR>s : Set X<GOAL>(closure ∘ image f) s = (image f ∘ closure) s
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₁ : γ₁<GOAL>inl c₁ ∈ sumLift₂ f g a b ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₁ : γ₁<GOAL>(∃ a₁ b₁ c₁_1, a = inl a₁ ∧ b = inl b₁ ∧ inl c₁ = inl c₁_1 ∧ c₁_1 ∈ f a₁ b₁) ↔ ∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f a₁ b₁
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₁ : γ₁<GOAL>¬∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ inl c₁ = inr c₂ ∧ c₂ ∈ g a₂ b₂
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>γ₁ : Type u_5<VAR>γ₂ : Type u_6<VAR>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₁ : γ₁<VAR>w✝¹ : α₂<VAR>w✝ : β₂<VAR>c₂ : γ₂<VAR>left✝¹ : a = inr w✝¹<VAR>left✝ : b = inr w✝<VAR>h : inl c₁ = inr c₂<VAR>right✝ : c₂ ∈ g w✝¹ w✝<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<VAR>s : e.source = univ<VAR>t : e.target = univ<GOAL>e = e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<VAR>s : e.source = univ<VAR>t : e.target = univ<VAR>x : α<GOAL>↑e x = ↑e' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<VAR>s : e.source = univ<VAR>t : e.target = univ<VAR>x : β<GOAL>↑e.symm x = ↑e'.symm x
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>h_two : p ≠ 2<VAR>h_three : p ≠ 3<GOAL>5 ≤ p
<VAR>n p : ℕ<VAR>hp : Prime p<VAR>h_two : p ≠ 2<VAR>h_three : p ≠ 3<VAR>h : p < 5<GOAL>False
<VAR>n p : ℕ<VAR>h : p < 5<GOAL>Prime p → p ≠ 2 → p ≠ 3 → False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n m : ℕ<GOAL>(trunc (n + 1) 1).coeff m = Polynomial.coeff 1 m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n m : ℕ<GOAL>(if m < n + 1 then if m = 0 then 1 else 0 else 0) = if m = 0 then 1 else 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : Field A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<GOAL>minpoly A 0 = X
<VAR>α : Type u_1<VAR>f : ℕ → ℝ≥0<VAR>k : ℕ<VAR>a : ℝ≥0<GOAL>HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
<VAR>α : Type u_1<VAR>f : ℕ → ℝ≥0<VAR>k : ℕ<VAR>a : ℝ≥0<GOAL>HasSum (fun n => ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
<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>h : DifferentiableWithinAt 𝕜 (fun y => -f y) s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : Semiring S<VAR>inst✝² : Semiring T<VAR>inst✝¹ : FunLike F R S<VAR>rcf : RingHomClass F R S<VAR>inst✝ : FunLike G T S<VAR>rcg : RingHomClass G T S<VAR>f : F<VAR>g : G<VAR>r : R<GOAL>r ∈ ker f ↔ f r = 0
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<VAR>hx : s.toFun i ≠ last s<GOAL>s.toFun i ∈ eraseLast s
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<VAR>hx : s.toFun i ≠ last s<VAR>hi : ↑i < (s.length - 1).succ<GOAL>s.toFun i ∈ eraseLast s
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>i : Fin (s.length + 1)<VAR>hx : s.toFun i ≠ last s<VAR>hi : ↑i < (s.length - 1).succ<GOAL>(eraseLast s).toFun ↑↑i.castSucc = s.toFun i
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<GOAL>0 ≤ f (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>fA : f ∈ candidates X Y<VAR>this : 0 ≤ 2 * f (x, y)<GOAL>0 ≤ f (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, f i • z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range (n + 1), f i • z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => f n • ∑ i ∈ Finset.range n.succ, z i + -∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => -∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => ∑ x ∈ Finset.range n, (f (x + 1) + -f x) • ∑ i ∈ Finset.range (x + 1), z i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Monotone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<VAR>hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b<VAR>n : ℕ<GOAL>‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|