ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a / d < b / c
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a * c < b * d
<VAR>α' : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>inst✝¹ : DecidableEq α'<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>g : α' ≃ α<VAR>a : α<VAR>v : β<GOAL>update f a v ∘ ⇑g = update (f ∘ ⇑g) (g.symm a) v
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a b : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>padicValNat p (a * b).natAbs = padicValNat p a.natAbs + padicValNat p b.natAbs
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond' : f ≫ g = 0<GOAL>f ≫ g ≫ h = 0
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond' : f ≫ g = 0<GOAL>explicitCokernelDesc cond' ≫ h = explicitCokernelDesc ⋯
<VAR>X Y Z W : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<VAR>cond' : f ≫ g = 0<GOAL>explicitCokernelπ f ≫ explicitCokernelDesc cond' ≫ h = g ≫ h
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>f : M →ₗ[R] M<VAR>n : ℕ<GOAL>rTensor N f ^ n = rTensor N (f ^ n)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f✝ : N →ₗ[R] P<VAR>f : M →ₗ[R] M<VAR>n : ℕ<VAR>h : map f id ^ n = map (f ^ n) (id ^ n)<GOAL>rTensor N f ^ n = rTensor N (f ^ n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.3959, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<GOAL>S.Exact ↔ IsZero h.left.H
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.3959, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<VAR>this : S.HasHomology<GOAL>S.Exact ↔ IsZero h.left.H
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ x₂ x₃ : X<VAR>p₀ q₀ : Path x₀ x₁<VAR>p₁ q₁ : Path x₁ x₂<VAR>F : p₀.Homotopy q₀<VAR>G : p₁.Homotopy q₁<VAR>x : ↑I × ↑I<GOAL>(if ↑x.2 ≤ 1 / 2 then (F.eval x.1).extend (2 * ↑x.2) else (G.eval x.1).extend (2 * ↑x.2 - 1)) = if h : ↑x.2 ≤ 1 / 2 then (F.eval x.1) ⟨2 * ↑x.2, ⋯⟩ else (G.eval x.1) ⟨2 * ↑x.2 - 1, ⋯⟩
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : CompleteLattice ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ι m<VAR>ω : Ω<GOAL>hitting u s ⊥ ⊤ ω = sInf {i | u i ω ∈ s}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : CompleteLattice ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ι m<VAR>ω : Ω<GOAL>(∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)) → ⊤ = sInf {i | u i ω ∈ s}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : CompleteLattice ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ι m<VAR>ω : Ω<VAR>h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)<GOAL>sInf {i | u i ω ∈ s} = ⊤
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : CompleteLattice ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ι m<VAR>ω : Ω<VAR>h_nmem_s : ∀ (x : ι), ¬(x ∈ Set.univ ∧ u x ω ∈ s)<GOAL>∀ a ∈ {i | u i ω ∈ s}, a = ⊤
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : CompleteLattice ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>f : Filtration ι m<VAR>ω : Ω<VAR>h_nmem_s : ∀ (x : ι), u x ω ∉ s<GOAL>∀ a ∈ {i | u i ω ∈ s}, a = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b a : α<VAR>s : Set α<GOAL>lowerBounds (insert a s) = Iic a ∩ lowerBounds s
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : WellPowered C<VAR>inst✝ : HasWidePullbacks C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>hf : f ∈ s<GOAL>sInf s ≤ f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : WellPowered C<VAR>inst✝ : HasWidePullbacks C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>hf : f ∈ s<GOAL>underlying.obj (sInf s) ⟶ underlying.obj f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : WellPowered C<VAR>inst✝ : HasWidePullbacks C<VAR>A : C<VAR>s : Set (Subobject A)<VAR>f : Subobject A<VAR>hf : f ∈ s<GOAL>?f ≫ f.arrow = (sInf s).arrow
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : NormalizationMonoid α<VAR>inst✝² : UniqueFactorizationMonoid α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : Unique αˣ<VAR>m : Multiset α<VAR>h : ∀ p ∈ m, Prime p<GOAL>normalizedFactors m.prod = m
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x < y ^ z⁻¹ ↔ x ^ z < y
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>⨅ r, ↑f ↑↑r = ↑f x
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>⨅ r, ↑f ↑↑r = ⨅ r, ↑f ↑r
<VAR>f✝ f : StieltjesFunction<VAR>x : ℝ<GOAL>BddBelow (↑f '' Ioi x)
<VAR>f✝ f : StieltjesFunction<VAR>x y : ℝ<VAR>hy_mem : y ∈ Ioi x<GOAL>↑f x ≤ ↑f y
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : DecidableEq G<VAR>f : G →* R<VAR>hf : Injective ⇑f<VAR>n : ℕ<VAR>hn : 0 < n<VAR>g₀ : G<VAR>this : DecidableEq R<GOAL>(filter (fun g => g ^ n = g₀) univ).card ≤ Multiset.card (nthRoots n (f g₀))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>a : α<GOAL>comap (fun x => (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>a : α<GOAL>Function.Injective fun x => (x.1 * a, x.2 * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>a p₁ p₂ q₁ q₂ : α<GOAL>(fun x => (x.1 * a, x.2 * a)) (p₁, p₂) = (fun x => (x.1 * a, x.2 * a)) (q₁, q₂) → (p₁, p₂) = (q₁, q₂)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>ι : Sort u_4<VAR>p : ι → Submonoid M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>ι : Sort u_4<VAR>p : ι → Submonoid M<VAR>m : M<GOAL>(∀ (b : Submonoid M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>i : Nat<VAR>α✝ : Type u_1<VAR>xs : List α✝<VAR>j : Nat<VAR>h₀ : i < xs.length<VAR>h₁ : xs.Nodup<VAR>h₂ : xs.get? i = xs.get? j<GOAL>i = j
<VAR>i : Nat<VAR>α✝ : Type u_1<VAR>xs : List α✝<VAR>j : Nat<VAR>h₀ : i < xs.length<VAR>h₁ : xs.Nodup<VAR>h₂ : xs.get? i = xs.get? j<GOAL>xs[i]? = xs[j]?
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ f, s ⊆ ⋃ n, U (f n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>c : Set ι<VAR>c_count : c.Countable<VAR>c_cov : s ⊆ ⋃ i ∈ c, U i<GOAL>∃ f, s ⊆ ⋃ n, U (f n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>c_count : ∅.Countable<VAR>c_cov : s ⊆ ⋃ i ∈ ∅, U i<GOAL>∃ f, s ⊆ ⋃ n, U (f n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>c : Set ι<VAR>c_count : c.Countable<VAR>c_cov : s ⊆ ⋃ i ∈ c, U i<VAR>c_nonempty : c.Nonempty<GOAL>∃ f, s ⊆ ⋃ n, U (f n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>c : Set ι<VAR>c_count : c.Countable<VAR>c_cov : s ⊆ ⋃ i ∈ c, U i<VAR>c_nonempty : c.Nonempty<VAR>f : ℕ → ↑c<VAR>f_surj : Function.Surjective f<GOAL>∃ f, s ⊆ ⋃ n, U (f n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>c : Set ι<VAR>c_count : c.Countable<VAR>c_cov : s ⊆ ⋃ i ∈ c, U i<VAR>c_nonempty : c.Nonempty<VAR>f : ℕ → ↑c<VAR>f_surj : Function.Surjective f<GOAL>∀ i ∈ c, U i ⊆ ⋃ n, U ↑(f n)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>ι : Type v<VAR>inst✝ : Nonempty ι<VAR>hs : IsLindelof s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>c : Set ι<VAR>c_count : c.Countable<VAR>c_cov : s ⊆ ⋃ i ∈ c, U i<VAR>c_nonempty : c.Nonempty<VAR>f : ℕ → ↑c<VAR>f_surj : Function.Surjective f<VAR>x : ι<VAR>hx : x ∈ c<VAR>n : ℕ<VAR>hn : f n = ⟨x, hx⟩<GOAL>U x ⊆ ⋃ n, U ↑(f n)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>Multiset.map (⇑f) p.roots = (map f p).roots
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>hroots : Multiset.card p.roots = p.natDegree<GOAL>Multiset.card (map f p).roots ≤ Multiset.card (Multiset.map (⇑f) p.roots)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B' I J D X : Set α<VAR>e f : α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>¬M.Indep X ↔ M.Dep X
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq : ℝ≥0<VAR>rq_pos : 0 < ↑rq<VAR>hrq : ↑rq < min 1 q.radius<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq : ℝ≥0<VAR>rq_pos : 0 < ↑rq<VAR>hrq : ↑rq < min 1 q.radius<VAR>rp : ℝ≥0<VAR>rp_pos : 0 < ↑rp<VAR>hrp : ↑rp < min 1 p.radius<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<GOAL>∃ r > 0, Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<GOAL>Summable fun b => Cq / 4 ^ b.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<GOAL>Summable fun b => Cq * (4 ^ b.fst)⁻¹
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<GOAL>Summable fun b => (4 ^ b.fst)⁻¹
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>hq : 0 < q.radius<VAR>hp : 0 < p.radius<VAR>rq rp : ℝ≥0<VAR>hrp : rp < 1 ∧ ↑rp < p.radius<VAR>hrq : rq < 1 ∧ ↑rq < q.radius<VAR>rp_pos : 0 < rp<VAR>rq_pos : 0 < rq<VAR>Cq : ℝ≥0<VAR>_hCq0 : Cq > 0<VAR>hCq : ∀ (n : ℕ), ‖q n‖₊ * rq ^ n ≤ Cq<VAR>Cp : ℝ≥0<VAR>hCp1 : Cp ≥ 1<VAR>hCp : ∀ (n : ℕ), ‖p n‖₊ * rp ^ n ≤ Cp<VAR>r0 : ℝ≥0 := (4 * Cp)⁻¹<VAR>r0_pos : 0 < r0<VAR>r : ℝ≥0 := rp * rq * r0<VAR>r_pos : 0 < r<VAR>I : ∀ (i : (n : ℕ) × Composition n), ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst ≤ Cq / 4 ^ i.fst<VAR>this : ∀ (n : ℕ), HasSum (fun c => (4 ^ n)⁻¹) (2 ^ (n - 1) / 4 ^ n)<GOAL>Summable fun b => (4 ^ b.fst)⁻¹