ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : EqOn f g s<VAR>hr : r ∈ 𝓤 α<VAR>t : β → Set β<VAR>t_open : ∀ x ∈ s, IsOpen (t x)<VAR>xt : ∀ x ∈ s, x ∈ t x<VAR>ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r<VAR>x : β<VAR>hx : x ∈ ⋃ x ∈ s, t x<GOAL>(f x, g x) ∈ r
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : TopologicalSpace β<VAR>r : Set (α × α)<VAR>s : Set β<VAR>f g : β → α<VAR>hf : ∀ x ∈ s, ContinuousAt f x<VAR>hg : ∀ x ∈ s, ContinuousAt g x<VAR>hfg : EqOn f g s<VAR>hr : r ∈ 𝓤 α<VAR>t : β → Set β<VAR>t_open : ∀ x ∈ s, IsOpen (t x)<VAR>xt : ∀ x ∈ s, x ∈ t x<VAR>ht : ∀ x ∈ s, ∀ z ∈ t x, (f z, g z) ∈ r<VAR>x : β<VAR>hx : ∃ i ∈ s, x ∈ t i<GOAL>(f x, g x) ∈ r
<VAR>P : ℤ → Prop<VAR>inst✝ : DecidablePred P<VAR>b b' : ℤ<VAR>Hb : ∀ (z : ℤ), P z → z ≤ b<VAR>Hb' : ∀ (z : ℤ), P z → z ≤ b'<VAR>Hinh : ∃ z, P z<VAR>n : ℤ<VAR>hn : P n<VAR>h2n : ∀ (z : ℤ), P z → z ≤ n<VAR>n' : ℤ<VAR>hn' : P n'<VAR>h2n' : ∀ (z : ℤ), P z → z ≤ n'<GOAL>↑⟨n, ⋯⟩ = ↑⟨n', ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : IsGLB s x<GOAL>IsGLB (id '' s) (id x)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 n g<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : ∀ x ∉ k, g x = 0<GOAL>ContDiff 𝕜 n (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedAddCommGroup E''<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>inst✝⁹ : NormedSpace 𝕜 E''<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : MeasurableSpace G<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup P<VAR>inst✝ : NormedSpace 𝕜 P<VAR>μ : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>n : ℕ∞<VAR>hcg : HasCompactSupport g<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContDiff 𝕜 n g<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : ∀ x ∉ k, g x = 0<GOAL>ContDiffOn 𝕜 n (f ⋆[L, μ] g) univ
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>f : D ≌ E<VAR>X : C<GOAL>f.functor.map (e.functor.map (e.unitIso.hom.app X ≫ e.inverse.map (f.unitIso.hom.app (e.functor.obj X)))) ≫ f.functor.map (e.counitIso.hom.app (f.inverse.obj (f.functor.obj (e.functor.obj X)))) ≫ f.counitIso.hom.app (f.functor.obj (e.functor.obj X)) = 𝟙 (f.functor.obj (e.functor.obj X))
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>f : D ≌ E<VAR>X : C<GOAL>f.functor.map ((f.unitIso.hom.app (e.functor.obj X) ≫ 𝟙 ((𝟭 D).obj (f.inverse.obj (f.functor.obj (e.functor.obj X))))) ≫ f.unitInv.app (e.functor.obj X)) = 𝟙 (f.functor.obj (e.functor.obj X))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>T.card = (B + 1) ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>A : Matrix α β ℤ<VAR>v : β → ℤ<VAR>hn : m < n<VAR>hm : 0 < m<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>∏ i : β, (Icc (0 i) ↑B).card = (B + 1) ^ n
<VAR>R : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>r : R<VAR>M : Type u_1<VAR>M' : Type u_3<VAR>M'' : Type ?u.123295<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>f : M →ₗ[R] M'<VAR>hf : Surjective ⇑f<VAR>H₁ : Surjective (⇑(r • ⊤).mkQ ∘ ⇑f)<GOAL>Surjective (⇑((map r) f) ∘ ⇑(r • ⊤).mkQ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>I.IsRadical ↔ IsReduced (R ⧸ I)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>(RingHom.ker (Quotient.mk I)).IsRadical ↔ IsReduced (R ⧸ I)
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E → F<VAR>C : ℝ≥0<GOAL>LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<GOAL>(((match l with | nil => 0 | node sz l x r => sz) + match m with | nil => 0 | node sz l x r => sz) + 1 + match r with | nil => 0 | node sz l x r => sz) + 1 = (((match l with | nil => 0 | node sz l x r => sz) + match m with | nil => 0 | node sz l x r => sz) + match r with | nil => 0 | node sz l x r => sz) + 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : PartialOrder α<VAR>s : Set α<VAR>a : α<GOAL>(∀ ⦃b : α⦄, a ≤ b → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, a < b → a ∈ s → b ∈ s
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : T.Finite<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<GOAL>S.Finite
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : Finite ↑T<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<GOAL>S.Finite
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : Finite ↑T<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<VAR>x✝¹ x✝ : ↑S<VAR>h_eq : (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝¹ = (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝<GOAL>x✝¹ = x✝
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : Finite ↑T<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<VAR>x✝¹ x✝ : ↑S<VAR>h_eq : (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝¹ = (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝<GOAL>↑↑x✝¹ = ↑↑x✝
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : Finite ↑T<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<VAR>x✝¹ x✝ : ↑S<VAR>h_eq : (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝¹ = (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝<GOAL>↑↑x✝¹ = ℚ⟮⋯.choose⟯
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>A : Type u_2<VAR>inst✝¹ : Field A<VAR>inst✝ : CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : Finite ↑T<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<VAR>x✝¹ x✝ : ↑S<VAR>h_eq : (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝¹ = (fun x => match x with | ⟨F, hF⟩ => ⟨⋯.choose, ⋯⟩) x✝<GOAL>↑↑x✝ = ℚ⟮⋯.choose⟯
<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>s : Set E<VAR>n : ℕ<GOAL>fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ iteratedFDerivWithin 𝕜 (n + 1) f s
<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>s : Set E<VAR>n : ℕ<GOAL>fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
<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>s : Set E<VAR>n : ℕ<VAR>x : E<GOAL>fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x = (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x
<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>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<GOAL>Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
<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>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<VAR>h : Iio x = ∅<GOAL>Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
<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>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<VAR>h : (Iio x).Nonempty<GOAL>Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
<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>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<VAR>h : (Iio x).Nonempty<VAR>l : β<VAR>hl : l < sSup (f '' Iio x)<GOAL>∀ᶠ (b : α) in 𝓝[<] x, l < f b
<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>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<VAR>h : (Iio x).Nonempty<VAR>m : β<VAR>hm : m > sSup (f '' Iio x)<GOAL>∀ᶠ (b : α) in 𝓝[<] x, f b < m
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s✝ t✝ s₁ s₂ t₁ t₂ : Set X<VAR>x : X<VAR>s t : Set X<GOAL>𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : StarRing R<VAR>inst✝² : StarOrderedRing R<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.PosSemidef<VAR>hB : (A ^ 2).PosSemidef<GOAL>A = hB.sqrt
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : ↥S<GOAL>IsUnit ↑x ↔ IsUnit x
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : ↥S<VAR>hx : IsUnit ↑x<GOAL>x * ⟨↑hx.unit⁻¹, ⋯⟩ = 1
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S✝ S : StarSubalgebra ℂ A<VAR>hS : IsClosed ↑S<VAR>x : ↥S<VAR>hx : IsUnit ↑x<GOAL>⟨↑hx.unit⁻¹, ⋯⟩ * x = 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<GOAL>({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (𝟙 f✝)).app = (𝟙 ({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map f✝)).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>X : ↑({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.obj a✝)<GOAL>({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (𝟙 f✝)).app X = (𝟙 ({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map f✝)).app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ g✝ h✝ : a✝ ⟶ b✝<VAR>η✝ : f✝ ⟶ g✝<VAR>θ✝ : g✝ ⟶ h✝<GOAL>({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (η✝ ≫ θ✝)).app = ({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ η✝ ≫ { obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ θ✝).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ g✝ h✝ : a✝ ⟶ b✝<VAR>η✝ : f✝ ⟶ g✝<VAR>θ✝ : g✝ ⟶ h✝<VAR>X : ↑({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.obj a✝)<GOAL>({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ (η✝ ≫ θ✝)).app X = ({ obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ η✝ ≫ { obj := fun C => Cat.of (WithInitial ↑C), map := fun {X Y} => map, map₂ := fun {a b} {f g} => map₂ }.map₂ θ✝).app X
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<GOAL>⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<GOAL>⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<GOAL>⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<VAR>cf : ℝ<VAR>hcf : cf ∈ lowerBounds (range ⇑f)<GOAL>⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<VAR>cf : ℝ<VAR>hcf : cf ∈ lowerBounds (range ⇑f)<VAR>Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x<GOAL>⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f g : GromovHausdorff.Cb X Y<VAR>cg : ℝ<VAR>hcg : cg ∈ lowerBounds (range ⇑g)<VAR>Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x<VAR>cf : ℝ<VAR>hcf : cf ∈ lowerBounds (range ⇑f)<VAR>Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x<VAR>Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g<GOAL>⨆ x, ⨅ y, f (inl x, inr y) ≤ (⨆ x, ⨅ y, g (inl x, inr y)) + dist f g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>A : CompleteSpace ℝ<GOAL>0 ≤ ∫ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>A : CompleteSpace ℝ<GOAL>0 ≤ if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : LT α<VAR>s : Finset ι<VAR>f : ι → WithTop α<GOAL>∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<GOAL>f (-c) = -f 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>X Y : J<VAR>f : X ⟶ Y<GOAL>𝟙 c.pt ≫ c.π.app Y = c.π.app X ≫ (D.map f).f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>T : Monad C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>D : J ⥤ T.Algebra<VAR>c : Cone (D ⋙ T.forget)<VAR>t : IsLimit c<VAR>X Y : J<VAR>f : X ⟶ Y<GOAL>𝟙 c.pt ≫ c.π.app Y = c.π.app Y
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>f : ι → α<VAR>a : α<GOAL>⋃ i, Ico (f i) a = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P ≃ₗ[R] Q<VAR>f✝ : N ≃ₗ[R] P<VAR>m : M<VAR>n✝ : N<VAR>p : P<VAR>x : M ⊗[R] N<VAR>y : N ⊗[R] M<VAR>f : M ≃ₗ[R] M<VAR>n : ℤ<GOAL>rTensor N f ^ n = rTensor N (f ^ n)