ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<VAR>t : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0<VAR>i : ι<VAR>hit : i ∈ t<GOAL>(algebraMap R S) (g i * ↑(sec (v i)).2) = 0
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type v'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module S N<VAR>inst✝² : IsScalarTower R S N<VAR>p : Submonoid R<VAR>inst✝¹ : IsLocalization p S<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<VAR>hp : p ≤ R⁰<VAR>ι : Type u_1<VAR>v : ι → N<VAR>hf : ∀ (s : Finset ι) (g : ι → S), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0<VAR>sec : N → M × ↥p<VAR>hsec : ∀ (y : N), (sec y).2 • y = f (sec y).1<VAR>t : Finset ι<VAR>g : ι → R<VAR>hg : ∑ i ∈ t, g i • (sec (v i)).1 = 0<VAR>i : ι<VAR>hit : i ∈ t<GOAL>∑ i ∈ t, (fun i => (algebraMap R S) (g i * ↑(sec (v i)).2)) i • v i = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>inst✝¹ : Preorder β₁<VAR>inst✝ : Preorder β₂<VAR>u₁ : β₁ → α₁<VAR>u₂ : β₂ → α₂<GOAL>map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>g : α → β<VAR>h : α → β → β<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<VAR>a : α<GOAL>Nat.rec (g a) (fun n IH => h a (n, IH).2) (f a) = (h a)^[f a] (g a)
<VAR>s : Set (ℚ × ℚ)<GOAL>s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
<VAR>s : Set (ℚ × ℚ)<GOAL>(∃ i, 0 < i ∧ {p | AbsoluteValue.abs (p.2 - p.1) < i} ⊆ s) ↔ ∃ i, 0 < i ∧ {p | dist p.1 p.2 < ↑i} ⊆ s
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b✝ : B<VAR>y✝ : E b✝<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>{ proj := b, snd := e.symm b y } = ↑e.symm (b, y)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Integrable f μ<GOAL>0 < μ {x | f x ≤ ∫ (a : α), f a ∂μ}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Group α<VAR>inst✝² : DivisionMonoid β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MonoidHomClass F α β<VAR>m : F<VAR>s✝ t✝ : Set α<VAR>hm : Injective ⇑m<VAR>s t : Set β<VAR>hs : s ⊆ range ⇑m<VAR>ht : t ⊆ range ⇑m<GOAL>⇑m '' (⇑m ⁻¹' (s / t)) = ⇑m '' (⇑m ⁻¹' s / ⇑m ⁻¹' t)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CharP R p<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(frobenius x).coeff n = ((map (_root_.frobenius R p)) x).coeff n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0<VAR>i : ι<GOAL>(nullHomotopicMap hom).f i = (dNext i) hom + (prevD i) hom + Hom.f 0 i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>hom : (i j : ι) → C.X i ⟶ D.X j<VAR>zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0<VAR>i : ι<GOAL>(nullHomotopicMap hom).f i = (dNext i) hom + (prevD i) hom
<VAR>n : ℕ<GOAL>ContinuousOn (fun x => term (n + 1) x) (Ici 1)
<VAR>n : ℕ<GOAL>ContinuousOn (fun x => ∫ (x_1 : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x_1 - ↑(n + 1)) / x_1 ^ (x + 1) ∂volume) (Ici 1)
<VAR>n : ℕ<GOAL>∀ x ∈ Ici 1, AEStronglyMeasurable (fun a => (a - ↑(n + 1)) / a ^ (x + 1)) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))
<VAR>n : ℕ<GOAL>∀ x ∈ Ici 1, ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ‖(a - ↑(n + 1)) / a ^ (x + 1)‖ ≤ (a - ↑(n + 1)) / a ^ 2
<VAR>n : ℕ<GOAL>Integrable (fun x => (x - ↑(n + 1)) / x ^ 2) (volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)))
<VAR>n : ℕ<GOAL>∀ᵐ (a : ℝ) ∂volume.restrict (Ioc (↑(n + 1)) (↑(n + 1) + 1)), ContinuousOn (fun x => (a - ↑(n + 1)) / a ^ (x + 1)) (Ici 1)
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>it.hasNext = true ↔ r ≠ []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<VAR>hinj : Injective f<VAR>x : α<VAR>this : (a : Prop) → Decidable a<GOAL>∃ a, f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<VAR>hinj : Injective f<VAR>x : α<VAR>this : (a : Prop) → Decidable a<VAR>val✝ : Fintype α<GOAL>∃ a, f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<VAR>hinj : Injective f<VAR>x : α<VAR>this : (a : Prop) → Decidable a<VAR>val✝ : Fintype α<VAR>h₁ : image f univ = univ<GOAL>∃ a, f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<VAR>hinj : Injective f<VAR>x : α<VAR>this : (a : Prop) → Decidable a<VAR>val✝ : Fintype α<VAR>h₁ : image f univ = univ<VAR>h₂ : x ∈ image f univ<GOAL>∃ a, f a = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<VAR>hinj : Injective f<VAR>x : α<VAR>this : (a : Prop) → Decidable a<VAR>val✝ : Fintype α<VAR>h₁ : image f univ = univ<VAR>h₂ : x ∈ image f univ<VAR>y : α<VAR>h : y ∈ univ ∧ f y = x<GOAL>∃ a, f a = x
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z<VAR>e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL<GOAL>‖f w‖ = ‖f z‖
<VAR>E : Type u<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℂ F<VAR>f : ℂ → F<VAR>z w : ℂ<VAR>hd : DiffContOnCl ℂ f (ball z (dist w z))<VAR>hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z<VAR>e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL<VAR>he : ∀ (x : F), ‖e x‖ = ‖x‖<GOAL>‖f w‖ = ‖f z‖
<VAR>α : Type u_1<VAR>m n : PosNum<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>α : Type u_1<VAR>m n : PosNum<GOAL>¬↑n < ↑m ↔ m ≤ n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<GOAL>((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = sheafifyLift J (whiskerLeft G.op (toSheafify K F)) ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<GOAL>toSheafify J (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫ ((G.pushforwardContinuousSheafificationCompatibility A J K).hom.app F).val = whiskerLeft G.op (toSheafify K F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>f : α → β<VAR>hs : autoParam ∅.Finite _auto✝<GOAL>∅.ncard ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>x : α<VAR>hx : x ∈ s<GOAL>(∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>x : α<VAR>hx : x ∈ s<GOAL>(s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>f : α → β<VAR>x a : α<VAR>hs : autoParam {a}.Finite _auto✝<VAR>hx : x ∈ {a}<GOAL>∀ {a_1 b : α}, a_1 ∈ {a} → b ∈ {a} → a_1 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>f : α → β<VAR>x a : α<VAR>hs : autoParam {a}.Finite _auto✝<VAR>hx : x = a<GOAL>∀ {a_1 b : α}, a_1 = a → b = a → a_1 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set α<VAR>f : α → β<VAR>x : α<VAR>hs : autoParam {x}.Finite _auto✝<GOAL>∀ {a b : α}, a = x → b = x → a = b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>h : IsTopologicalBasis {s | IsClopen s}<VAR>x y : X<VAR>hxy : x ≠ y<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>h : IsTopologicalBasis {s | IsClopen s}<VAR>x y : X<VAR>hxy : x ≠ y<VAR>U : Set X<VAR>hU : U ∈ {s | IsClopen s}<VAR>hxU : x ∈ U<VAR>hyU : U ⊆ {y_1 | y_1 ≠ y}<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Surjective (image f) ↔ Surjective f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Surjective (image f)<VAR>y : β<GOAL>∃ a, f a = y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Surjective (image f)<VAR>y : β<VAR>s : Set α<VAR>hs : f '' s = {y}<GOAL>∃ a, f a = y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>h : Surjective (image f)<VAR>y : β<VAR>s : Set α<VAR>hs : f '' s = {y}<VAR>this : y ∈ {y}<GOAL>∃ a, f a = y
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type w<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜 F✝<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<VAR>F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type w<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜 F✝<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<VAR>F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s<VAR>this : FiniteDimensional 𝕜 ↥F<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type w<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜 F✝<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<VAR>F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s<VAR>this : FiniteDimensional 𝕜 ↥F<VAR>Fclosed : IsClosed ↑F<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type w<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜 F✝<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<VAR>F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s<VAR>this✝ : FiniteDimensional 𝕜 ↥F<VAR>Fclosed : IsClosed ↑F<VAR>this : ∃ x, x ∉ F<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type w<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜 F✝<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<VAR>F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s<VAR>this✝ : FiniteDimensional 𝕜 ↥F<VAR>Fclosed : IsClosed ↑F<VAR>this : ∃ x, x ∉ F<VAR>x : E<VAR>xR : ‖x‖ ≤ R<VAR>hx : ∀ y ∈ F, 1 ≤ ‖x - y‖<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>F✝ : Type w<VAR>inst✝⁷ : NormedAddCommGroup F✝<VAR>inst✝⁶ : NormedSpace 𝕜 F✝<VAR>F' : Type x<VAR>inst✝⁵ : AddCommGroup F'<VAR>inst✝⁴ : Module 𝕜 F'<VAR>inst✝³ : TopologicalSpace F'<VAR>inst✝² : TopologicalAddGroup F'<VAR>inst✝¹ : ContinuousSMul 𝕜 F'<VAR>inst✝ : CompleteSpace 𝕜<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>h : ¬FiniteDimensional 𝕜 E<VAR>s : Finset E<VAR>F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s<VAR>this✝ : FiniteDimensional 𝕜 ↥F<VAR>Fclosed : IsClosed ↑F<VAR>this : ∃ x, x ∉ F<VAR>x : E<VAR>xR : ‖x‖ ≤ R<VAR>hx : ∀ y ∈ F, 1 ≤ ‖x - y‖<VAR>hx' : ∀ y ∈ F, 1 ≤ ‖y - x‖<GOAL>∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s t = 0 ↔ closure s = closure t
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝² : HasZeroObject C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasBinaryBiproduct X Y<GOAL>BicartesianSq biprod.fst biprod.snd 0 0
<VAR>α : Type u_1<VAR>inst✝¹ : Div α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y
<VAR>α : Type u_1<VAR>inst✝¹ : Div α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : α<GOAL>(equivShrink α) (x / y) = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x) / (equivShrink α).symm ((equivShrink α) y))
<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>k n : ℕ<VAR>x✝ : E<GOAL>‖x✝‖ ^ k * ‖iteratedFDeriv ℝ n (⇑0) x✝‖ ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s : Set α<VAR>h : BddAbove s<VAR>hs : s.Nonempty<GOAL>(𝓟 s).limsSup = sSup s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s : Set α<VAR>h : BddAbove s<VAR>hs : s.Nonempty<GOAL>sInf {a | ∀ x ∈ s, x ≤ a} = sSup s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s✝ t✝ : Multiset α<VAR>a✝ : α<VAR>s : Multiset α<VAR>h : ∀ (a : α) (t : Multiset α), s ≠ a ::ₘ a ::ₘ t<VAR>a : α<VAR>le : a ::ₘ a ::ₘ 0 ≤ s<VAR>t : Multiset α<VAR>s_eq : s = a ::ₘ a ::ₘ 0 + t<GOAL>s = a ::ₘ a ::ₘ t
<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 f : MvPolynomial σ R<VAR>x : σ →₀ ℕ<VAR>H : x ∈ f.support<VAR>v : σ<VAR>h : v ∉ f.vars<GOAL>x v = 0
<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 f : MvPolynomial σ R<VAR>x : σ →₀ ℕ<VAR>H : x ∈ f.support<VAR>v : σ<VAR>h : x v ≠ 0<GOAL>v ∈ f.vars
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<GOAL>∃ x ∈ S, IsClosed {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<VAR>V : Set X<VAR>Vsub : V ⊆ S<VAR>Vne : V.Nonempty<VAR>Vcls : IsClosed V<VAR>hV : ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V<GOAL>∃ x ∈ S, IsClosed {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<VAR>x : X<VAR>Vsub : {x} ⊆ S<VAR>Vne : {x}.Nonempty<VAR>Vcls : IsClosed {x}<VAR>hV : ∀ V' ⊆ {x}, V'.Nonempty → IsClosed V' → V' = {x}<GOAL>∃ x ∈ S, IsClosed {x}
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<VAR>h : UniqueDiffWithinAt 𝕜 s x<GOAL>iteratedDerivWithin 1 f s x = derivWithin f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<VAR>h : UniqueDiffWithinAt 𝕜 s x<GOAL>(fderivWithin 𝕜 f s x) 1 = derivWithin f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<VAR>h : l ≠ []<VAR>head✝ : α<VAR>tail✝ : List α<VAR>x✝ : head✝ :: tail✝ ≠ []<GOAL>(head✝ :: tail✝).maximum ≠ ⊥
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>μ : Measure G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>t : G<VAR>p : G → Prop<GOAL>(∀ᵐ (x : G) ∂μ, p (x * t)) ↔ {x | p x} ∈ Filter.map (fun h => h * t) (ae μ)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>n✝¹ : ℕ<VAR>f : Fin (n✝¹ + 1) → α<VAR>a : α<VAR>n✝ n m : ℕ<VAR>h : n ≤ m<GOAL>∀ {a b : Fin n}, { toFun := fun i => ⟨castLE h i, ⋯⟩, invFun := fun i => ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤ { toFun := fun i => ⟨castLE h i, ⋯⟩, invFun := fun i => ⟨↑↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔ a ≤ b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid A<VAR>inst✝¹⁰ : Module R A<VAR>inst✝⁹ : AddCommMonoid B<VAR>inst✝⁸ : Module R B<VAR>inst✝⁷ : AddCommMonoid C<VAR>inst✝⁶ : Module R C<VAR>inst✝⁵ : AddCommMonoid D<VAR>inst✝⁴ : Module R D<VAR>inst✝³ : CoalgebraStruct R A<VAR>inst✝² : CoalgebraStruct R B<VAR>inst✝¹ : CoalgebraStruct R C<VAR>inst✝ : CoalgebraStruct R D<VAR>φ₁ : B →ₗc[R] C<VAR>φ₂ : A →ₗc[R] B<VAR>x✝ : A<GOAL>(map __src✝ __src✝ ∘ₗ comul) x✝ = (comul ∘ₗ __src✝) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<GOAL>(s ∩ (t ∩ t')).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<GOAL>¬s ⊆ tᶜ ∪ t'ᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<VAR>h' : s ⊆ tᶜ ∪ t'ᶜ<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<VAR>h' : s ⊆ tᶜ ∪ t'ᶜ<VAR>xt' : x ∉ t'<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<VAR>h' : s ⊆ tᶜ ∪ t'ᶜ<VAR>xt' : x ∉ t'<VAR>yt : y ∉ t<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<VAR>h' : s ⊆ tᶜ ∪ t'ᶜ<VAR>xt' : x ∉ t'<VAR>yt : y ∉ t<VAR>this : (s ∩ (tᶜ ∩ t'ᶜ)).Nonempty<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>h : IsPreconnected s<VAR>t t' : Set α<VAR>ht : IsClosed t<VAR>ht' : IsClosed t'<VAR>htt' : s ⊆ t ∪ t'<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<VAR>y : α<VAR>ys : y ∈ s<VAR>yt' : y ∈ t'<VAR>h' : s ⊆ tᶜ ∪ t'ᶜ<VAR>xt' : x ∉ t'<VAR>yt : y ∉ t<VAR>this : (s ∩ (t ∪ t')ᶜ).Nonempty<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<GOAL>(s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : y ∈ v<GOAL>¬s ⊆ uᶜ ∪ vᶜ