ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>this : Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop (𝓝 (∑' (n : ℕ), f n))<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>this : Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop (𝓝 (∑' (n : ℕ), f n))<VAR>F : ℕ → R := fun p => ∑' (e : ℕ), f (p ^ e)<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>this : Tendsto (fun n => ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p => ∑' (e : ℕ), f (p ^ e)) i) atTop (𝓝 (∑' (n : ℕ), f n))<VAR>F : ℕ → R := fun p => ∑' (e : ℕ), f (p ^ e)<VAR>H : ∀ (n : ℕ), ∏ i ∈ range n, {p | Nat.Prime p}.mulIndicator F i = ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : Kernel α β<VAR>a✝ : α<VAR>s✝ : Set β<VAR>hs : MeasurableSet s✝<GOAL>((κ.comapRight ⋯) a✝) s✝ = (κ a✝) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : Kernel α β<VAR>a✝ : α<VAR>s✝ : Set β<VAR>hs : MeasurableSet s✝<GOAL>(κ a✝) (id '' s✝) = (κ a✝) s✝
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁵ : T2Space β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>f : γ → α<VAR>inst✝² : MeasurableSpace.CountablySeparated α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : StandardBorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_meas : Measurable f<VAR>f_inj : InjOn f s<VAR>this : UpgradedStandardBorel γ := upgradeStandardBorel γ<VAR>tγ : TopologicalSpace γ := inferInstance<GOAL>MeasurableSet (f '' s)
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁵ : T2Space β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>f : γ → α<VAR>inst✝² : MeasurableSpace.CountablySeparated α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : StandardBorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_meas : Measurable f<VAR>f_inj : InjOn f s<VAR>this : UpgradedStandardBorel γ := upgradeStandardBorel γ<VAR>tγ : TopologicalSpace γ := inferInstance<VAR>τ : TopologicalSpace α<VAR>left✝¹ : SecondCountableTopology α<VAR>left✝ : T4Space α<VAR>right✝ : OpensMeasurableSpace α<GOAL>MeasurableSet (f '' s)
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁵ : T2Space β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>f : γ → α<VAR>inst✝² : MeasurableSpace.CountablySeparated α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : StandardBorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_meas : Measurable f<VAR>f_inj : InjOn f s<VAR>this : UpgradedStandardBorel γ := upgradeStandardBorel γ<VAR>tγ : TopologicalSpace γ := inferInstance<VAR>τ : TopologicalSpace α<VAR>left✝¹ : SecondCountableTopology α<VAR>left✝ : T4Space α<VAR>right✝ : OpensMeasurableSpace α<VAR>t' : TopologicalSpace γ<VAR>t't : t' ≤ tγ<VAR>f_cont : Continuous f<VAR>t'_polish : PolishSpace γ<GOAL>MeasurableSet (f '' s)
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>tβ : TopologicalSpace β<VAR>inst✝⁵ : T2Space β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace α<VAR>s : Set γ<VAR>f✝ : γ → β<VAR>f : γ → α<VAR>inst✝² : MeasurableSpace.CountablySeparated α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : StandardBorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_meas : Measurable f<VAR>f_inj : InjOn f s<VAR>this : UpgradedStandardBorel γ := upgradeStandardBorel γ<VAR>tγ : TopologicalSpace γ := inferInstance<VAR>τ : TopologicalSpace α<VAR>left✝¹ : SecondCountableTopology α<VAR>left✝ : T4Space α<VAR>right✝ : OpensMeasurableSpace α<VAR>t' : TopologicalSpace γ<VAR>t't : t' ≤ tγ<VAR>f_cont : Continuous f<VAR>t'_polish : PolishSpace γ<VAR>M : MeasurableSet s<GOAL>MeasurableSet (f '' s)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<GOAL>rexp ∘ Neg.neg '' univ = Ioi 0
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<GOAL>(spectrum ℝ A).Finite
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<GOAL>(⇑(algebraMap ℝ 𝕜) ⁻¹' spectrum 𝕜 A).Finite
<VAR>X : TopCat<VAR>U V : Opens ↑X<GOAL>↑(⋯.functor.obj ((map U.inclusion).obj V)) = ↑(V ⊓ U)
<VAR>X : TopCat<VAR>U V : Opens ↑X<GOAL>V.1 ∩ Set.range ⇑U.inclusion = ↑(V ⊓ U)
<VAR>X : TopCat<VAR>U V : Opens ↑X<GOAL>V.1 ∩ ↑U = ↑(V ⊓ U)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : MeasurableSpace α✝<VAR>inst✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsTop x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s<GOAL>borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : MeasurableSpace α✝<VAR>inst✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsTop x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s<VAR>e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ<VAR>e_1✝ : α = αᵒᵈ<GOAL>{S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Ioc l u = S} = {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s, l < u ∧ Ico l u = S}
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α✝<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : MeasurableSpace α✝<VAR>inst✝⁷ : OpensMeasurableSpace α✝<VAR>inst✝⁶ : MeasurableSpace δ<VAR>inst✝⁵ : LinearOrder α✝<VAR>inst✝⁴ : OrderClosedTopology α✝<VAR>a b x✝ : α✝<VAR>α : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α<VAR>hd : Dense s<VAR>hbot : ∀ (x : α), IsTop x → x ∈ s<VAR>hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s<VAR>x y : αᵒᵈ<VAR>hlt : x < y<VAR>he : Ioo x y = ∅<GOAL>Ioo y x = ∅
<VAR>σ : Type u<VAR>F G : Type u → Type u<VAR>inst✝² : Applicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α : Type u_1<VAR>β γ : Type u<VAR>g : α → G β<VAR>f : β → γ<VAR>x : σ ⊕ α<GOAL>(fun x => f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x => f <$> g x) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>a : R<GOAL>(X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>this : ((X - C a) ^ rootMultiplicity a p).Monic<GOAL>(X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>a : R<VAR>this : ((X - C a) ^ rootMultiplicity a p).Monic<GOAL>(X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = 0 + (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : PosSMulReflectLT α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>smul : ∀ (a : α) (b : β), f (a • b) = a • f b<VAR>a : α<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<VAR>h : a • b₁ < a • b₂<GOAL>b₁ < b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>γ : Type u_3<VAR>inst✝⁸ : Zero α<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Preorder β<VAR>inst✝⁴ : Zero γ<VAR>inst✝³ : Preorder γ<VAR>inst✝² : SMul α β<VAR>inst✝¹ : SMul α γ<VAR>f : β → γ<VAR>inst✝ : PosSMulReflectLT α γ<VAR>hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂<VAR>a : α<VAR>ha : 0 ≤ a<VAR>b₁ b₂ : β<VAR>smul : α → β → True<VAR>h : a • f b₁ < a • f b₂<GOAL>f b₁ < f b₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝¹² : Semiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : AddCommMonoid N'<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid P'<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R N'<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R P'<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>f₁₂ : M →ₗ[R] N<VAR>f₂₃ : N →ₗ[R] P<VAR>g₁₂ : M' →ₗ[R] N'<VAR>g₂₃ : N' →ₗ[R] P'<VAR>e₁ : M ≃ₗ[R] M'<VAR>e₂ : N ≃ₗ[R] N'<VAR>e₃ : P ≃ₗ[R] P'<VAR>h₁₂ : g₁₂ ∘ₗ ↑e₁ = ↑e₂ ∘ₗ f₁₂<VAR>h₂₃ : g₂₃ ∘ₗ ↑e₂ = ↑e₃ ∘ₗ f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<GOAL>Exact ⇑g₁₂ ⇑g₂₃
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : MulAction G₀ α<VAR>inst✝² : MeasurableSpace G₀<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSMul G₀ α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>MeasurableSet (a • s)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : GroupWithZero G₀<VAR>inst✝³ : MulAction G₀ α<VAR>inst✝² : MeasurableSpace G₀<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSMul G₀ α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>MeasurableSet ((fun x => a⁻¹ • x) ⁻¹' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : β →CO γ<VAR>f₁ f₂ : α →CO β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v w : V<VAR>s t : Set V<VAR>sconn : (induce s G).Connected<VAR>tconn : (induce t G).Connected<VAR>hv : v ∈ s<VAR>hw : w ∈ t<VAR>ha : G.Adj v w<GOAL>(induce (s ∪ t) G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v w : V<VAR>s t : Set V<VAR>sconn : (⊤.induce s).Connected<VAR>tconn : (⊤.induce t).Connected<VAR>hv : v ∈ s<VAR>hw : w ∈ t<VAR>ha : G.Adj v w<GOAL>(⊤.induce (s ∪ t)).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v w : V<VAR>s t : Set V<VAR>sconn : (⊤.induce s).Connected<VAR>tconn : (⊤.induce t).Connected<VAR>hv : v ∈ s<VAR>hw : w ∈ t<VAR>ha : G.Adj v w<GOAL>⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t ≤ ⊤.induce (s ∪ t)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>v w : V<VAR>s t : Set V<VAR>sconn : (⊤.induce s).Connected<VAR>tconn : (⊤.induce t).Connected<VAR>hv : v ∈ s<VAR>hw : w ∈ t<VAR>ha : G.Adj v w<GOAL>(⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t).verts = (⊤.induce (s ∪ t)).verts
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<GOAL>sq.HasLift ↔ ⋯.HasLift
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>f : A ⟶ X<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>g : B ⟶ Y<VAR>sq : CommSq f i p g<GOAL>Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<VAR>f' : ↑ps → ι := fun x => f ⟨↑x, ⋯⟩<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<VAR>f' : ↑ps → ι := fun x => f ⟨↑x, ⋯⟩<VAR>hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<VAR>f' : ↑ps → ι := fun x => f ⟨↑x, ⋯⟩<VAR>hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x<VAR>hf'i : Function.Injective f'<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<VAR>f' : ↑ps → ι := fun x => f ⟨↑x, ⋯⟩<VAR>hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x<VAR>hf'i : Function.Injective f'<VAR>f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }<VAR>hu : map f'e univ = s<GOAL>centroid k s p = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<VAR>f' : ↑ps → ι := fun x => f ⟨↑x, ⋯⟩<VAR>hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x<VAR>hf'i : Function.Injective f'<VAR>f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }<VAR>hu : map f'e univ = s<GOAL>centroid k univ (p ∘ ⇑f'e) = centroid k univ fun x => ↑x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>p : ι → P<VAR>hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j<VAR>ps : Set P<VAR>inst✝ : Fintype ↑ps<VAR>hps : ps = p '' ↑s<VAR>f : ↑(p '' ↑s) → ι := fun x => Exists.choose ⋯<VAR>hf : ∀ (x : ↑(p '' ↑s)), f x ∈ s ∧ p (f x) = ↑x<VAR>f' : ↑ps → ι := fun x => f ⟨↑x, ⋯⟩<VAR>hf' : ∀ (x : ↑ps), f' x ∈ s ∧ p (f' x) = ↑x<VAR>hf'i : Function.Injective f'<VAR>f'e : ↑ps ↪ ι := { toFun := f', inj' := hf'i }<VAR>hu : map f'e univ = s<VAR>x : ↑ps<GOAL>p (f' x) = ↑x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p q : α → Prop<VAR>a' : α<GOAL>(∃ a, p a ∧ a' = a) ↔ p a'
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>M : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝² : MonoidWithZero M₀<VAR>l✝ : List M₀<VAR>inst✝¹ : Nontrivial M₀<VAR>inst✝ : NoZeroDivisors M₀<VAR>a : M₀<VAR>l : List M₀<GOAL>(a :: l).prod = 0 ↔ 0 ∈ a :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrderedAddCommGroup α<VAR>inst✝¹ : OrderTopology α<VAR>l : Filter β<VAR>f g : β → α<VAR>inst✝ : NoMaxOrder α<GOAL>(𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {b | |b| < ε}
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasPullbacks C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<GOAL>∀ (g : Subobject X), (pullback f).obj ((map f).obj g) = g
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : LinearOrderedField α<GOAL>(∀ (x : α), ∃ n, x < ↑n) → Archimedean α
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : LinearOrderedField α<GOAL>(∀ (x : α), ∃ n, x < ↑n) → ∀ (x : α), ∃ n, x < ↑n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>h✝ : ∀ (x : α), ∃ n, x < ↑n<VAR>x : α<VAR>n : ℤ<VAR>h : x < ↑n<GOAL>↑n ≤ ↑n.toNat
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>hn : 2 ≤ n<GOAL>clog b n = clog b ((n + b - 1) / b) + 1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹³ : CommRing R₁<VAR>inst✝¹² : AddCommGroup M₁<VAR>inst✝¹¹ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁷ : CommRing R₃<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁴ : Field K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>inst✝¹ : Fintype n<VAR>b : Basis n R₃ M₃<VAR>J J₃ A A' : Matrix n n R₃<VAR>inst✝ : DecidableEq n<GOAL>A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : b ≠ 0<GOAL>Finite a b
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : WfDvdMonoid α<VAR>a : α<VAR>ha : ¬IsUnit a<VAR>n : ℕ<VAR>c : α<VAR>ndvd : ¬a ∣ c<VAR>hb : a ^ n * c ≠ 0<GOAL>Finite a (a ^ n * c)
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X Y : T<GOAL>map (𝟙 Y) = 𝟭 (Under Y)
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X Y : T<GOAL>∀ (X : Under Y), (map (𝟙 Y)).obj X = (𝟭 (Under Y)).obj X
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X Y : T<GOAL>autoParam (∀ (X Y_1 : Under Y) (f : X ⟶ Y_1), (map (𝟙 Y)).map f = eqToHom ⋯ ≫ (𝟭 (Under Y)).map f ≫ eqToHom ⋯) _auto✝
<VAR>R : CommRingCat<VAR>f : ↑Γ(Spec R, ⊤)<GOAL>(Spec R).basicOpen f = PrimeSpectrum.basicOpen ((Scheme.ΓSpecIso R).hom f)
<VAR>R : CommRingCat<VAR>f : ↑Γ(Spec R, ⊤)<GOAL>f = (Scheme.ΓSpecIso R).inv ((Scheme.ΓSpecIso R).hom f)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ e.target<GOAL>LiftPropWithinAt Q (↑e.symm) e.target x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>inst✝² : ChartedSpace H' M'<VAR>inst✝¹ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG✝ : G.LocalInvariantProp G' P<VAR>inst✝ : HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ e.target<GOAL>e.target ∈ 𝓝 x
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G<VAR>g : ℝ → E := ⇑(AffineMap.lineMap x y)<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g✝ : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>bound : ∀ x ∈ s, ‖f' x‖ ≤ C<VAR>hs : Convex ℝ s<VAR>xs : x ∈ s<VAR>ys : y ∈ s<VAR>this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G<VAR>g : ℝ → E := ⇑(AffineMap.lineMap x y)<VAR>segm : MapsTo g (Icc 0 1) s<GOAL>‖f y - f x‖ ≤ C * ‖y - x‖