ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D✝<VAR>inst✝⁶ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ ≤ C<VAR>Nfgu : ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D✝<VAR>inst✝⁶ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t✝ u : Set E<VAR>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ ≤ C<VAR>Nfgu : ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x‖ ≤ ↑n ! * C * D ^ n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<VAR>hs : IsIntegral R s<GOAL>minpoly R s = P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<VAR>hs : IsIntegral R s<GOAL>minpoly R s - P = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<VAR>hs : IsIntegral R s<VAR>hnz : ¬minpoly R s - P = 0<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<VAR>hs : IsIntegral R s<VAR>hnz : ¬minpoly R s - P = 0<GOAL>(minpoly R s - P).degree < (minpoly R s).degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<VAR>hs : IsIntegral R s<VAR>hnz : ¬minpoly R s - P = 0<GOAL>(minpoly R s).degree = P.degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>hP : (Polynomial.aeval s) P = 0<VAR>Pmin : ∀ (Q : R[X]), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree<VAR>hs : IsIntegral R s<VAR>hnz : ¬minpoly R s - P = 0<GOAL>(minpoly R s).leadingCoeff = P.leadingCoeff
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulWithZero α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosReflectLT α β<VAR>h : a • b < 0<VAR>hb : 0 ≤ b<GOAL>a • b < 0 • b
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>hf : f = HSub.hSub<VAR>ra : IsRat a na da<VAR>rb : IsRat b nb db<VAR>h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc<VAR>h₂ : da.mul db = k.mul dc<GOAL>IsRat (f a b) nc dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>hf : f = HSub.hSub<VAR>ra : IsRat a na da<VAR>rb : IsRat b nb db<VAR>h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc<VAR>h₂ : da.mul db = k.mul dc<GOAL>IsRat (a + -b) nc dc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>hf : f = HSub.hSub<VAR>ra : IsRat a na da<VAR>rb : IsRat b nb db<VAR>h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc<VAR>h₂ : da.mul db = k.mul dc<GOAL>(na.mul ↑db).add ((-nb).mul ↑da) = (↑k).mul nc
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>f : α → α → α<VAR>a b : α<VAR>na nb nc : ℤ<VAR>da db dc k : ℕ<VAR>hf : f = HSub.hSub<VAR>ra : IsRat a na da<VAR>rb : IsRat b nb db<VAR>h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc<VAR>h₂ : da.mul db = k.mul dc<GOAL>(na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>y : ℝ<GOAL>HasSum (fun n => ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>y : ℝ<GOAL>HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>μ : Measure ℝ<VAR>f : ℝ → E<VAR>hfi : Integrable f μ<VAR>y : ℝ<GOAL>HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ) in ⋃ n, Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>t : Set Y<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<GOAL>Unbounded (fun x x_1 => x < x_1) s ↔ ∀ (a : α), ∃ b ∈ s, 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>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<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_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>hd : HasDerivAt d d' x<GOAL>HasDerivAt (fun y => c y * d y) (c' * d x + c x * d') x
<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>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<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_2<VAR>𝔸 : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝔸<VAR>c d : 𝕜 → 𝔸<VAR>c' d' : 𝔸<VAR>u v : 𝕜 → 𝕜'<VAR>hc : HasDerivWithinAt c c' univ x<VAR>hd : HasDerivWithinAt d d' univ x<GOAL>HasDerivWithinAt (fun y => c y * d y) (c' * d x + c x * d') univ x
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Finite F<VAR>hF : ringChar F ≠ 2<GOAL>∃ a, ¬IsSquare a
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : Finite F<VAR>hF : ringChar F ≠ 2<VAR>h : ¬Function.Injective fun x => x * x<GOAL>∃ a, ¬IsSquare a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝¹ : SemilatticeSup M<VAR>inst✝ : OrderBot M<VAR>h : weightedTotalDegree w φ < n<GOAL>(weightedHomogeneousComponent w n) φ = 0
<VAR>R : Type u_1<VAR>inst✝¹⁹ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁸ : AddCommMonoid M<VAR>inst✝¹⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁴ : AddCommMonoid P<VAR>inst✝¹³ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹⁰ : AddCommGroup N'<VAR>inst✝⁹ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>R' : Type u_10<VAR>M'' : Type u_11<VAR>M₂'' : Type u_12<VAR>N'' : Type u_13<VAR>N₂'' : Type u_14<VAR>inst✝⁸ : CommSemiring R'<VAR>inst✝⁷ : AddCommMonoid M''<VAR>inst✝⁶ : AddCommMonoid M₂''<VAR>inst✝⁵ : AddCommMonoid N''<VAR>inst✝⁴ : AddCommMonoid N₂''<VAR>inst✝³ : Module R' M''<VAR>inst✝² : Module R' M₂''<VAR>inst✝¹ : Module R' N''<VAR>inst✝ : Module R' N₂''<VAR>n : ℕ<VAR>f : M'' [⋀^Fin n.succ]→ₗ[R'] N''<VAR>m : M''<VAR>v : Fin n → M''<VAR>i j : Fin n<VAR>hv : v i = v j<VAR>hij : i ≠ j<GOAL>Matrix.vecCons m v i.succ = Matrix.vecCons m v j.succ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m✝ n✝ : ℤ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>mn : m < n<GOAL>(a ^ n)⁻¹ < (a ^ m)⁻¹
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>u : R[X]ˣ<VAR>n : ℕ<GOAL>((↑u).coeff n)⁻¹ = (↑u⁻¹).coeff n
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Field R<VAR>p q : R[X]<VAR>u : R[X]ˣ<VAR>n : ℕ<GOAL>(1 / if n = 0 then (↑u).coeff 0 else 0) = if n = 0 then (↑u⁻¹).coeff 0 else 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>s c : ι → Set α<VAR>hc : ∀ (i : ι), (c i).Countable<VAR>h'c : ∀ (i : ι), s i ⊆ closure (c i)<GOAL>IsSeparable (⋃ i, s i)
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>s c : ι → Set α<VAR>hc : ∀ (i : ι), (c i).Countable<VAR>h'c : ∀ (i : ι), s i ⊆ closure (c i)<VAR>i : ι<GOAL>s i ⊆ closure (⋃ i, c i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 a<VAR>u : α<VAR>hu : a < u<GOAL>∃ u' ∈ Ioc a u, Ico a u' ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>s ∪ insert a t = insert a (s ∪ t)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l₁ l₂ : ι →₀ 𝕜<GOAL>⟪(Finsupp.total ι E 𝕜 v) l₁, (Finsupp.total ι E 𝕜 v) l₂⟫_𝕜 = l₂.sum fun i y => (starRingEnd 𝕜) (l₁ i) * y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}<VAR>hSc : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<GOAL>∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}<VAR>hSc : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>q : E →ₗ.[ℝ] ℝ<VAR>hqs : q ∈ S<VAR>hpq : p ≤ q<VAR>hq : ∀ z ∈ S, q ≤ z → z = q<GOAL>∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}<VAR>hSc : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>q : E →ₗ.[ℝ] ℝ<VAR>hqs : q ∈ S<VAR>hpq : p ≤ q<VAR>hq : ∀ z ∈ S, q ≤ z → z = q<GOAL>q.domain = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}<VAR>hSc : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>q : E →ₗ.[ℝ] ℝ<VAR>hqs : q ∈ S<VAR>hpq : p ≤ q<VAR>hq : q.domain ≠ ⊤<GOAL>∃ z ∈ S, q ≤ z ∧ z ≠ q
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}<VAR>hSc : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>q : E →ₗ.[ℝ] ℝ<VAR>hqs : q ∈ S<VAR>hpq : p ≤ q<VAR>hq : q.domain ≠ ⊤<VAR>hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s<GOAL>∃ z ∈ S, q ≤ z ∧ z ≠ q
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}<VAR>hSc : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>q : E →ₗ.[ℝ] ℝ<VAR>hqs : q ∈ S<VAR>hpq : p ≤ q<VAR>hq : q.domain ≠ ⊤<VAR>hqd : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>r : E →ₗ.[ℝ] ℝ<VAR>hqr : q < r<VAR>hr : ∀ (x : ↥r.domain), ↑x ∈ s → 0 ≤ ↑r x<GOAL>∃ z ∈ S, q ≤ z ∧ z ≠ q
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>A : Type u_3<VAR>inst✝¹⁶ : Category.{u_5, u_1} C<VAR>inst✝¹⁵ : HasZeroObject C<VAR>inst✝¹⁴ : HasShift C ℤ<VAR>inst✝¹³ : Preadditive C<VAR>inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹¹ : Pretriangulated C<VAR>inst✝¹⁰ : Category.{?u.52987, u_2} D<VAR>inst✝⁹ : HasZeroObject D<VAR>inst✝⁸ : HasShift D ℤ<VAR>inst✝⁷ : Preadditive D<VAR>inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive<VAR>inst✝⁵ : Pretriangulated D<VAR>inst✝⁴ : Category.{u_4, u_3} A<VAR>inst✝³ : Abelian A<VAR>F : C ⥤ A<VAR>inst✝² inst✝¹ : F.IsHomological<VAR>inst✝ : F.ShiftSequence ℤ<VAR>T T' : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>hT' : T' ∈ distinguishedTriangles<VAR>φ : T ⟶ T'<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>(F.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : NoMaxOrder α<VAR>hs : IsUpperSet s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ upperBounds s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : NoMaxOrder α<VAR>hs : IsUpperSet s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ upperBounds s<VAR>c : α<VAR>hc : b < c<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<GOAL>(unitization s).range = Algebra.adjoin R ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<GOAL>Algebra.adjoin R ↑(NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype s)) = Algebra.adjoin R ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : SetLike S A<VAR>hSA : NonUnitalSubsemiringClass S A<VAR>hSRA : SMulMemClass S R A<VAR>s : S<GOAL>Algebra.adjoin R {x | x ∈ s} = Algebra.adjoin R ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ ν : Kernel α β<VAR>hν : IsFiniteKernel ν<VAR>hκν : κ ≤ ν<GOAL>IsFiniteKernel κ
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y : α i.succ<VAR>z : α 0<VAR>P : ((i : Fin n.succ) → α i) → Sort v<VAR>h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (cons x₀ x)<VAR>x₀ : α 0<VAR>x : (i : Fin n) → α i.succ<GOAL>consCases h (cons x₀ x) = h x₀ x
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x✝ : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y : α i.succ<VAR>z : α 0<VAR>P : ((i : Fin n.succ) → α i) → Sort v<VAR>h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (cons x₀ x)<VAR>x₀ : α 0<VAR>x : (i : Fin n) → α i.succ<GOAL>h (cons x₀ x 0) (tail (cons x₀ x)) = h x₀ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<VAR>n : ℕ<GOAL>dist (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : SeminormedAddCommGroup α<VAR>r C : ℝ<VAR>f : ℕ → α<VAR>hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n<VAR>n : ℕ<GOAL>‖f n‖ ≤ C * r ^ n
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>-x ≈ 0 ↔ x ≈ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<VAR>n : ℕ<GOAL>rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G✝<VAR>inst✝⁵ : Inv G✝<VAR>inst✝⁴ : ContinuousInv G✝<VAR>G : Type u_1<VAR>inst✝³ : DivInvMonoid G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : ContinuousMul G<VAR>inst✝ : ContinuousInv G<VAR>x y : G<VAR>h : x ⤳ y<VAR>n : ℕ<GOAL>(x ^ Int.ofNat n) ⤳ (y ^ Int.ofNat n)
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G✝<VAR>inst✝⁵ : Inv G✝<VAR>inst✝⁴ : ContinuousInv G✝<VAR>G : Type u_1<VAR>inst✝³ : DivInvMonoid G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : ContinuousMul G<VAR>inst✝ : ContinuousInv G<VAR>x y : G<VAR>h : x ⤳ y<VAR>n : ℕ<GOAL>(x ^ Int.negSucc n) ⤳ (y ^ Int.negSucc n)
<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 : HasFDerivAtFilter f f' x L<VAR>c : F<GOAL>HasFDerivAtFilter (fun x => c - f x) (-f') x L
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s₁ s₂ : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) = (fromLocalizedModule S f) (LocalizedModule.mk m s₁)
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m.gcd (n - m) = m.gcd n
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : M →ₗ[S] M<VAR>h : IsProj m f<VAR>x : ↥m<GOAL>↑(h.codRestrict ↑x) = ↑x
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : M →ₗ[S] M<VAR>h : IsProj m f<VAR>x : ↥m<GOAL>f ↑x = ↑x
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<GOAL>(coeff R m) (φ * (monomial R n) a) = if n ≤ m then (coeff R (m - n)) φ * a else 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s t r : Set α<VAR>h : Disjoint s t<GOAL>↑(Sum.inl ⁻¹' (⇑(sumSet h) ⁻¹' r)) = r ∩ s