ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu✝ : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<VAR>hgu : ContDiffOn 𝕜 (↑n) gu su<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>B : E →L[𝕜] F →L[𝕜] G<VAR>f : D → E<VAR>g : D → F<VAR>N : ℕ∞<VAR>s : Set D<VAR>x : D<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : ↑n ≤ N<VAR>Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D<VAR>Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E<VAR>Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F<VAR>Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G<VAR>isoD : Du ≃ₗᵢ[𝕜] D<VAR>isoE : Eu ≃ₗᵢ[𝕜] E<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>hfu✝ : fu = ⇑isoE.symm ∘ f ∘ ⇑isoD<VAR>gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>hgu✝ : gu = ⇑isoF.symm ∘ g ∘ ⇑isoD<VAR>Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>hBu₀ : Bu₀ = ((B.comp ↑{ toLinearEquiv := isoE.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip.comp ↑{ toLinearEquiv := isoF.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).flip<VAR>Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑{ toLinearEquiv := isoG.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })) Bu₀<VAR>Bu_eq : (fun y => (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y => (B (f y)) (g y)) ∘ ⇑isoD<VAR>Bu_le : ‖Bu‖ ≤ ‖B‖<VAR>su : Set Du := ⇑isoD ⁻¹' s<VAR>hsu : UniqueDiffOn 𝕜 su<VAR>xu : Du := isoD.symm x<VAR>hxu : xu ∈ su<VAR>xu_x : isoD xu = x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu su<VAR>hgu : ContDiffOn 𝕜 (↑n) gu su<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu su xu‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖