ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hγ : IsIntegralCurveOn γ v univ<VAR>dt : ℝ<GOAL>IsIntegralCurveOn (γ ∘ fun x => x + dt) v univ
<VAR>p q : ℚ<VAR>hp : 0 ≤ p<GOAL>q.toNNRat ≤ p.toNNRat ↔ q ≤ p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>f : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖(h.comp f) x‖ ≤ ‖h‖ * ‖f‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>f : E →SL[σ₁₂] F<VAR>x : E<GOAL>‖(h.comp f) x‖ ≤ ‖h‖ * (‖f‖ * ‖x‖)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<GOAL>(comap C P).IsMaximal
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<GOAL>(comap ((Quotient.mk P).comp C) ⊥).IsMaximal
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsJacobson R<VAR>P : Ideal R[X]<VAR>hP : P.IsMaximal<VAR>this : ⊥.IsMaximal<GOAL>(comap ((Quotient.mk P).comp C) ⊥).IsMaximal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s t : Set α<VAR>f : β → α<VAR>hf : Surjective f<VAR>eq : f ⁻¹' s = f ⁻¹' t<GOAL>s = t
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>s t : Associates α<VAR>d : Associates α<VAR>eq : t = s * d<GOAL>s.factors ≤ t.factors
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>s t : Associates α<VAR>d : Associates α<VAR>eq : t = s * d<GOAL>s.factors ≤ s.factors + d.factors
<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 : 𝓝[s \ {x}] x = ⊥<GOAL>fderivWithin 𝕜 f s x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : ball 0 r ⊆ s<GOAL>r * gauge s x ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : ball 0 r ⊆ s<VAR>hr : r ≤ 0<GOAL>r * gauge s x ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : ball 0 r ⊆ s<VAR>hr : 0 < r<GOAL>r * gauge s x ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : ball 0 r ⊆ s<VAR>hr : 0 < r<GOAL>gauge s x ≤ gauge (ball 0 r) x
<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✝ : Semiring R<VAR>k : ℕ<VAR>p : R[X]<VAR>m : ℕ<GOAL>((⇑derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>s : Set E<VAR>hs : Orthonormal 𝕜 Subtype.val<VAR>w : Set E<VAR>hws : w ⊇ s<VAR>hw_ortho : Orthonormal 𝕜 Subtype.val<VAR>hw_max : ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w<GOAL>(span 𝕜 (Set.range Subtype.val))ᗮ = ⊥
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x ≤ y<GOAL>deriv f x ≤ deriv f y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<VAR>x : ℝ<VAR>hx hy : x ∈ S<VAR>hxy : x ≤ x<GOAL>deriv f x ≤ deriv f x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : ∀ x ∈ S, DifferentiableAt ℝ f x<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x ≤ y<VAR>hxy' : x < y<GOAL>deriv f x ≤ deriv f y
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ioi a = Ioo ↑a ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>this : Countable ↑s<GOAL>{t | t.Finite ∧ t ⊆ s}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>this : Countable ↑s<GOAL>{t | t.Finite ∧ t ⊆ s} ⊆ range fun t => Subtype.val '' ↑t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>this : Countable ↑s<VAR>t : Set ↑s<VAR>ht : (Subtype.val '' t).Finite<GOAL>Subtype.val '' t ∈ range fun t => Subtype.val '' ↑t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>hs : s.Countable<VAR>this : Countable ↑s<VAR>t : Finset ↑s<VAR>ht : (Subtype.val '' ↑t).Finite<GOAL>Subtype.val '' ↑t ∈ range fun t => Subtype.val '' ↑t
<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>h : 0 < b<GOAL>a * b⁻¹ ≤ c ↔ a ≤ b * c
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>s t : (forget C).obj ((stalkFunctor C x).obj F)<VAR>hst : ((stalkFunctor C x).map f) s = ((stalkFunctor C x).map f) t<GOAL>s = t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>t : (forget C).obj ((stalkFunctor C x).obj F)<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>hst : ((stalkFunctor C x).map f) ((F.germ ⟨x, hxU₁⟩) s) = ((stalkFunctor C x).map f) t<GOAL>(F.germ ⟨x, hxU₁⟩) s = t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>U₂ : Opens ↑X<VAR>hxU₂ : x ∈ U₂<VAR>t : (forget C).obj (F.obj (op U₂))<VAR>hst : ((stalkFunctor C x).map f) ((F.germ ⟨x, hxU₁⟩) s) = ((stalkFunctor C x).map f) ((F.germ ⟨x, hxU₂⟩) t)<GOAL>(F.germ ⟨x, hxU₁⟩) s = (F.germ ⟨x, hxU₂⟩) t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>U₂ : Opens ↑X<VAR>hxU₂ : x ∈ U₂<VAR>t : (forget C).obj (F.obj (op U₂))<VAR>hst : (G.germ ⟨x, hxU₁⟩) ((f.app (op U₁)) s) = (G.germ ⟨x, hxU₂⟩) ((f.app (op U₂)) t)<GOAL>(F.germ ⟨x, hxU₁⟩) s = (F.germ ⟨x, hxU₂⟩) t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>U₂ : Opens ↑X<VAR>hxU₂ : x ∈ U₂<VAR>t : (forget C).obj (F.obj (op U₂))<VAR>hst : (G.germ ⟨x, hxU₁⟩) ((f.app (op U₁)) s) = (G.germ ⟨x, hxU₂⟩) ((f.app (op U₂)) t)<VAR>W : Opens ↑X<VAR>hxW : x ∈ W<VAR>iWU₁ : W ⟶ U₁<VAR>iWU₂ : W ⟶ U₂<VAR>heq : (G.map iWU₁.op) ((f.app (op U₁)) s) = (G.map iWU₂.op) ((f.app (op U₂)) t)<GOAL>(F.germ ⟨x, hxU₁⟩) s = (F.germ ⟨x, hxU₂⟩) t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>U₂ : Opens ↑X<VAR>hxU₂ : x ∈ U₂<VAR>t : (forget C).obj (F.obj (op U₂))<VAR>hst : (G.germ ⟨x, hxU₁⟩) ((f.app (op U₁)) s) = (G.germ ⟨x, hxU₂⟩) ((f.app (op U₂)) t)<VAR>W : Opens ↑X<VAR>hxW : x ∈ W<VAR>iWU₁ : W ⟶ U₁<VAR>iWU₂ : W ⟶ U₂<VAR>heq : (f.app (op W)) ((F.map iWU₁.op) s) = (f.app (op W)) ((F.map iWU₂.op) t)<GOAL>(F.germ ⟨x, hxU₁⟩) s = (F.germ ⟨x, hxU₂⟩) t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>U₂ : Opens ↑X<VAR>hxU₂ : x ∈ U₂<VAR>t : (forget C).obj (F.obj (op U₂))<VAR>hst : (G.germ ⟨x, hxU₁⟩) ((f.app (op U₁)) s) = (G.germ ⟨x, hxU₂⟩) ((f.app (op U₂)) t)<VAR>W : Opens ↑X<VAR>hxW : x ∈ W<VAR>iWU₁ : W ⟶ U₁<VAR>iWU₂ : W ⟶ U₂<VAR>heq : (F.map iWU₁.op) s = (F.map iWU₂.op) t<VAR>e_1✝ : (forget C).obj ((stalkFunctor C x).obj F) = (forget C).obj (F.stalk ↑⟨x, hxW⟩)<GOAL>(F.germ ⟨x, hxU₁⟩) s = (F.germ ⟨x, hxW⟩) ((F.map iWU₁.op) s)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F G : Presheaf C X<VAR>f : F ⟶ G<VAR>h : ∀ (U : Opens ↑X), Function.Injective ⇑(f.app (op U))<VAR>x : ↑X<VAR>U₁ : Opens ↑X<VAR>hxU₁ : x ∈ U₁<VAR>s : (forget C).obj (F.obj (op U₁))<VAR>U₂ : Opens ↑X<VAR>hxU₂ : x ∈ U₂<VAR>t : (forget C).obj (F.obj (op U₂))<VAR>hst : (G.germ ⟨x, hxU₁⟩) ((f.app (op U₁)) s) = (G.germ ⟨x, hxU₂⟩) ((f.app (op U₂)) t)<VAR>W : Opens ↑X<VAR>hxW : x ∈ W<VAR>iWU₁ : W ⟶ U₁<VAR>iWU₂ : W ⟶ U₂<VAR>heq : (F.map iWU₁.op) s = (F.map iWU₂.op) t<VAR>e_1✝ : (forget C).obj ((stalkFunctor C x).obj F) = (forget C).obj (F.stalk ↑⟨x, hxW⟩)<GOAL>(F.germ ⟨x, hxU₂⟩) t = (F.germ ⟨x, hxW⟩) ((F.map iWU₂.op) t)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>c : F<GOAL>Function.HasTemperateGrowth (fderiv ℝ fun x => c)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>dual A K I * I = dual A K 1
<VAR>x y : EReal<GOAL>y ≤ x ↔ ∀ (z : ℝ), x < ↑z → y ≤ ↑z
<VAR>x y : EReal<GOAL>(∀ (z : ℝ), x < ↑z → y ≤ ↑z) → y ≤ x
<VAR>x : ℂ<VAR>n : ℤ<VAR>y : ℂ<GOAL>x ^ (↑n * y) = (x ^ y) ^ n
<VAR>n : ℤ<VAR>y : ℂ<GOAL>0 ^ (↑n * y) = (0 ^ y) ^ n
<VAR>x : ℂ<VAR>n : ℤ<VAR>y : ℂ<VAR>hx : x ≠ 0<GOAL>x ^ (↑n * y) = (x ^ y) ^ n
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>hs : s.Nonempty<GOAL>centroid R s id ∈ (convexHull R) ↑s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>hs : s.Nonempty<GOAL>s.centerMass (centroidWeights R s) id ∈ (convexHull R) ↑s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>hs : s.Nonempty<GOAL>∀ i ∈ s, 0 ≤ centroidWeights R s i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>hs : s.Nonempty<GOAL>0 < ∑ i ∈ s, centroidWeights R s i
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>M₀ : Type u_5<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : FunLike F ℚ M₀<VAR>inst✝ : MonoidWithZeroHomClass F ℚ M₀<VAR>f g : F<VAR>h : ∀ (m : ℤ), f ↑m = g ↑m<VAR>r : ℚ<GOAL>f r = g r
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>M₀ : Type u_5<VAR>inst✝² : MonoidWithZero M₀<VAR>inst✝¹ : FunLike F ℚ M₀<VAR>inst✝ : MonoidWithZeroHomClass F ℚ M₀<VAR>f g : F<VAR>h : ∀ (m : ℤ), f ↑m = g ↑m<VAR>r : ℚ<GOAL>f ↑↑r.den = g ↑↑r.den
<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 × Y)<GOAL>(∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ (a : X) (b : Y), (a, b) ∈ s → ∃ u v, IsOpen u ∧ IsOpen v ∧ a ∈ u ∧ b ∈ v ∧ u ×ˢ v ⊆ s
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>c : KernelFork S.g<VAR>hc : IsLimit c<GOAL>(ofIsLimitKernelFork S hf c hc).g' = S.g
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>h : AEDisjoint μ s t<VAR>ht : NullMeasurableSet t μ<GOAL>μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>AntitoneOn (fun x => x⁻¹) (Set.Icc a b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<VAR>x✝ : α<GOAL>x✝ = x✝ - 0
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>LinearMap.range (map f) = Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>Submodule.span R (Set.range (⇑(map f) ∘ ⇑(tprod R))) = Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<GOAL>Set.range (⇑(map f) ∘ ⇑(tprod R)) = {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁹ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>E : Type u_9<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : Module R E<VAR>F : Type u_10<VAR>inst✝⁴ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝³ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝² : (i : ι) → Module R (t i)<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>x : ⨂[R] (i : ι), t i<GOAL>x ∈ Set.range (⇑(map f) ∘ ⇑(tprod R)) ↔ x ∈ {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsSeparatedMap f<VAR>g : A → Y<GOAL>IsSeparatedMap snd
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsClosed (Function.pullbackDiagonal f)<VAR>g : A → Y<GOAL>IsClosed (Function.pullbackDiagonal snd)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsClosed (Function.pullbackDiagonal f)<VAR>g : A → Y<GOAL>IsClosed (Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>h : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>Prime (hζ.toInteger - 1)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>h : IsCyclotomicExtension {p} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑p<GOAL>IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>z : ℝ≥0<GOAL>nndist z 0 = z
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝³ : LinearOrder n<VAR>inst✝² : IsWellOrder n fun x x_1 => x < x_1<VAR>inst✝¹ : LocallyFiniteOrderBot n<VAR>S : Matrix n n 𝕜<VAR>inst✝ : Fintype n<VAR>hS : S.PosDef<VAR>i j : n<VAR>hij : i < j<GOAL>lowerInv hS i j = 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>f : ι → Set α<GOAL>thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i)
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<VAR>hr : Irrational r<GOAL>{x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁷ : OrderedRing 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : Nontrivial 𝕜<VAR>inst✝ : DenselyOrdered 𝕜<VAR>x z : E<VAR>x✝ : z ∈ openSegment 𝕜 x x<VAR>a b : 𝕜<VAR>left✝¹ : 0 < a<VAR>left✝ : 0 < b<VAR>hab : a + b = 1<VAR>hz : a • x + b • x = z<GOAL>z ∈ {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁷ : OrderedRing 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : Nontrivial 𝕜<VAR>inst✝ : DenselyOrdered 𝕜<VAR>x z : E<VAR>h : z = x<GOAL>z ∈ openSegment 𝕜 x x