ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<GOAL>∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<GOAL>∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<VAR>this : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<VAR>this : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)<VAR>L₁ : Tendsto (fun n => f (∑ i ∈ Finset.range n, u i)) atTop (𝓝 (f x))<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<VAR>this : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)<VAR>L₁ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (f x))<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<VAR>this : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)<VAR>L₁ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (f x))<VAR>L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<VAR>this : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)<VAR>L₁ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (f x))<VAR>L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))<VAR>feq : f x = y - 0<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>g : F → E<VAR>hg : ∀ (y : F), dist (f (g y)) y ≤ 1 / 2 * ‖y‖ ∧ ‖g y‖ ≤ C * ‖y‖<VAR>h : F → F := fun y => y - f (g y)<VAR>hle : ∀ (y : F), ‖h y‖ ≤ 1 / 2 * ‖y‖<VAR>y : F<VAR>hnle : ∀ (n : ℕ), ‖h^[n] y‖ ≤ (1 / 2) ^ n * ‖y‖<VAR>u : ℕ → E := fun n => g (h^[n] y)<VAR>ule : ∀ (n : ℕ), ‖u n‖ ≤ (1 / 2) ^ n * (C * ‖y‖)<VAR>sNu : Summable fun n => ‖u n‖<VAR>su : Summable u<VAR>x : E := tsum u<VAR>x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖<VAR>fsumeq : ∀ (n : ℕ), f (∑ i ∈ Finset.range n, u i) = y - h^[n] y<VAR>this : Tendsto (fun n => ∑ i ∈ Finset.range n, u i) atTop (𝓝 x)<VAR>L₁ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (f x))<VAR>L₂ : Tendsto (fun n => y - h^[n] y) atTop (𝓝 (y - 0))<VAR>feq : f x = y<GOAL>∃ x, f x = y ∧ ‖x‖ ≤ (2 * C + 1) * ‖y‖
<VAR>𝓕 : Type u_1<VAR>α✝ : Type u_2<VAR>E✝ : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedCommGroup E✝<VAR>inst✝² : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E✝<VAR>r r₁ r₂ : ℝ<VAR>α : Type u_5<VAR>E : Type u_6<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : PseudoEMetricSpace α<VAR>K Kf Kg : ℝ≥0<VAR>f g : α → E<VAR>s : Set α<VAR>x : α<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf + Kg) fun x => f x / g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<GOAL>∃ y, dist x y < δ ∧ dist y z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x y < δ ∧ dist y z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>hε : 0 < ε<VAR>h : dist x z / (ε + δ) < 1<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
<VAR>a : Ordinal.{u_1}<VAR>ha : Principal (fun x x_1 => x + x_1) a<VAR>b : Ordinal.{u_1}<GOAL>Principal (fun x x_1 => x + x_1) (a ^ b)
<VAR>b : Ordinal.{u_1}<VAR>ha : Principal (fun x x_1 => x + x_1) 0<GOAL>Principal (fun x x_1 => x + x_1) (0 ^ b)
<VAR>b c : Ordinal.{u_1}<VAR>ha : Principal (fun x x_1 => x + x_1) (ω ^ c)<GOAL>Principal (fun x x_1 => x + x_1) ((ω ^ c) ^ b)
<VAR>θ : Angle<VAR>h : θ ≠ ↑π<GOAL>SignType.sign θ.toReal = θ.sign
<VAR>θ : Angle<VAR>h : θ ≠ ↑π<VAR>ht : θ.toReal < 0<GOAL>SignType.sign θ.toReal = θ.sign
<VAR>θ : Angle<VAR>h : θ ≠ ↑π<VAR>ht : θ.toReal = 0<GOAL>SignType.sign θ.toReal = θ.sign
<VAR>θ : Angle<VAR>h : θ ≠ ↑π<VAR>ht : 0 < θ.toReal<GOAL>SignType.sign θ.toReal = θ.sign
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>χ : DirichletCharacter ℂ N<VAR>k : ZMod N<VAR>hχ : χ.IsPrimitive<GOAL>𝓕 (⇑χ) k = χ⁻¹ (-k) * gaussSum χ stdAddChar
<VAR>x : ℝ<VAR>n : ℕ<GOAL>cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
<VAR>x : ℝ<VAR>n : ℕ<VAR>A : 1 < 2 ^ (n + 1)<GOAL>cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
<VAR>x : ℝ<VAR>n : ℕ<VAR>A : 1 < 2 ^ (n + 1)<VAR>B : π / 2 ^ (n + 1) < π<GOAL>cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
<VAR>x : ℝ<VAR>n : ℕ<VAR>A : 1 < 2 ^ (n + 1)<VAR>B : π / 2 ^ (n + 1) < π<VAR>C : 0 < π / 2 ^ (n + 1)<GOAL>cos (π / 2 ^ (n + 1 + 1)) = sqrtTwoAddSeries 0 (n + 1) / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<GOAL>Memℒp f 1 μ ↔ Integrable f μ
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x : α<VAR>s t : Set α<VAR>y✝ z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedAddCommMonoid γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousWithinAt f s x<VAR>hg : LowerSemicontinuousWithinAt g s x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<VAR>y : γ<VAR>hy : y < (fun z => f z + g z) x<GOAL>∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝³ : Preorder β<VAR>f✝ g✝ : α → β<VAR>x : α<VAR>s t : Set α<VAR>y✝ z : β<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedAddCommMonoid γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : OrderTopology γ<VAR>f g : α → γ<VAR>hf : LowerSemicontinuousWithinAt f s x<VAR>hg : LowerSemicontinuousWithinAt g s x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<VAR>y : γ<VAR>hy : y < (fun z => f z + g z) x<VAR>u v : Set γ<VAR>u_open : IsOpen u<VAR>xu : f x ∈ u<VAR>v_open : IsOpen v<VAR>xv : g x ∈ v<VAR>h : u ×ˢ v ⊆ {p | y < p.1 + p.2}<GOAL>∀ᶠ (x' : α) in 𝓝[s] x, y < (fun z => f z + g z) x'
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiable 𝓘(𝕜, E) 𝓘(𝕜, E') f ↔ Differentiable 𝕜 f
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddGroup A<VAR>inst✝ : HasShift C A<VAR>X✝ Y : C<VAR>f : X✝ ⟶ Y<VAR>n : A<VAR>X : C<GOAL>(shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) = (shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((shiftFunctor C n).obj X)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>p : TangentBundle I M<VAR>st : s ⊆ t<VAR>hs : UniqueMDiffWithinAt I s p.proj<VAR>h : MDifferentiableWithinAt I I' f t p.proj<GOAL>(mfderivWithin I I' f s p.proj) p.snd = (mfderivWithin I I' f t p.proj) p.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f : Filter α<VAR>m : α → ℝ≥0∞<VAR>a b : ℝ≥0∞<VAR>hm : Tendsto m f (𝓝 a)<VAR>ha : a ≠ 0 ∨ b ≠ ⊤<GOAL>Tendsto (fun x => m x * b) f (𝓝 (a * b))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : (S.map F).HasHomology<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.Exact<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : (S.map F).HasHomology<VAR>this : S.HasHomology<GOAL>(S.map F).Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{u_4, u_2} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : (S.map F).HasHomology<VAR>this : S.HasHomology<VAR>h : 𝟙 S.leftHomologyData.H = 0<GOAL>(S.map F).Exact
<VAR>n d : Int<GOAL>(n /. d).inv = d /. n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>u : Set τ<VAR>hu : u ∈ f<GOAL>ω f ϕ s ⊆ closure (image2 ϕ u s)