ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s✝ : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hp : HasFPowerSeriesAt f p z₀<VAR>hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • (fslope^[p.order] p).coeff n) ((swap dslope z₀)^[p.order] f z)<VAR>x : 𝕜<VAR>hx2 : HasSum (fun n => (x - z₀) ^ n • p.coeff n) (f x)<VAR>this : ∀ k < p.order, p.coeff k = 0<VAR>s : E<VAR>hs1 : (x - z₀) ^ p.order • s = f x<VAR>hs2 : HasSum (fun m => (x - z₀) ^ m • p.coeff (m + p.order)) s<VAR>hx1 : HasSum (fun n => (x - z₀) ^ n • p.coeff (n + p.order)) ((swap dslope z₀)^[p.order] f x)<GOAL>(swap dslope z₀)^[p.order] f x = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<GOAL>hg.compLp g0 0 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<GOAL>↑↑(hg.compLp g0 0) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<GOAL>g ∘ ↑↑0 =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>a✝ : α<VAR>ha : ↑↑0 a✝ = 0 a✝<GOAL>(g ∘ ↑↑0) a✝ = 0 a✝
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>v : ι → M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>i : ι<GOAL>e.det v • (Basis.mk hli hsp).coord i = (↑e.det).toLinearMap v i
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>v : ι → M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>i : ι<GOAL>∀ (i_1 : ι), (e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) i_1) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) i_1)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>v : ι → M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>i k : ι<GOAL>(e.det v • (Basis.mk hli hsp).coord i) ((Basis.mk hli hsp) k) = ((↑e.det).toLinearMap v i) ((Basis.mk hli hsp) k)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>v : ι → M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>k : ι<GOAL>e.det v * ((Basis.mk hli hsp).coord k) (v k) = ↑e.det (update v k (v k))
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>M' : Type u_3<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>ι : Type u_4<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>e : Basis ι R M<VAR>A : Type u_5<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Module A M<VAR>v : ι → M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>i k : ι<VAR>hik : k ≠ i<GOAL>e.det v * ((Basis.mk hli hsp).coord i) (v k) = ↑e.det (update v i (v k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : MonotoneOn f s<VAR>h₂ : MonotoneOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<VAR>A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s<VAR>B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t<VAR>x : α<VAR>hx : x ∈ s ∪ t<VAR>y : α<VAR>hy : y ∈ s ∪ t<VAR>hxy : x ≤ y<GOAL>f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : MonotoneOn f s<VAR>h₂ : MonotoneOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<VAR>A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s<VAR>B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t<VAR>x : α<VAR>hx : x ∈ s ∪ t<VAR>y : α<VAR>hy : y ∈ s ∪ t<VAR>hxy : x ≤ y<VAR>hxc : x < c<GOAL>f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>a : α<VAR>f : α → β<VAR>s t : Set α<VAR>c : α<VAR>h₁ : MonotoneOn f s<VAR>h₂ : MonotoneOn f t<VAR>hs : IsGreatest s c<VAR>ht : IsLeast t c<VAR>A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s<VAR>B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t<VAR>x : α<VAR>hx : x ∈ s ∪ t<VAR>y : α<VAR>hy : y ∈ s ∪ t<VAR>hxy : x ≤ y<VAR>hcx : c ≤ x<GOAL>f x ≤ f y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x : A<GOAL>⅟2 • (x - star x) ∈ skewAdjoint A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x y : A<GOAL>↑((fun x => ⟨⅟2 • (x - star x), ⋯⟩) (x + y)) = ↑((fun x => ⟨⅟2 • (x - star x), ⋯⟩) x + (fun x => ⟨⅟2 • (x - star x), ⋯⟩) y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>r : R<VAR>x : A<GOAL>↑({ toFun := fun x => ⟨⅟2 • (x - star x), ⋯⟩, map_add' := ⋯ }.toFun (r • x)) = ↑((RingHom.id R) r • { toFun := fun x => ⟨⅟2 • (x - star x), ⋯⟩, map_add' := ⋯ }.toFun x)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)<VAR>x✝³ : α<VAR>x✝² : Bool<VAR>x✝¹ : α<VAR>x✝ : Bool<GOAL>∃ L₅, Step ([] ++ tl.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)) L₅ ∧ Step ((x✝³, x✝²) :: (x✝³, !x✝²) :: tl ++ x✝⁴) L₅
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ tl x✝⁴ : List (α × Bool)<VAR>x✝³ : α<VAR>x✝² : Bool<VAR>x✝¹ : α<VAR>x✝ : Bool<GOAL>∃ L₅, Step ((x✝¹, x✝) :: (x✝¹, !x✝) :: tl ++ x✝⁴) L₅ ∧ Step ([] ++ tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁴)) L₅
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>x3 : α<VAR>b3 : Bool<VAR>tl x✝⁵ : List (α × Bool)<VAR>x4 : α<VAR>b4 : Bool<VAR>tl2 x✝⁴ : List (α × Bool)<VAR>x✝³ : α<VAR>x✝² : Bool<VAR>x✝¹ : α<VAR>x✝ : Bool<VAR>H : (x3, b3) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = (x4, b4) :: tl2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴<VAR>H1 : (x3, b3) = (x4, b4)<VAR>H2 : tl.append ((x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵) = tl2.append ((x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴)<VAR>L₅ : List (α × Bool)<VAR>H3 : Step (tl ++ x✝⁵) L₅<VAR>H4 : Step (tl2 ++ x✝⁴) L₅<GOAL>Step ((x4, b4) :: tl2 ++ x✝⁴) ((x3, b3) :: L₅)
<VAR>N k m : ℕ<GOAL>m ∈ N.roughNumbersUpTo k ↔ m ∈ (N.succ.primesBelow \ k.primesBelow).biUnion fun p => Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)
<VAR>N k m : ℕ<GOAL>(m < N.succ ∧ m ≠ 0 ∧ ∃ x ≤ m, Prime x ∧ x ∣ m ∧ k ≤ x) ↔ ∃ a, ((a < N.succ ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N.succ ∧ m ≠ 0 ∧ a ∣ m
<VAR>N k m : ℕ<GOAL>(∃ x, m < N.succ ∧ m ≠ 0 ∧ ¬m < x ∧ Prime x ∧ x ∣ m ∧ ¬x < k) ↔ ∃ a, ((a < N.succ ∧ Prime a) ∧ (a < k → ¬Prime a)) ∧ m < N.succ ∧ m ≠ 0 ∧ a ∣ m
<VAR>N k m p : ℕ<GOAL>m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m
<VAR>N k m p : ℕ<VAR>H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ<GOAL>m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m
<VAR>N k m p : ℕ<VAR>H₁ : m ≠ 0 → p ∣ m → m < N.succ → p < N.succ<VAR>H₂ : m ≠ 0 → p ∣ m → ¬m < p<GOAL>m < N.succ ∧ m ≠ 0 ∧ ¬m < p ∧ Prime p ∧ p ∣ m ∧ ¬p < k ↔ ((p < N.succ ∧ Prime p) ∧ (p < k → ¬Prime p)) ∧ m < N.succ ∧ m ≠ 0 ∧ p ∣ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : LinearOrderedCommSemiring β<VAR>inst✝¹ : ExistsAddOfLE β<VAR>f f₁ f₂ f₃ f₄ g μ : α → β<VAR>inst✝ : Fintype α<VAR>h₁ : 0 ≤ f₁<VAR>h₂ : 0 ≤ f₂<VAR>h₃ : 0 ≤ f₃<VAR>h₄ : 0 ≤ f₄<VAR>h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)<GOAL>(∑ a : α, f₁ a) * ∑ a : α, f₂ a ≤ (∑ a : α, f₃ a) * ∑ a : α, f₄ a
<VAR>R : Type u_1<VAR>inst✝¹⁷ : CommSemiring R<VAR>S : Submonoid R<VAR>M✝ : Type u_2<VAR>M'✝ : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : AddCommMonoid M'✝<VAR>inst✝¹⁴ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝¹³ : CommSemiring A<VAR>inst✝¹² : Algebra R A<VAR>inst✝¹¹ : Module A M'✝<VAR>inst✝¹⁰ : IsLocalization S A<VAR>inst✝⁹ : Module R M✝<VAR>inst✝⁸ : Module R M'✝<VAR>inst✝⁷ : Module R M''<VAR>inst✝⁶ : IsScalarTower R A M'✝<VAR>f✝ : M✝ →ₗ[R] M'✝<VAR>g : M✝ →ₗ[R] M''<VAR>inst✝⁵ : IsLocalizedModule S f✝<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : (↑f'symm.nnnorm)⁻¹ ≤ ↑c<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<GOAL>y ∈ f '' closedBall b ε