ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≤ 0<VAR>x✝ : E<GOAL>x✝ ∈ p.ball x r ↔ x✝ ∈ ∅
<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✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≤ 0<VAR>x✝ : E<GOAL>r ≤ p (x✝ - x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u<GOAL>∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{max (u + 1) v}<VAR>h : c < univ.{u, v}<GOAL>∃ c', c = lift.{max (u + 1) v, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{max (u + 1) v}<VAR>h : c < univ.{u, v}<VAR>a : Cardinal.{u + 1}<VAR>e : lift.{v, u + 1} a = c<VAR>h' : a < #Ordinal.{u}<GOAL>∃ c', c = lift.{max (u + 1) v, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{max (u + 1) v}<VAR>h : c < univ.{u, v}<VAR>a : Cardinal.{u + 1}<VAR>e : lift.{v, u + 1} a = c<VAR>h' : a < univ.{u, u + 1}<GOAL>∃ c', c = lift.{max (u + 1) v, u} c'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{max (u + 1) v}<VAR>h : c < univ.{u, v}<VAR>c' : Cardinal.{u}<VAR>e : lift.{v, u + 1} (lift.{u + 1, u} c') = c<VAR>h' : lift.{u + 1, u} c' < univ.{u, u + 1}<GOAL>∃ c', c = lift.{max (u + 1) v, u} c'
<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✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x<GOAL>∫ (y : ℝ) in a..b, φ y ≤ g b - g a
<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✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x<GOAL>-(g b - g a) ≤ -∫ (y : ℝ) in a..b, φ y
<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✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x<GOAL>-(g b - g a) = -g b - -g a
<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✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, φ x ≤ g' x<GOAL>-∫ (y : ℝ) in a..b, φ y = ∫ (y : ℝ) in a..b, (-φ) y
<VAR>α : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>β : Type u_1<VAR>inst✝ : DecidableEq β<VAR>l : List α<VAR>f : α → β<VAR>x : α<GOAL>count x l ≤ count (f x) (map f l)
<VAR>α : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>β : Type u_1<VAR>inst✝ : DecidableEq β<VAR>l : List α<VAR>f : α → β<VAR>x : α<GOAL>countP (fun x_1 => x_1 == x) l ≤ countP ((fun x_1 => x_1 == f x) ∘ f) l
<VAR>α : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>β : Type u_1<VAR>inst✝ : DecidableEq β<VAR>l : List α<VAR>f : α → β<VAR>x : α<GOAL>∀ (x_1 : α), x_1 ∈ l → (x_1 == x) = true → ((fun x_2 => x_2 == f x) ∘ f) x_1 = true
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<GOAL>↑n < find P ↔ ∀ m ≤ n, ¬P m
<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>n : ℕ<GOAL>↑n < find P → ∀ m ≤ n, ¬P m
<VAR>m n : ℕ<GOAL>(m + n).gcd m = n.gcd m
<VAR>α : Type u_1<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(partialSups f) n ≤ x✝ ↔ ⨆ i, f ↑i ≤ x✝
<VAR>α : Type u_1<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(∀ k ≤ n, f k ≤ x✝) ↔ ∀ i ∈ Set.Iic n, f i ≤ x✝
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>cosKernel (-a) x = cosKernel a x
<VAR>x a' : ℝ<GOAL>cosKernel (-↑a') x = cosKernel (↑a') x
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : Ideal.PrimePair P<GOAL>IsIdeal (↑IF.F)ᶜ
<VAR>P : Type u_1<VAR>inst✝ : Preorder P<VAR>IF : Ideal.PrimePair P<GOAL>IsIdeal ↑IF.I
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>s : Stream' α<VAR>k n : ℕ<VAR>h : k + 1 < n + 1<GOAL>(take (n + 1) s).get? (k + 1) = some (s.get (k + 1))
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝⁵ : IsTrans α r<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : Nonempty γ<VAR>f✝ : γ → α<VAR>inst✝³ : Finite β<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : IsDirected α fun x x_1 => x ≤ x_1<VAR>f : β → α<GOAL>BddAbove (Set.range f)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝⁵ : IsTrans α r<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : Nonempty γ<VAR>f✝ : γ → α<VAR>inst✝³ : Finite β<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : IsDirected α fun x x_1 => x ≤ x_1<VAR>f : β → α<VAR>M : α<VAR>hM : ∀ (i : β), f i ≤ M<GOAL>BddAbove (Set.range f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hs : NullMeasurableSet s μ<VAR>hd : AEDisjoint μ s t<GOAL>μ (s ∪ t) = μ 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>x y : F<GOAL>‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2
<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>x y : F<VAR>h : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2<GOAL>‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2
<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 p : R[X]<VAR>hq : q.Monic<GOAL>p %ₘ q = p %ₘ (q * C q.leadingCoeff⁻¹)
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : NonUnitalNonAssocSemiring A<VAR>inst✝¹⁰ : Module R A<VAR>inst✝⁹ : Star A<VAR>inst✝⁸ : NonUnitalNonAssocSemiring B<VAR>inst✝⁷ : Module R B<VAR>inst✝⁶ : Star B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : Module R C<VAR>inst✝³ : Star C<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>φ : F<VAR>x✝ : B<GOAL>x✝ ∈ ↑(NonUnitalStarAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : NonUnitalNonAssocSemiring A<VAR>inst✝¹⁰ : Module R A<VAR>inst✝⁹ : Star A<VAR>inst✝⁸ : NonUnitalNonAssocSemiring B<VAR>inst✝⁷ : Module R B<VAR>inst✝⁶ : Star B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : Module R C<VAR>inst✝³ : Star C<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>φ : F<VAR>x✝ : B<GOAL>(∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ
<VAR>x y : ℝ<VAR>a b : Cauchy abs<GOAL>{ cauchy := a } = { cauchy := b } ↔ { cauchy := a }.cauchy = { cauchy := b }.cauchy
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ c✝ a b c : α<GOAL>max (a / b) (a / c) = a / min b c
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>op : α → α → α<VAR>ha : Std.Associative op<VAR>hc : Std.Commutative op<VAR>a : α<VAR>l : List α<VAR>a₁ a₂ : α<GOAL>op ((a :: l) <*> a₁) a₂ = op a₁ (foldr (fun x x_1 => op x x_1) a₂ (a :: l))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>op : α → α → α<VAR>ha : Std.Associative op<VAR>hc : Std.Commutative op<VAR>a : α<VAR>l : List α<VAR>a₁ a₂ : α<GOAL>op a₁ (op (l <*> a) a₂) = op a₁ (op a (foldr (fun x x_1 => op x x_1) a₂ l))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Icc a b = Icc (b / c) (a / c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r' r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>r'0 : 0 < ↑r'<VAR>h : ↑r' < r<GOAL>(fun y => f y.1 - f y.2 - (p 1) fun x => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r✝ r'✝ r : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f p x r<VAR>r' : ℝ≥0<VAR>r'0 : 0 < ↑r'<VAR>h : ↑r' < r<GOAL>𝓝 (x, x) ≤ 𝓟 (EMetric.ball (x, x) ↑r')
<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>p : Prop<VAR>u v : V<VAR>h : G.Reachable u v<VAR>hp : G.Path u v → p<GOAL>p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>x y : ℝ<VAR>hx : 0 ≤ x<GOAL>↑(x.toNNReal * ‖y‖₊) = ↑‖x * y‖₊
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>x : 𝕎 R<VAR>i : ℕ<GOAL>(x * ↑p).coeff (i + 1) = x.coeff i ^ p
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<VAR>hν : IsProjectiveLimit ν P<GOAL>μ = ν
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<VAR>hν : IsProjectiveLimit ν P<VAR>this : IsFiniteMeasure μ<GOAL>μ = ν
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<VAR>hν : IsProjectiveLimit ν P<VAR>this : IsFiniteMeasure μ<VAR>s : Set ((i : ι) → α i)<VAR>hs : s ∈ measurableCylinders α<GOAL>μ s = ν s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>μ ν : Measure ((i : ι) → α i)<VAR>inst✝ : ∀ (i : Finset ι), IsFiniteMeasure (P i)<VAR>hμ : IsProjectiveLimit μ P<VAR>hν : IsProjectiveLimit ν P<VAR>this : IsFiniteMeasure μ<VAR>I : Finset ι<VAR>S : Set ((i : { x // x ∈ I }) → α ↑i)<VAR>hS : MeasurableSet S<VAR>hs : cylinder I S ∈ measurableCylinders α<GOAL>μ (cylinder I S) = ν (cylinder I S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<GOAL>p.radius ≤ (f.compFormalMultilinearSeries p).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius<GOAL>↑r ≤ (f.compFormalMultilinearSeries p).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius<GOAL>(fun n => ‖f.compFormalMultilinearSeries p n‖ * ↑r ^ n) =O[atTop] fun x => 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius<GOAL>(fun n => ‖f.compFormalMultilinearSeries p n‖ * ↑r ^ n) =O[atTop] fun n => ‖p n‖ * ↑r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius<GOAL>IsBigOWith ‖f‖ atTop (fun n => ‖f.compFormalMultilinearSeries p n‖) fun n => ‖p n‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p✝ : FormalMultilinearSeries 𝕜 E F<VAR>r✝ : ℝ≥0<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>f : F →L[𝕜] G<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius<VAR>n : ℕ<GOAL>‖‖f.compFormalMultilinearSeries p n‖‖ ≤ ‖f‖ * ‖‖p n‖‖
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>s₁ s₂ : Stream' α<VAR>x✝ : a ∈ s₂<VAR>n : ℕ<VAR>h : (fun b => a = b) (s₂.get n)<GOAL>(fun b => a = b) ((s₁ ⋈ s₂).get (2 * n + 1))
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>x : M<VAR>N : Submodule R M := ⨅ i, I ^ i • ⊤<GOAL>x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>x : M<VAR>N : Submodule R M := ⨅ i, I ^ i • ⊤<VAR>hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N<GOAL>x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<VAR>y : Set β<GOAL>minimals r (⇑f ⁻¹' y) = ⇑f ⁻¹' minimals s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<VAR>y : Set β<GOAL>y = y ∩ range ⇑f.toRelEmbedding
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<VAR>inst✝¹⁰ : Semiring R₃<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p✝ p' : Submodule R M<VAR>q q' : Submodule R₂ M₂<VAR>x : M<VAR>F : Type u_9<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>σ : R →+* R<VAR>inst✝ : RingHomSurjective σ<VAR>ι : Sort u_10<VAR>f : M →ₛₗ[σ] M<VAR>p : ι → Submodule R M<VAR>hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i<VAR>this : ∀ (i : ι), map f (p i) ≤ p i<GOAL>map f (iInf p) ≤ iInf p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : C<VAR>α : X ≅ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : α.inv ≫ f = g<GOAL>f = α.hom ≫ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : IsBigOWith c l f₁ f₂<VAR>hc : c < 1<VAR>x : α<VAR>hx : x ∈ {x | (fun x => ‖f₁ x‖ ≤ c * ‖f₂ x‖) x}<GOAL>x ∈ {x | (fun x => ‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖) x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : IsBigOWith c l f₁ f₂<VAR>hc : c < 1<VAR>x : α<VAR>hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖<GOAL>‖f₂ x‖ ≤ 1 / (1 - c) * ‖f₂ x - f₁ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : IsBigOWith c l f₁ f₂<VAR>hc : c < 1<VAR>x : α<VAR>hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖<GOAL>‖f₂ x‖ - c * ‖f₂ x‖ ≤ ‖f₂ x - f₁ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : IsBigOWith c l f₁ f₂<VAR>hc : c < 1<VAR>x : α<VAR>hx : ‖f₁ x‖ ≤ c * ‖f₂ x‖<GOAL>0 < 1 - c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>x y : Ordinal.{u_4}<GOAL>x * y % x = 0
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>x : E<VAR>hx : x ∈ s<GOAL>p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>x : E<VAR>hx : x ∈ s<GOAL>p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (p x 0).uncurry0