ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝⁷ : DecidableEq α✝<VAR>inst✝⁶ : PartialOrder α✝<VAR>inst✝⁵ : BoundedOrder α✝<VAR>inst✝⁴ : IsSimpleOrder α✝<VAR>α : Type ?u.83175<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LE α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : IsSimpleOrder α<VAR>x : α<GOAL>(fun x => Bool.casesOn x ⊥ ⊤) ((fun x => decide (x = ⊤)) x) = x
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝⁷ : DecidableEq α✝<VAR>inst✝⁶ : PartialOrder α✝<VAR>inst✝⁵ : BoundedOrder α✝<VAR>inst✝⁴ : IsSimpleOrder α✝<VAR>α : Type ?u.83175<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : LE α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : IsSimpleOrder α<VAR>x : Bool<GOAL>(fun x => decide (x = ⊤)) ((fun x => Bool.casesOn x ⊥ ⊤) x) = x
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>hIE : I ⊆ E<GOAL>(uniqueBaseOn I E).Indep J ↔ J ⊆ I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<VAR>hIE : I ⊆ E<GOAL>J ⊆ I → J ⊆ E
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k ≤ n), u (k + 1)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<VAR>i : ι'<GOAL>Continuous ⇑((q i).comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<VAR>i : ι'<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>hC : (q i).comp f ≤ C • s.sup p<GOAL>Continuous ⇑((q i).comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<VAR>i : ι'<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>hC : (q i).comp f ≤ s.sup (C • p)<GOAL>Continuous ⇑((q i).comp f)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<VAR>i : ι'<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>hC : (q i).comp f ≤ s.sup (C • p)<GOAL>Continuous ⇑(∑ i ∈ s, (C • p) i)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<VAR>i : ι'<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>hC : (q i).comp f ≤ s.sup (C • p)<GOAL>Continuous fun x => (coeFnAddMonoidHom 𝕝 E) (∑ i ∈ s, C • p i) x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : AddCommGroup E<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : NormedField 𝕝<VAR>inst✝⁹ : Module 𝕝 E<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : AddCommGroup F<VAR>inst✝⁶ : Module 𝕜₂ F<VAR>inst✝⁵ : NormedField 𝕝₂<VAR>inst✝⁴ : Module 𝕝₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝² : RingHomIsometric τ₁₂<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>p : SeminormFamily 𝕝 E ι<VAR>q : SeminormFamily 𝕝₂ F ι'<VAR>x✝¹ : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>x✝ : TopologicalSpace F<VAR>hq : WithSeminorms q<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p q f<VAR>this : TopologicalAddGroup E<VAR>i : ι'<VAR>s : Finset ι<VAR>C : ℝ≥0<VAR>hC : (q i).comp f ≤ s.sup (C • p)<GOAL>Continuous fun x => ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E) (C • p c) x
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : V ↪ W<VAR>inst✝ : Subsingleton V<GOAL>SimpleGraph.map f G ≤ G'
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : V ↪ W<VAR>inst✝ : Subsingleton V<GOAL>G ≤ SimpleGraph.comap (⇑f) G'
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<GOAL>HasFDerivAtFilter f f' x L ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : ∀ (x' : E), ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0<GOAL>HasFDerivAtFilter f f' x L ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : ∀ (x' : E), ‖x' - x‖ = 0 → ‖f x' - f x - f' (x' - x)‖ = 0<GOAL>Tendsto (fun x_1 => ‖f x_1 - f x - f' (x_1 - x)‖ / ‖x_1 - x‖) L (𝓝 0) ↔ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i ≠ p
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : i.castSucc < p<GOAL>p.succAbove i ≠ p
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : p < i.succ<GOAL>p.succAbove i ≠ p
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>Memℒp f 2 μ ↔ Integrable (fun x => ‖f x‖ ^ 2) μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>Memℒp f 2 μ ↔ Memℒp (fun x => ‖f x‖ ^ 2) 1 μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → F<VAR>hf : AEStronglyMeasurable f μ<VAR>x✝ : α<GOAL>‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup F<VAR>f : α → F<VAR>hf : AEStronglyMeasurable f μ<GOAL>1 = 2 / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hb : BddAbove s<GOAL>↑(sSup s) = ⨆ a ∈ s, ↑a
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f✝ : G →g G'<VAR>f' : G' →g G''<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>f : G →g G'<VAR>hp : (Walk.map f p).IsPath<GOAL>p.IsPath
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : CauchyFilter α<GOAL>f ∈ closure (range pureCauchy)
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : CauchyFilter α<VAR>h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s<GOAL>f ∈ closure (range pureCauchy)
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : CauchyFilter α<VAR>h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s<GOAL>((𝓤 (CauchyFilter α)).lift' fun t => range pureCauchy ∩ UniformSpace.ball f t).NeBot
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : CauchyFilter α<VAR>h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s<GOAL>Monotone fun t => range pureCauchy ∩ UniformSpace.ball f t
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : CauchyFilter α<VAR>h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s<VAR>s : Set (CauchyFilter α × CauchyFilter α)<VAR>hs : s ∈ 𝓤 (CauchyFilter α)<GOAL>(range pureCauchy ∩ UniformSpace.ball f s).Nonempty
<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>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>inst✝¹ : T2Space M<VAR>inst✝ : T2Space M₂<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<GOAL>e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)
<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>R : Type u_7<VAR>R₂ : Type u_8<VAR>M : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring R₂<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>σ : R →+* R₂<VAR>σ' : R₂ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>inst✝¹ : T2Space M<VAR>inst✝ : T2Space M₂<VAR>f : ι → M<VAR>e : M ≃SL[σ] M₂<GOAL>∑' (z : ι), f z = e.symm (e (∑' (z : ι), f z))
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C).card * B.card ≤ (A / B).card * (B / C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A✝ B✝ C✝ A B C : Finset α<GOAL>(A * C).card * B⁻¹.card ≤ (A * B⁻¹).card * (B⁻¹ * C).card
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc a b → f x = g x<VAR>h' : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc b a → f x = g x<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ ⊤<VAR>hb : b ≠ ⊤<VAR>h : a.toNNReal ≤ b.toNNReal<GOAL>a ≤ b
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c w : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c w : ℂ<GOAL>(∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, 0), f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>this : (circleMap c R ⁻¹' {w}).Countable<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z) = ∮ (z : ℂ) in C(c, R), f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>this : (circleMap c R ⁻¹' {w}).Countable<VAR>θ : ℝ<VAR>hθ : θ ∉ circleMap c R ⁻¹' {w}<VAR>_' : θ ∈ Ι 0 (2 * π)<GOAL>deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) = deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c w : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>this : (circleMap c R ⁻¹' {w}).Countable<VAR>θ : ℝ<VAR>_' : θ ∈ Ι 0 (2 * π)<VAR>hθ : circleMap c R θ ≠ w<GOAL>deriv (circleMap c R) θ • (fun z => (z - w)⁻¹ • (z - w) • f z) (circleMap c R θ) = deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f✝ f : α → ℚ → ℝ<VAR>a : α<GOAL>IsRatStieltjesPoint (fun p => f p.2) ((), a) ↔ IsRatStieltjesPoint f a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ<VAR>f : α → ℝ<VAR>h : ∀ (x y : α), f x ≤ f y + dist x y<GOAL>∀ (x y : α), f x ≤ f y + ↑1 * dist x y
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>this : ↑((∑ i ∈ s, ((fun i => ⟨|f i|, ⋯⟩) i + (fun i => ⟨|g i|, ⋯⟩) i) ^ p) ^ (1 / p)) ≤ ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p) ^ (1 / p) + (∑ i ∈ s, (fun i => ⟨|g i|, ⋯⟩) i ^ p) ^ (1 / p))<GOAL>(∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>this : (∑ x ∈ s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) + (∑ x ∈ s, |g x| ^ p) ^ (1 / p)<GOAL>(∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle x (x - y)).cos * ‖x - y‖ = ‖x‖
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>a b : ℤ<GOAL>shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b (a + b) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hf : (mulSupport f).Finite<VAR>hg : (mulSupport g).Finite<GOAL>∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>inst✝ : Nonempty M<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<VAR>inhabited_h : Inhabited M<GOAL>(∀'liftAt 1 n φ).Realize v xs ↔ φ.Realize v xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>inst✝ : Nonempty M<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<VAR>inhabited_h : Inhabited M<GOAL>(∀ (a : M), φ.Realize v (snoc xs a ∘ castSucc)) ↔ φ.Realize v xs
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Ring R<VAR>n : ℤ<GOAL>(↑n).natTrailingDegree = 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>ht : t.Finite<VAR>hs : LinearIndependent K fun (x : ↑s) => ↑x<VAR>hst : s ⊆ ↑(span K t)<VAR>this✝ : s ⊆ ↑(span K ↑ht.toFinset)<VAR>u : Finset V<VAR>_hust : ↑u ⊆ s ∪ ↑ht.toFinset<VAR>hsu : s ⊆ ↑u<VAR>Eq : u.card = ht.toFinset.card<VAR>this : s.Finite<GOAL>this.toFinset.card ≤ u.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b✝ c✝ a b c : G<GOAL>a * (b / c) = a * b / c
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M✝ M : ModuleCat R<VAR>x : ↑(obj' f M)<GOAL>(LinearMap.baseChange S (𝟙 M)) x = (𝟙 (obj' f M)) x
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M✝ M : ModuleCat R<VAR>x : ↑(obj' f M)<GOAL>(LinearMap.baseChange S (𝟙 M)) x = x
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M✝ M : ModuleCat R<GOAL>(LinearMap.baseChange S (𝟙 M)) 0 = 0
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M✝ M : ModuleCat R<VAR>x✝ : ↑((restrictScalars f).obj (mk S))<VAR>y✝ : ↑M<GOAL>(LinearMap.baseChange S (𝟙 M)) (x✝ ⊗ₜ[R] y✝) = x✝ ⊗ₜ[R] y✝
<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M✝ M : ModuleCat R<VAR>m s : ↑((restrictScalars f).obj (mk S)) ⊗[R] ↑M<VAR>ihx : (LinearMap.baseChange S (𝟙 M)) m = m<VAR>ihy : (LinearMap.baseChange S (𝟙 M)) s = s<GOAL>(LinearMap.baseChange S (𝟙 M)) (m + s) = m + s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>ws : ι → R<VAR>zs : ι → E<VAR>wt : ι' → R<VAR>zt : ι' → E<VAR>hws : ∑ i ∈ s, ws i = 1<VAR>hwt : ∑ i ∈ t, wt i = 1<VAR>a b : R<VAR>hab : a + b = 1<GOAL>a • s.centerMass ws zs + b • t.centerMass wt zt = (s.disjSum t).centerMass (Sum.elim (fun i => a * ws i) fun j => b * wt j) (Sum.elim zs zt)