ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hg : ContinuousWithinAt g s x<GOAL>P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt (↑f ∘ g) s x ∧ P ((↑f ∘ g) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) 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>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hg : ContinuousWithinAt g s x<GOAL>P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ P ((↑f ∘ g) ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>r s : ℝ<VAR>hrs : r.IsConjExponent s<GOAL>{x | ∃ k > 0, beattySeq' r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<GOAL>ContinuousAt (⇑f) 0
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>h : ¬ContinuousAt (⇑f) 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>h : ¬ContinuousAt (⇑f) 0<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => _root_.id (b i)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>h : ¬ContinuousAt (⇑f) 0<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>h : ¬∀ (ib : Set F), ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib → ∃ ia, ia ≠ 0 ∧ ∀ x ∈ (↑ia)⁻¹ • b ia, f x ∈ _root_.id ib<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x ∈ (↑ia)⁻¹ • b ia, f x ∉ _root_.id V<VAR>hV : V ∈ 𝓝 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x ∈ (↑ia)⁻¹ • b ia, f x ∉ V<VAR>hV : V ∈ 𝓝 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<VAR>r : ℝ<VAR>hr : r > 0<VAR>h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<VAR>r : ℝ<VAR>hr : r > 0<VAR>h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V<VAR>n : ℕ<VAR>hn : r < ↑n<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<VAR>r : ℝ<VAR>hr : r > 0<VAR>h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V<VAR>n : ℕ<VAR>hn : r < ↑n<VAR>h1 : r ≤ ‖↑n‖<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<VAR>r : ℝ<VAR>hr : r > 0<VAR>h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V<VAR>n : ℕ<VAR>hn : r < ↑n<VAR>h1 : r ≤ ‖↑n‖<VAR>hn' : 0 < ‖↑n‖<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<VAR>r : ℝ<VAR>hr : r > 0<VAR>h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V<VAR>n : ℕ<VAR>hn : r < ↑n<VAR>h1 : r ≤ ‖↑n‖<VAR>hn' : ¬n = 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹¹ : AddCommGroup E<VAR>inst✝¹⁰ : UniformSpace E<VAR>inst✝⁹ : UniformAddGroup E<VAR>inst✝⁸ : AddCommGroup F<VAR>inst✝⁷ : UniformSpace F<VAR>inst✝⁶ : FirstCountableTopology E<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : ContinuousSMul 𝕜 E<VAR>inst✝² : RCLike 𝕜'<VAR>inst✝¹ : Module 𝕜' F<VAR>inst✝ : ContinuousSMul 𝕜' F<VAR>σ : 𝕜 →+* 𝕜'<VAR>f : E →ₛₗ[σ] F<VAR>hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)<VAR>b : ℕ → Set E<VAR>bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)<VAR>bE : (𝓝 0).HasAntitoneBasis fun i => b i<VAR>bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n<VAR>V : Set F<VAR>hV : V ∈ 𝓝 0<VAR>u : ℕ → E<VAR>hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia<VAR>hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V<VAR>h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)<VAR>h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)<VAR>r : ℝ<VAR>hr : r > 0<VAR>h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V<VAR>n : ℕ<VAR>hn : r < ↑n<VAR>h1 : r ≤ ‖↑n‖<VAR>hn' : ¬n = 0<VAR>h'' : f (u n) ∈ V<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f✝ f : X → Y<VAR>hf : Continuous f<VAR>U Z : Set Y<VAR>hU : IsOpen U<VAR>hZ : IsClosed Z<GOAL>IsLocallyClosed (f ⁻¹' (U ∩ Z))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>Y : R<GOAL>![0, Y, 0] 1 ^ 2 * ![0, Y, 0] 2 + W.a₁ * ![0, Y, 0] 0 * ![0, Y, 0] 1 * ![0, Y, 0] 2 + W.a₃ * ![0, Y, 0] 1 * ![0, Y, 0] 2 ^ 2 = ![0, Y, 0] 0 ^ 3 + W.a₂ * ![0, Y, 0] 0 ^ 2 * ![0, Y, 0] 2 + W.a₄ * ![0, Y, 0] 0 * ![0, Y, 0] 2 ^ 2 + W.a₆ * ![0, Y, 0] 2 ^ 3
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>Y : R<GOAL>Y ^ 2 * 0 + W.a₁ * 0 * Y * 0 + W.a₃ * Y * 0 ^ 2 = 0 ^ 3 + W.a₂ * 0 ^ 2 * 0 + W.a₄ * 0 * 0 ^ 2 + W.a₆ * 0 ^ 3
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ b ≤ c ↔ a \ c ≤ b
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(X ^ n + C a).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k : ℕ<VAR>h : k.succ ≠ 0<GOAL>(X ^ k.succ + C a).Monic
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : PseudoEMetricSpace X<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G X<VAR>inst✝ : IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>(fun x => c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>s : AddSubmonoid M<GOAL>(span ℕ ↑s).toAddSubmonoid = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a✝ : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a✝ : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a✝ : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>∑ i ∈ Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a✝ : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>∑ k ∈ range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a✝ : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>Summable fun k => d (n + k)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<GOAL>Set.range ⇑(lift f g H').val.base = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>this : IsIso (pullback.snd f g)<GOAL>Set.range ⇑(lift f g H').val.base = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>this : IsIso (pullback.snd f g)<GOAL>Set.range ⇑(inv (pullback.snd f g) ≫ pullback.fst f g).val.base = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>this✝ : IsIso (pullback.snd f g)<VAR>this : (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫ pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) = (pullback.fst f g).val.base<GOAL>Set.range ⇑(inv (pullback.snd f g) ≫ pullback.fst f g).val.base = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>this✝ : IsIso (pullback.snd f g)<VAR>this : (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫ pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) = (pullback.fst f g).val.base<GOAL>Set.range (⇑(pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) ∘ ⇑((inv (pullback.snd f g)).val.base ≫ (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom)) = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>this✝ : IsIso (pullback.snd f g)<VAR>this : (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫ pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) = (pullback.fst f g).val.base<GOAL>Set.range ⇑(pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) = ⇑f.val.base ⁻¹' Set.range ⇑g.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : LocallyRingedSpace<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>H : IsOpenImmersion f<VAR>H' : Set.range ⇑g.val.base ⊆ Set.range ⇑f.val.base<VAR>this✝ : IsIso (pullback.snd f g)<VAR>this : (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫ pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f) ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) = (pullback.fst f g).val.base<GOAL>Function.Surjective ⇑((inv (pullback.snd f g)).val.base ≫ (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a✝ b✝ c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>0 < a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α →ₘ[μ] β<GOAL>f.toGerm = ↑↑f
<VAR>r : ℝ<GOAL>¬(↑r).Infinite
<VAR>r : ℝ<GOAL>∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>G : K ⥤ C<VAR>inst✝ : HasColimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>k : K<GOAL>colimit.ι G k ≫ (isoOfEquivalence e w).inv = G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ : P<GOAL>affineSpan k {p₁, p₂} ∥ affineSpan k {p₃, p₄} ↔ vectorSpan k {p₁, p₂} = vectorSpan k {p₃, p₄}