ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a b b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ : ℝ<GOAL>ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ) (q, b₀)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a b b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < min a₀ b₀<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < min a₀ b₀<VAR>b : ℝ<VAR>lt_b : max a₀ b₀ < b<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : max a₀ b₀ < b<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this : IsCompact ({q} ×ˢ Icc a b)<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ < 1<VAR>h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b<VAR>h''δ : (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ < 1<VAR>h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b<VAR>h''δ : (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[univ] q<VAR>hv : ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this✝ : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ < 1<VAR>h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b<VAR>h''δ : (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[univ] q<VAR>hv : ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ<VAR>this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)<GOAL>∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀), dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this✝ : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ < 1<VAR>h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b<VAR>h''δ : (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[univ] q<VAR>hv : ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ<VAR>this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)<GOAL>∀ a ∈ v ×ˢ Ioo (b₀ - δ) (b₀ + δ), dist (∫ (t : ℝ) in a₀..a.2, f a.1 t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ) < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this✝ : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ < 1<VAR>h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b<VAR>h''δ : (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[univ] q<VAR>this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)<VAR>p : X<VAR>s : ℝ<VAR>hp : p ∈ v<VAR>hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)<VAR>hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ<GOAL>‖∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ‖ < ε
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : TopologicalSpace X<VAR>a✝ b✝ b₀✝ b₁ b₂ : ℝ<VAR>μ : Measure ℝ<VAR>f✝ : ℝ → E<VAR>inst✝¹ : NoAtoms μ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → ℝ → E<VAR>a₀ : ℝ<VAR>hf : Continuous (Function.uncurry f)<VAR>q : X<VAR>b₀ ε : ℝ<VAR>εpos : ε > 0<VAR>a : ℝ<VAR>a_lt : a < a₀ ∧ a < b₀<VAR>b : ℝ<VAR>lt_b : a₀ < b ∧ b₀ < b<VAR>this✝ : IsCompact ({q} ×ˢ Icc a b)<VAR>M : ℝ<VAR>hM : M ∈ upperBounds ((fun x => ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : δ < 1<VAR>h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b<VAR>h''δ : (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[univ] q<VAR>this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)<VAR>p : X<VAR>s : ℝ<VAR>hp : p ∈ v<VAR>hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)<VAR>hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ<VAR>J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v<GOAL>‖∫ (t : ℝ) in a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ‖ < ε
<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>f : E →L[𝕜] F<VAR>x y✝ : E<VAR>x✝ : y✝ ∈ EMetric.ball 0 ⊤<GOAL>HasSum (fun n => (f.fpowerSeries x (n + 2)) fun x => y✝) (f (x + y✝) - ∑ i ∈ Finset.range 2, (f.fpowerSeries x i) fun x => y✝)
<VAR>α : Type u_1<VAR>m✝ m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<GOAL>(μ.trim hm).FiniteSpanningSetsIn Set.univ
<VAR>α : Type u_1<VAR>m✝ m0✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>s : Set α<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>hm₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim ⋯)<VAR>i : ℕ<GOAL>(μ.trim hm) (spanningSets (μ.trim ⋯) i) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>i : Fin 1<GOAL>({a}.orderEmbOfFin ⋯) i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : MonoidHomClass F α β<VAR>l : Finset ι<VAR>S : ι → Set α<VAR>x✝ : α<GOAL>x✝ ∈ (fun f => ∏ i ∈ l, f i) '' (↑l).pi S ↔ x✝ ∈ ∏ i ∈ l, S i
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>derivWithin (fun y => f y + c) s x = derivWithin f s x
<VAR>α : Type u_1<VAR>inst✝ : AddGroupWithOne α<VAR>n : ZNum<GOAL>↑(ofZNum n) = ↑(↑n).toNat
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t A B : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ a⁻¹ • A ↔ a • x ∈ A
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>IsOpen ↑v.integer
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<GOAL>∀ x ∈ ↑v.integer, ↑v.integer ∈ 𝓝 x
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>hx : x ∈ ↑v.integer<GOAL>↑v.integer ∈ 𝓝 x
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>hx : x ∈ ↑v.integer<GOAL>∃ γ, {y | v (y - x) < ↑γ} ⊆ ↑v.integer
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : DivisionRing 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : CharZero 𝕜<VAR>inst✝² : Algebra ℝ 𝕜<VAR>inst✝¹ : ContinuousSMul ℝ 𝕜<VAR>inst✝ : TopologicalDivisionRing 𝕜<VAR>x : 𝕜<GOAL>Tendsto (fun n => ↑n / (↑n + x)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : DivisionRing 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : CharZero 𝕜<VAR>inst✝² : Algebra ℝ 𝕜<VAR>inst✝¹ : ContinuousSMul ℝ 𝕜<VAR>inst✝ : TopologicalDivisionRing 𝕜<VAR>x : 𝕜<GOAL>ℕ → 𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : DivisionRing 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : CharZero 𝕜<VAR>inst✝² : Algebra ℝ 𝕜<VAR>inst✝¹ : ContinuousSMul ℝ 𝕜<VAR>inst✝ : TopologicalDivisionRing 𝕜<VAR>x : 𝕜<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>?convert_2 n = ↑n / (↑n + x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : DivisionRing 𝕜<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : CharZero 𝕜<VAR>inst✝² : Algebra ℝ 𝕜<VAR>inst✝¹ : ContinuousSMul ℝ 𝕜<VAR>inst✝ : TopologicalDivisionRing 𝕜<VAR>x : 𝕜<GOAL>Tendsto ?convert_2 atTop (𝓝 1)
<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>inst✝⁴ : BorelSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>u : Set ↑s<VAR>hu : MeasurableSet u<GOAL>MeasurableSet (s.restrict f '' u)
<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>inst✝⁴ : BorelSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>u : Set ↑s<VAR>hu : MeasurableSet u<VAR>A : MeasurableSet (Subtype.val '' u)<GOAL>MeasurableSet (s.restrict f '' u)
<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>inst✝⁴ : BorelSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : PolishSpace γ<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : BorelSpace γ<VAR>hs : MeasurableSet s<VAR>f_cont : ContinuousOn f s<VAR>f_inj : InjOn f s<VAR>u : Set ↑s<VAR>hu : MeasurableSet u<VAR>A : MeasurableSet (Subtype.val '' u)<VAR>B : MeasurableSet (f '' (Subtype.val '' u))<GOAL>MeasurableSet (s.restrict f '' u)
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>e : ι₂ ↪ ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>((map e s₂).weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint (p ∘ ⇑e) b) (w ∘ ⇑e)
<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>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>e : ι₂ ↪ ι<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>∑ i ∈ map e s₂, w i • (p i -ᵥ b) = ∑ i ∈ s₂, (w ∘ ⇑e) i • ((p ∘ ⇑e) i -ᵥ b)
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>hb' : LinearIndependent S (⇑f' ∘ b)<GOAL>LinearIndependent K (⇑f ∘ b)
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>hb : ¬LinearIndependent K (⇑f ∘ b)<GOAL>¬LinearIndependent S (⇑f' ∘ b)
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>hb : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑f ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0<GOAL>∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑f' ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<GOAL>∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑f' ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<GOAL>∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<VAR>a : K<VAR>hag : ∀ i ∈ s, IsLocalization.IsInteger R (a * g i)<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hgI : a * g j ∉ ↑(RingHom.ker (algebraMap R S))<GOAL>∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0
<VAR>R : Type u<VAR>inst✝¹⁸ : CommRing R<VAR>S : Type v<VAR>inst✝¹⁷ : CommRing S<VAR>f✝ : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝¹⁶ : Algebra R S<VAR>K : Type u_1<VAR>inst✝¹⁵ : Field K<VAR>inst✝¹⁴ : Algebra R K<VAR>hRK : IsFractionRing R K<VAR>L : Type u_2<VAR>inst✝¹³ : Field L<VAR>inst✝¹² : Algebra S L<VAR>inst✝¹¹ : IsFractionRing S L<VAR>V : Type u_3<VAR>V' : Type u_4<VAR>V'' : Type u_5<VAR>inst✝¹⁰ : AddCommGroup V<VAR>inst✝⁹ : Module R V<VAR>inst✝⁸ : Module K V<VAR>inst✝⁷ : IsScalarTower R K V<VAR>inst✝⁶ : AddCommGroup V'<VAR>inst✝⁵ : Module R V'<VAR>inst✝⁴ : Module S V'<VAR>inst✝³ : IsScalarTower R S V'<VAR>inst✝² : AddCommGroup V''<VAR>inst✝¹ : Module R V''<VAR>inst✝ : IsDedekindDomain R<VAR>hRS : RingHom.ker (algebraMap R S) ≠ ⊤<VAR>f : V'' →ₗ[R] V<VAR>hf : Function.Injective ⇑f<VAR>f' : V'' →ₗ[R] V'<VAR>ι : Type u_6<VAR>b : ι → V''<VAR>s : Finset ι<VAR>g : ι → K<VAR>eq : ∑ i ∈ s, g i • (⇑f ∘ b) i = 0<VAR>j' : ι<VAR>hj's : j' ∈ s<VAR>hj'g : ¬g j' = 0<VAR>a : K<VAR>j : ι<VAR>hjs : j ∈ s<VAR>hgI : a * g j ∉ ↑(RingHom.ker (algebraMap R S))<VAR>g'' : (i : ι) → i ∈ s → R<VAR>hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i<VAR>this : (a : Prop) → Decidable a := Classical.propDecidable<VAR>g' : ι → R := fun i => if h : i ∈ s then g'' i h else 0<GOAL>∃ x, ∃ (_ : ∑ i ∈ s, x i • (⇑f' ∘ b) i = 0), ∃ x_1, ∃ (_ : x_1 ∈ s), ¬x x_1 = 0