ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<GOAL>HasFDerivAt b (h.deriv p) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>u : Set (E × F)<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<GOAL>HasFDerivWithinAt b (h.deriv p) u p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<GOAL>DifferentiableAt 𝕜 b p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>u : Set (E × F)<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<GOAL>DifferentiableWithinAt 𝕜 b u p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<GOAL>fderiv 𝕜 b p = h.deriv p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>u : Set (E × F)<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<VAR>hxs : UniqueDiffWithinAt 𝕜 u p<GOAL>fderivWithin 𝕜 b u p = h.deriv p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 b<GOAL>Differentiable 𝕜 b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>u : Set (E × F)<VAR>h : IsBoundedBilinearMap 𝕜 b<GOAL>DifferentiableOn 𝕜 b u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : G' → E<VAR>g : G' → F<VAR>f' : G' →L[𝕜] E<VAR>g' : G' →L[𝕜] F<VAR>x : G'<VAR>s : Set G'<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt g g' s x<GOAL>HasFDerivWithinAt (fun y => (B (f y)) (g y)) (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.precompL G' B) f') (g x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : G' → E<VAR>g : G' → F<VAR>f' : G' →L[𝕜] E<VAR>g' : G' →L[𝕜] F<VAR>x : G'<VAR>hf : HasFDerivAt f f' x<VAR>hg : HasFDerivAt g g' x<GOAL>HasFDerivAt (fun y => (B (f y)) (g y)) (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.precompL G' B) f') (g x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : G' → E<VAR>g : G' → F<VAR>f' : G' →L[𝕜] E<VAR>g' : G' →L[𝕜] F<VAR>x : G'<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<GOAL>HasStrictFDerivAt (fun y => (B (f y)) (g y)) (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.precompL G' B) f') (g x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : G' → E<VAR>g : G' → F<VAR>x : G'<VAR>s : Set G'<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hg : DifferentiableWithinAt 𝕜 g s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun y => (B (f y)) (g y)) s x = ((ContinuousLinearMap.precompR G' B) (f x)) (fderivWithin 𝕜 g s x) + ((ContinuousLinearMap.precompL G' B) (fderivWithin 𝕜 f s x)) (g x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : G' → E<VAR>g : G' → F<VAR>x : G'<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>fderiv 𝕜 (fun y => (B (f y)) (g y)) x = ((ContinuousLinearMap.precompR G' B) (f x)) (fderiv 𝕜 g x) + ((ContinuousLinearMap.precompL G' B) (fderiv 𝕜 f x)) (g x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<GOAL>dslope f a a = deriv f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : 𝕜<VAR>f : 𝕜 → E<VAR>h : b ≠ a<GOAL>dslope f a b = slope f a b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E →L[𝕜] F<VAR>g : 𝕜 → E<VAR>a b : 𝕜<VAR>H : a = b → DifferentiableAt 𝕜 g a<GOAL>dslope (⇑f ∘ g) a b = f (dslope g a b)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<GOAL>Set.EqOn (dslope f a) (slope f a) {a}ᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : 𝕜<VAR>f : 𝕜 → E<VAR>h : b ≠ a<GOAL>dslope f a =ᶠ[𝓝 b] slope f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a : 𝕜<VAR>f : 𝕜 → E<GOAL>dslope f a =ᶠ[𝓝[≠] a] slope f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<GOAL>(b - a) • dslope f a b = f b - f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>a b : 𝕜<VAR>f : 𝕜 → E<VAR>h : b ≠ a<GOAL>dslope (fun x => (x - a) • f x) a b = f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<GOAL>Set.EqOn (dslope (fun x => (x - a) • f x) a) f {a}ᶜ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>DecidableEq 𝕜<VAR>f : 𝕜 → E<VAR>a : 𝕜<GOAL>dslope (fun x => (x - a) • f x) a = Function.update f a (deriv (fun x => (x - a) • f x) a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<GOAL>ContinuousAt (dslope f a) a ↔ DifferentiableAt 𝕜 f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : ContinuousWithinAt (dslope f a) s b<GOAL>ContinuousWithinAt f s b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>h : ContinuousAt (dslope f a) b<GOAL>ContinuousAt f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<VAR>s : Set 𝕜<VAR>h : ContinuousOn (dslope f a) s<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<GOAL>ContinuousWithinAt (dslope f a) s b ↔ ContinuousWithinAt f s b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>h : b ≠ a<GOAL>ContinuousAt (dslope f a) b ↔ ContinuousAt f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<VAR>s : Set 𝕜<VAR>h : s ∈ 𝓝 a<GOAL>ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : DifferentiableWithinAt 𝕜 (dslope f a) s b<GOAL>DifferentiableWithinAt 𝕜 f s b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>h : DifferentiableAt 𝕜 (dslope f a) b<GOAL>DifferentiableAt 𝕜 f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<VAR>s : Set 𝕜<VAR>h : DifferentiableOn 𝕜 (dslope f a) s<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<GOAL>DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a : 𝕜<VAR>s : Set 𝕜<VAR>h : a ∉ s<GOAL>DifferentiableOn 𝕜 (dslope f a) s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>h : b ≠ a<GOAL>DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>self : DiffContOnCl 𝕜 f s<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>self : DiffContOnCl 𝕜 f s<GOAL>ContinuousOn f (closure s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f (closure s)<GOAL>DiffContOnCl 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : Differentiable 𝕜 f<GOAL>DiffContOnCl 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsClosed s<GOAL>DiffContOnCl 𝕜 f s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>DiffContOnCl 𝕜 f Set.univ ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>c : F<GOAL>DiffContOnCl 𝕜 (fun x => c) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>s : Set E<VAR>g : G → E<VAR>t : Set G<VAR>hf : DiffContOnCl 𝕜 f s<VAR>hg : DiffContOnCl 𝕜 g t<VAR>h : Set.MapsTo g t s<GOAL>DiffContOnCl 𝕜 (f ∘ g) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>h : DiffContOnCl 𝕜 f (Metric.ball x r)<GOAL>ContinuousOn f (Metric.closedBall x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>r : ℝ<VAR>hd : DifferentiableOn 𝕜 f (Metric.ball x r)<VAR>hc : ContinuousOn f (Metric.closedBall x r)<GOAL>DiffContOnCl 𝕜 f (Metric.ball x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : DiffContOnCl 𝕜 f s<VAR>hs : IsOpen s<VAR>hx : x ∈ s<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : DiffContOnCl 𝕜 f s<VAR>hx : s ∈ 𝓝 x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s t : Set E<VAR>h : DiffContOnCl 𝕜 f s<VAR>ht : t ⊆ s<GOAL>DiffContOnCl 𝕜 f t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<VAR>hg : DiffContOnCl 𝕜 g s<GOAL>DiffContOnCl 𝕜 (f + g) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<VAR>c : F<GOAL>DiffContOnCl 𝕜 (fun x => f x + c) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<VAR>c : F<GOAL>DiffContOnCl 𝕜 (fun x => c + f x) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<GOAL>DiffContOnCl 𝕜 (-f) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f g : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<VAR>hg : DiffContOnCl 𝕜 g s<GOAL>DiffContOnCl 𝕜 (f - g) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<VAR>c : F<GOAL>DiffContOnCl 𝕜 (fun x => f x - c) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>hf : DiffContOnCl 𝕜 f s<VAR>c : F<GOAL>DiffContOnCl 𝕜 (fun x => c - f x) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>R : Type u_5<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>hf : DiffContOnCl 𝕜 f s<VAR>c : R<GOAL>DiffContOnCl 𝕜 (c • f) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>𝕜' : Type u_5<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>f : E → F<VAR>s : Set E<VAR>hc : DiffContOnCl 𝕜 c s<VAR>hf : DiffContOnCl 𝕜 f s<GOAL>DiffContOnCl 𝕜 (fun x => c x • f x) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>𝕜' : Type u_5<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>s : Set E<VAR>hc : DiffContOnCl 𝕜 c s<VAR>y : F<GOAL>DiffContOnCl 𝕜 (fun x => c x • y) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>f : E → 𝕜<VAR>hf : DiffContOnCl 𝕜 f s<VAR>h₀ : ∀ x ∈ closure s, f x ≠ 0<GOAL>DiffContOnCl 𝕜 f⁻¹ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>g : G → E<VAR>t : Set G<VAR>hf : Differentiable 𝕜 f<VAR>hg : DiffContOnCl 𝕜 g t<GOAL>DiffContOnCl 𝕜 (f ∘ g) t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>U : Set E<VAR>c : E<VAR>R : ℝ<VAR>hf : DifferentiableOn 𝕜 f U<VAR>hc : Metric.closedBall c R ⊆ U<GOAL>DiffContOnCl 𝕜 f (Metric.ball c R)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Set.Ioo a b, g' x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Set.Ico a b)<VAR>hcg : ContinuousOn g (Set.Ico a b)<VAR>hg' : ∀ x ∈ Set.Ioo a b, g' x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Set.Ioo a b, g' x ≠ 0<VAR>hfb : Filter.Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Filter.Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Set.Ioc a b)<VAR>hcg : ContinuousOn g (Set.Ioc a b)<VAR>hg' : ∀ x ∈ Set.Ioo a b, g' x ≠ 0<VAR>hfb : f b = 0<VAR>hgb : g b = 0<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[<] b) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Set.Ioi a, g' x ≠ 0<VAR>hftop : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>hgtop : Filter.Tendsto g Filter.atTop (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) Filter.atTop l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atTop l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Set.Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Set.Iio a, g' x ≠ 0<VAR>hfbot : Filter.Tendsto f Filter.atBot (𝓝 0)<VAR>hgbot : Filter.Tendsto g Filter.atBot (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) Filter.atBot l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Set.Ioo a b)<VAR>hg' : ∀ x ∈ Set.Ioo a b, deriv g x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Set.Ioo a b)<VAR>hcf : ContinuousOn f (Set.Ico a b)<VAR>hcg : ContinuousOn g (Set.Ico a b)<VAR>hg' : ∀ x ∈ Set.Ioo a b, deriv g x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Set.Ioo a b)<VAR>hg' : ∀ x ∈ Set.Ioo a b, deriv g x ≠ 0<VAR>hfb : Filter.Tendsto f (𝓝[<] b) (𝓝 0)<VAR>hgb : Filter.Tendsto g (𝓝[<] b) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] b) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[<] b) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Set.Ioi a)<VAR>hg' : ∀ x ∈ Set.Ioi a, deriv g x ≠ 0<VAR>hftop : Filter.Tendsto f Filter.atTop (𝓝 0)<VAR>hgtop : Filter.Tendsto g Filter.atTop (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atTop l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atTop l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f g : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Set.Iio a)<VAR>hg' : ∀ x ∈ Set.Iio a, deriv g x ≠ 0<VAR>hfbot : Filter.Tendsto f Filter.atBot (𝓝 0)<VAR>hgbot : Filter.Tendsto g Filter.atBot (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => deriv f x / deriv g x) Filter.atBot l<GOAL>Filter.Tendsto (fun x => f x / g x) Filter.atBot l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[>] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[>] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[<] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[<] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[<] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[<] a) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝[≠] a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝[≠] a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝[≠] a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[≠] a) l
<VAR>a : ℝ<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x<VAR>hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0<VAR>hfa : Filter.Tendsto f (𝓝 a) (𝓝 0)<VAR>hga : Filter.Tendsto g (𝓝 a) (𝓝 0)<VAR>hdiv : Filter.Tendsto (fun x => f' x / g' x) (𝓝 a) l<GOAL>Filter.Tendsto (fun x => f x / g x) (𝓝[≠] a) l