ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>hH : Group.IsNilpotent G<VAR>inst✝ : Nontrivial G<GOAL>Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ center G) + 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>hH : Group.IsNilpotent G<VAR>inst✝ : Nontrivial G<GOAL>Group.nilpotencyClass G = Group.nilpotencyClass G - 1 + 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>A : C<VAR>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h₁ : IsIso (cyclesMap φ)<VAR>h₂ : Epi φ.τ₁<GOAL>IsIso (homologyMap φ)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>A : C<VAR>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h₁ : IsIso (cyclesMap φ)<VAR>h₂ : Epi φ.τ₁<VAR>h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0<GOAL>IsIso (homologyMap φ)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hJ : M.Basis J X<GOAL>∃ I', M.Basis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hJ : M.Basis J X<VAR>I' : Set α<VAR>hI' : (M ↾ X).Base I'<VAR>hII' : I ⊆ I'<VAR>hI'IJ : I' ⊆ I ∪ J<GOAL>∃ I', M.Basis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Indep I<VAR>hIX : I ⊆ X<VAR>hJ : M.Basis J X<VAR>I' : Set α<VAR>hI' : M.Basis I' X<VAR>hII' : I ⊆ I'<VAR>hI'IJ : I' ⊆ I ∪ J<GOAL>∃ I', M.Basis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
<VAR>p q✝ q : ℚ≥0<GOAL>q.num.Coprime q.den
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : DecidableEq P<VAR>p : ι → P<VAR>s : Finset ι<VAR>n : ℕ<VAR>hc : s.card = n + 1<GOAL>finrank k ↥(vectorSpan k ↑(Finset.image p s)) ≤ n
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * sinh x ^ 3 + 3 * sinh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<GOAL>sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2<GOAL>sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x
<VAR>x y : ℂ<VAR>h1 : x + 2 * x = 3 * x<VAR>h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2<GOAL>sinh x * (sinh x ^ 2 + 1 + sinh x ^ 2) + 2 * sinh x * (sinh x ^ 2 + 1) = 4 * sinh x ^ 3 + 3 * sinh x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ x ∈ s, ‖x‖ ≤ r
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>x • ↑y = ↑(x * y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<GOAL>liminf (fun n => (preimage f)^[n] s) atTop =ᵐ[μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<GOAL>limsup (compl ∘ fun n => (preimage f)^[n] s) atTop =ᵐ[μ] sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' sᶜ =ᵐ[μ] sᶜ<GOAL>limsup (compl ∘ fun n => (preimage f)^[n] s) atTop =ᵐ[μ] sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' sᶜ =ᵐ[μ] sᶜ<VAR>x✝ : ℕ<GOAL>(compl ∘ fun n => (preimage f)^[n] s) x✝ = (preimage f)^[x✝] sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' sᶜ =ᵐ[μ] sᶜ<VAR>x✝ : ℕ<VAR>n : α<GOAL>n ∈ (compl ∘ fun n => (preimage f)^[n] s) x✝ ↔ n ∈ (preimage f)^[x✝] sᶜ
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>F : J ⥤ C<VAR>inst✝² : HasLimit F<VAR>G : C ⥤ D<VAR>inst✝¹ : HasLimit (F ⋙ G)<VAR>E : Type u''<VAR>inst✝ : Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : HasLimit ((F ⋙ G) ⋙ H)<VAR>this : HasLimit (F ⋙ G ⋙ H)<VAR>j✝ : J<GOAL>(H.map (post F G) ≫ post (F ⋙ G) H) ≫ π ((F ⋙ G) ⋙ H) j✝ = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
<VAR>J : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>F : J ⥤ C<VAR>inst✝² : HasLimit F<VAR>G : C ⥤ D<VAR>inst✝¹ : HasLimit (F ⋙ G)<VAR>E : Type u''<VAR>inst✝ : Category.{v'', u''} E<VAR>H : D ⥤ E<VAR>h : HasLimit ((F ⋙ G) ⋙ H)<VAR>this : HasLimit (F ⋙ G ⋙ H)<VAR>j✝ : J<GOAL>H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hq : q.Monic<VAR>hpq : (p * q).Monic<GOAL>p.Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hq : q.Monic<VAR>hpq : ¬p.Monic<GOAL>¬(p * q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hq : q.Monic<VAR>hpq : ¬p.leadingCoeff = 1<GOAL>¬(p * q).leadingCoeff = 1
<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 : α → ℝ<VAR>h : 0 ≤ᶠ[ae μ] f<GOAL>HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ < ⊤
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<GOAL>‖f m‖ ≤ ‖f‖ * ∏ x : ι, ‖m x‖
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<GOAL>(HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<GOAL>Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory C c)
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<GOAL>Localization.StrictUniversalPropertyFixedTarget (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomologicalComplex.homotopyEquivalences C c).Localization
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>s.card ≤ n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>s : Finset V<VAR>h : G.IsClique ↑s<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>n = card (Fin n)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ✝ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ n<VAR>m : ℕ<GOAL>((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>b c : Ordinal.{u_4}<VAR>h : c ≠ 0<GOAL>0 < b / c ↔ c ≤ b
<VAR>R : Type u<VAR>inst✝ : LinearOrder R<VAR>a b : Tropical (WithTop R)<GOAL>a + b = 0 ↔ a = 0 ∧ b = 0
<VAR>R : Type u<VAR>inst✝ : LinearOrder R<VAR>a b : Tropical (WithTop R)<GOAL>a = 0 ∧ a ≤ b ∨ b = 0 ∧ b ≤ a ↔ a = 0 ∧ b = 0
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n
<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>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>s : Set E<VAR>t : Set F<VAR>x : E<VAR>N : ℕ∞<VAR>hg : ContDiffOn 𝕜 N g t<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hn : ↑n ≤ N<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hst : MapsTo f s t<VAR>hx : x ∈ s<VAR>C D : ℝ<VAR>Fu : Type (max uF uG) := ULift.{uG, uF} F<VAR>Gu : Type (max uF uG) := ULift.{uF, uG} G<VAR>isoF : Fu ≃ₗᵢ[𝕜] F<VAR>isoG : Gu ≃ₗᵢ[𝕜] G<VAR>fu : E → Fu := ⇑isoF.symm ∘ f<VAR>gu : Fu → Gu := ⇑isoG.symm ∘ g ∘ ⇑isoF<VAR>tu : Set Fu := ⇑isoF ⁻¹' t<VAR>htu : UniqueDiffOn 𝕜 tu<VAR>hstu : MapsTo fu s tu<VAR>Ffu : isoF (fu x) = f x<VAR>hfu : ContDiffOn 𝕜 (↑n) fu s<VAR>hgu : ContDiffOn 𝕜 (↑n) gu tu<VAR>Nfu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i fu s x‖ ≤ D ^ i<VAR>Ngu : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ ≤ C<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n ! * C * D ^ n