ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : InfConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>ha : IsGLB (range f) a<GOAL>Tendsto f atBot (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>s : Finset α<VAR>a : α<GOAL>(image f s).erase (f a) ⊆ image f (s.erase a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>s : Finset α<VAR>a : α<GOAL>∀ ⦃x : β⦄, x ≠ f a → ∀ x_1 ∈ s, f x_1 = x → ∃ a_4, (a_4 ≠ a ∧ a_4 ∈ s) ∧ f a_4 = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>s : Finset α<VAR>a x : α<VAR>hx : x ∈ s<VAR>hb : f x ≠ f a<GOAL>∃ a_1, (a_1 ≠ a ∧ a_1 ∈ s) ∧ f a_1 = f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : R1Space X<VAR>x✝ y : X<VAR>inst✝ : WeaklyLocallyCompactSpace X<VAR>x : X<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Mf : Monotone f<VAR>bdd : autoParam (BddAbove (range g)) _auto✝<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Mf : Monotone f<VAR>bdd : autoParam (BddAbove (range g)) _auto✝<GOAL>sSup (range (f ∘ g)) = sSup (range fun i => f (g i))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<GOAL>↑((orthogonalProjection K) v) = v ↔ v ∈ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>h : ↑((orthogonalProjection K) v) = v<GOAL>v ∈ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>h : v ∈ K<GOAL>∀ w ∈ K, ⟪v - v, w⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>x y : α<GOAL>‖(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>x y : α<GOAL>‖(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>s✝ t : Set α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>H : (↑s).Nontrivial ↔ s.offDiag.Nonempty<GOAL>(↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.138641, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.138648, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.138641, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.138648, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') ↔ Nonempty (IsColimit (Cocone.whisker e.inverse c'))
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.138641, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.138648, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>(∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Cocone.whisker e.functor c).ι.app j)) ↔ ∀ (j : K), IsPullback ((Cocone.whisker e.inverse c').ι.app j) ((whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom).app j) f (c.ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K✝ : Type u_1<VAR>inst✝² : Category.{?u.138641, u_1} K✝<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.138648, u_2} D<VAR>K : Type u_3<VAR>inst✝ : Category.{u_4, u_3} K<VAR>e : J ≌ K<VAR>F : K ⥤ C<VAR>c : Cocone F<VAR>hc : IsVanKampenColimit c<VAR>F' : J ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ e.functor ⋙ F<VAR>f : c'.pt ⟶ (Cocone.whisker e.functor c).pt<VAR>e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>(whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) ≫ c.ι = (Cocone.whisker e.inverse c').ι ≫ (Functor.const K).map f
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x.2 * x.1 = n ∧ ¬n = 0 ↔ x ∈ n.divisorsAntidiagonal
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : Cᵒᵖ ⥤ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>(J.isoSheafify hP).inv = J.sheafifyLift (𝟙 P) hP
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P : Cᵒᵖ ⥤ D<VAR>hP : Presheaf.IsSheaf J P<GOAL>J.toSheafify P ≫ (J.isoSheafify hP).inv = 𝟙 P
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : OplaxNatTrans F G<VAR>θ : OplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g : a ⟶ b<VAR>h : b ⟶ c<GOAL>f ◁ θ.naturality (g ≫ h) ≫ f ◁ θ.app a ◁ H.mapComp g h = f ◁ G.mapComp g h ▷ θ.app c ≫ f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫ f ◁ G.map g ◁ θ.naturality h ≫ f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫ f ◁ θ.naturality g ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<GOAL>Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Free K V<VAR>this : Free K ↥⊤<GOAL>Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝¹ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<VAR>F : Type u_5<VAR>inst✝ : FunLike F M N<VAR>mc : MonoidHomClass F M N<VAR>f : M →* N<GOAL>mrange (f.restrict S) = map f S
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>a : R<GOAL>(if a = 0 then ⊥ else sum 0 fun x e => e) = 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p p' : Submodule R M<GOAL>map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : ↥(Lp E 1 μ)<GOAL>‖setToFun μ T hT ↑↑f‖ ≤ max C 0 * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : ↥(Lp E 1 μ)<GOAL>‖(L1.setToL1 hT) f‖ ≤ max C 0 * ‖f‖
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as : Multiset α<VAR>bs₀ bs₁ : Multiset β<GOAL>Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as : Multiset α<VAR>bs₀ bs₁ : Multiset β<GOAL>(∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<VAR>h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<VAR>h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)<VAR>h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p<GOAL>(a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>a b : ℝ≥0<VAR>hp_pos : 0 < p<VAR>hpq : p ≤ q<VAR>h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)<VAR>h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p<GOAL>((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>(κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℚ_[p]<VAR>h : ‖z1 + z2‖ < ‖z1‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>‖z1 + z2‖ ≥ ‖z1‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z1 z2 : ℚ_[p]<VAR>h : ‖z1 + z2‖ < ‖z1‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>max ‖z1‖ ‖z2‖ ≥ ‖z1‖
<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>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>t : Set 𝕜<VAR>s : Set F<VAR>x : 𝕜<GOAL>derivWithin f t x ∈ s ↔ DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : MetrizableSpace E<VAR>f g : α → E<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>this✝¹ : MeasurableSpace (E × E) := borel (E × E)<VAR>this✝ : BorelSpace (E × E)<GOAL>MeasurableSet {x | f x = g x}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>V : OpenNhdsOf 1<GOAL>chaar K₀ ∈ clPrehaar (↑K₀) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>V : OpenNhdsOf 1<VAR>this : Classical.choose ⋯ ∈ ⋂ V, clPrehaar (↑K₀) V<GOAL>chaar K₀ ∈ clPrehaar (↑K₀) V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>V : OpenNhdsOf 1<VAR>this : ∀ (i : OpenNhdsOf 1), Classical.choose ⋯ ∈ clPrehaar (↑K₀) i<GOAL>chaar K₀ ∈ clPrehaar (↑K₀) V
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<GOAL>(Polynomial.idealX K).valuation P = (PowerSeries.idealX K).valuation ↑P
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<GOAL>∀ (p q : K[X]), q ≠ 0 → (Polynomial.idealX K).valuation (RatFunc.mk p q) = (PowerSeries.idealX K).valuation ↑(RatFunc.mk p q)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<VAR>f g : K[X]<VAR>h : g ≠ 0<GOAL>(Polynomial.idealX K).valuation (RatFunc.mk f g) = (PowerSeries.idealX K).valuation ↑(RatFunc.mk f g)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<VAR>f g : K[X]<VAR>h : g ≠ 0<GOAL>(PowerSeries.idealX K).valuation ↑(IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩) = (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<VAR>f g : K[X]<VAR>h : g ≠ 0<GOAL>↑(IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩) = IsLocalization.mk' (LaurentSeries K) ↑f ⟨↑g, ⋯⟩
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<VAR>f g : K[X]<VAR>h : g ≠ 0<GOAL>(Polynomial.idealX K).intValuation f = (PowerSeries.idealX K).intValuation ↑f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>P : RatFunc K<VAR>f g : K[X]<VAR>h : g ≠ 0<GOAL>(Polynomial.idealX K).intValuation g = (PowerSeries.idealX K).intValuation ↑⟨↑g, ⋯⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>x✝¹ : f.SameCycle x y<VAR>x✝ : f.SameCycle y z<VAR>i : ℤ<VAR>hi : (f ^ i) x = y<VAR>j : ℤ<VAR>hj : (f ^ j) y = z<GOAL>(f ^ (j + i)) x = z
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : ℕ → α → β<VAR>i : ℕ<VAR>h : i < l.length<VAR>h' : optParam (i < (mapIdx f l).length) ⋯<GOAL>(mapIdx f l).nthLe i h' = f i (l.nthLe i h)
<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>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace ℝ D<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedSpace ℝ V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : MeasurableSpace D<VAR>inst✝¹ : BorelSpace D<VAR>inst✝ : SecondCountableTopology D<VAR>μ : Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : 𝓢(D, V)<VAR>k : ℕ<GOAL>Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ
<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>inst✝⁸ : _root_.RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace ℝ D<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedSpace ℝ V<VAR>inst✝³ : NormedSpace 𝕜 V<VAR>inst✝² : MeasurableSpace D<VAR>inst✝¹ : BorelSpace D<VAR>inst✝ : SecondCountableTopology D<VAR>μ : Measure D<VAR>hμ : μ.HasTemperateGrowth<VAR>f : 𝓢(D, V)<VAR>k : ℕ<VAR>x : D<GOAL>‖f x‖ = ‖iteratedFDeriv ℝ 0 (⇑f) x‖
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(sin ↑x).im = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeInf α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f atBot l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>ν : Measure β<VAR>e : α ≃ᵐ β<GOAL>Measure.map (⇑e) (Measure.map (⇑e.symm) ν) = ν
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>-(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<GOAL>T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>f : G →g G'<VAR>p : G.Walk u v<GOAL>(Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph
<VAR>x y : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x ≠ 1<GOAL>log x < x - 1
<VAR>x y : ℝ<VAR>hx1 : 0 < x<VAR>hx2 : x ≠ 1<VAR>h : log x ≠ 0<GOAL>log x < x - 1
<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>p : Set β → Prop<GOAL>(∃ t ⊆ f '' s, p t) ↔ ∃ t ⊆ s, p (f '' t)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>n : ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁) ≫ (CategoryTheory.shiftFunctor C n).map f.hom₂ = (CategoryTheory.shiftFunctor C n).map f.hom₁ ≫ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₁)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>n : ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂) ≫ (CategoryTheory.shiftFunctor C n).map f.hom₃ = (CategoryTheory.shiftFunctor C n).map f.hom₂ ≫ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>n : ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁) ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) = (CategoryTheory.shiftFunctor C n).map f.hom₃ ≫ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>n : ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁ ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) = n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.hom₁) ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasShift C ℤ<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>n : ℤ<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁ ≫ (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) = n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁ ≫ (CategoryTheory.shiftFunctor C n ⋙ CategoryTheory.shiftFunctor C 1).map f.hom₁
<VAR>α : Type u_1<VAR>m✝ : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>m : MeasurableSpace ↑(memPartition t n)<GOAL>Measurable fun a => ⟨memPartitionSet t n a, ⋯⟩
<VAR>α : Type u_1<VAR>m✝ : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>m : MeasurableSpace ↑(memPartition t n)<VAR>s : ↑(memPartition t n)<GOAL>MeasurableSet ((fun a => ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {s})
<VAR>α : Type u_1<VAR>m✝ : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>m : MeasurableSpace ↑(memPartition t n)<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet {x | memPartitionSet t n x = s}
<VAR>α : Type u_1<VAR>m✝ : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<VAR>n : ℕ<VAR>m : MeasurableSpace ↑(memPartition t n)<VAR>s : Set α<VAR>hs : s ∈ memPartition t n<GOAL>MeasurableSet {x | x ∈ s}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>f : F<VAR>s t : Finset α<VAR>a b : α<GOAL>1 ∈ s / t ↔ ¬Disjoint s t