ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>P✝ Q✝ R✝ : Algebra F<VAR>f✝ f'✝ : P✝ ⟶ Q✝<VAR>g✝ : Q✝ ⟶ R✝<GOAL>((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>F : C ⥤ C<VAR>inst✝ : F.Additive<VAR>P✝ Q✝ R✝ : Algebra F<VAR>f✝ : P✝ ⟶ Q✝<VAR>g✝ g'✝ : Q✝ ⟶ R✝<GOAL>(f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a✝ b✝ : α<VAR>inst✝ : LE α<VAR>a : α<VAR>b : WithBot α<VAR>h : b ≠ ⊥<GOAL>a ≤ b.unbot h ↔ ↑a ≤ b
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : γ → α<VAR>t : Finset γ<GOAL>R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m✝ m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : T2Space M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : Countable β<VAR>inst✝ : CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : γ → α<VAR>t : Finset γ<GOAL>R (m (⨆ x, s ↑x)) (∏' (x : { x // x ∈ t }), m (s ↑x))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>γ : Type u_5<VAR>x : X<VAR>y : Y<VAR>f : Filter γ<VAR>mx : γ → X<VAR>my : γ → Y<VAR>hx : Tendsto mx f (𝓝 x)<VAR>hy : Tendsto my f (𝓝 y)<GOAL>Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>γ : Type u_5<VAR>x : X<VAR>y : Y<VAR>f : Filter γ<VAR>mx : γ → X<VAR>my : γ → Y<VAR>hx : Tendsto mx f (𝓝 x)<VAR>hy : Tendsto my f (𝓝 y)<GOAL>Tendsto (fun c => (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Group M<VAR>inst✝ : MulAction M α<VAR>s : Set α<VAR>m : M<GOAL>m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : HasGroupoid M (contDiffGroupoid 0 I)<VAR>inst✝¹ : LocallyCompactSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>LocallyCompactSpace M
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : HasGroupoid M (contDiffGroupoid 0 I)<VAR>inst✝¹ : LocallyCompactSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>this : ProperSpace E<GOAL>LocallyCompactSpace M
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : HasGroupoid M (contDiffGroupoid 0 I)<VAR>inst✝¹ : LocallyCompactSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>this✝ : ProperSpace E<VAR>this : LocallyCompactSpace H<GOAL>LocallyCompactSpace M
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s✝ s : Set G<VAR>N : Subgroup G<VAR>hN : N.Normal<GOAL>s * ↑N = ↑N * s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s✝ s : Set G<VAR>N : Subgroup G<VAR>hN : N.Normal<GOAL>⋃ a ∈ s, (fun x => a * x) '' ↑N = ⋃ a ∈ s, (fun x => x * a) '' ↑N
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>inst✝ : Algebra.IsSeparable F E<VAR>h : LinearIndependent F v<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>l : Filter α<GOAL>l ≤ comap f ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l✝ f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>l : Filter α<GOAL>l ≤ ⊤
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>b c : α<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<GOAL>(b :: c :: l₁ ++ a :: l₂).getLast? = (a :: l₂).getLast?
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>htu : Disjoint t u<GOAL>(condCount s) (t ∪ u) = (condCount s) t + (condCount s) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>htu : Disjoint t u<GOAL>Disjoint (s ∩ t) (s ∩ u)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>htu : Disjoint t u<GOAL>MeasurableSet (s ∩ u)
<VAR>a : ℝ<GOAL>frontier {z | a ≤ z.re} = {z | z.re = a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>e : Equiv.Perm α<VAR>f : α ↪ β<VAR>a : α<GOAL>f.toEquivRange.symm ⟨f a, ⋯⟩ = a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝² : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝¹ : F.PreservesMonomorphisms<VAR>I : D<VAR>hI : Injective I<VAR>X Y : C<VAR>f : X ⟶ G.obj I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<GOAL>∃ h, g ≫ h = f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝² : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝¹ : F.PreservesMonomorphisms<VAR>I : D<VAR>hI : Injective I<VAR>X Y : C<VAR>f : X ⟶ G.obj I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<VAR>w : F.obj Y ⟶ I<VAR>h : F.map g ≫ w = F.map f ≫ adj.counit.app I<GOAL>∃ h, g ≫ h = f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝² : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝¹ : F.PreservesMonomorphisms<VAR>I : D<VAR>hI : Injective I<VAR>X Y : C<VAR>f : X ⟶ G.obj I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<VAR>w : F.obj Y ⟶ I<VAR>h : F.map g ≫ w = F.map f ≫ adj.counit.app I<GOAL>g ≫ adj.unit.app Y ≫ G.map w = f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>inst✝² : Category.{u_2, u_1} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝¹ : F.PreservesMonomorphisms<VAR>I : D<VAR>hI : Injective I<VAR>X Y : C<VAR>f : X ⟶ G.obj I<VAR>g : X ⟶ Y<VAR>inst✝ : Mono g<VAR>w : F.obj Y ⟶ I<VAR>h : F.map g ≫ w = F.map f ≫ adj.counit.app I<GOAL>adj.unit.app X ≫ G.map (F.map f ≫ adj.counit.app I) = f
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(d.sum fun x e => e) ≤ n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>(d.sum fun x e => e) ≤ n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>∑ a ∈ d.support, d a ≤ d.sum fun i c => c • 1 i
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>∑ a ∈ d.support, d a ≤ d.sum fun i c => c
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>⋃₀ ↑(hC.diffFinset hs ht) = s \ t
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>w w' : InfinitePlace K<GOAL>w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>w w' : InfinitePlace K<GOAL>w' ∈ MulAction.orbit (K ≃ₐ[k] K) w → w.comap (algebraMap k K) = w'.comap (algebraMap k K)
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>w : InfinitePlace K<VAR>σ : K ≃ₐ[k] K<GOAL>w.comap (algebraMap k K) = (σ • w).comap (algebraMap k K)
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ✝ : K ≃ₐ[k] K<VAR>w✝ : InfinitePlace K<VAR>inst✝ : IsGalois k K<VAR>w : InfinitePlace K<VAR>σ : K ≃ₐ[k] K<GOAL>mk (w.embedding.comp (algebraMap k K)) = mk ((w.embedding.comp ↑σ.symm).comp (algebraMap k K))
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
<VAR>b : ℕ<VAR>hb : 1 < b<GOAL>Int.gcd 0 ↑b ≠ 1
<VAR>b : ℕ<VAR>hb : 1 < b<GOAL>b ≠ 1
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x} * closedBall y δ = closedBall (x * y) δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>c : 𝕜<VAR>g : α → 𝕜<VAR>hc : c ≠ 0<GOAL>(f =Θ[l] fun x => c * g x) ↔ f =Θ[l] g
<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✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 1 → E<GOAL>(q.comp p 1) v = (q 1) fun _i => (p 1) v
<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✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 1 → E<VAR>this : {Composition.ones 1} = Finset.univ<GOAL>(q.comp p 1) v = (q 1) fun _i => (p 1) v
<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✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 1 → E<VAR>this : {Composition.ones 1} = Finset.univ<GOAL>(q (Composition.ones 1).length) (p.applyComposition (Composition.ones 1) v) = (q 1) fun _i => (p 1) v
<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✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 1 → E<VAR>this : {Composition.ones 1} = Finset.univ<VAR>i : ℕ<VAR>hi1 : i < (Composition.ones 1).length<VAR>hi2 : i < 1<GOAL>p.applyComposition (Composition.ones 1) v ⟨i, hi1⟩ = (p 1) v
<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✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 1 → E<VAR>this : {Composition.ones 1} = Finset.univ<VAR>i : ℕ<VAR>hi1 : i < (Composition.ones 1).length<VAR>hi2 : i < 1<GOAL>((p 1) fun x => v (Fin.castLE ⋯ ⟨i, hi1⟩)) = (p 1) v
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<GOAL>f.norm = ↑p ^ (-f.valuation)
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<GOAL>¬↑f (stationaryPoint hf) = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>H : ↑f (stationaryPoint hf) = 0<GOAL>False
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>H : ↑f (stationaryPoint hf) = 0<GOAL>LimZero f
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>H : ↑f (stationaryPoint hf) = 0<VAR>ε : ℚ<VAR>hε : ε > 0<GOAL>∃ i, ∀ j ≥ i, padicNorm p (↑f j) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>H : ↑f (stationaryPoint hf) = 0<VAR>ε : ℚ<VAR>hε : ε > 0<GOAL>∀ j ≥ stationaryPoint hf, padicNorm p (↑f j) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>H : ↑f (stationaryPoint hf) = 0<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : n ≥ stationaryPoint hf<GOAL>padicNorm p (↑f n) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>H : ↑f (stationaryPoint hf) = 0<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>n : ℕ<VAR>hn : n ≥ stationaryPoint hf<GOAL>padicNorm p (↑f (stationaryPoint hf)) < ε
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y : C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>F G : C ⥤ Dᵒᵖ<VAR>e : F ≅ G<VAR>X : C<GOAL>(e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ<VAR>hf_nonneg : 0 ≤ᶠ[ae μ] f<VAR>hg_nonneg : 0 ≤ᶠ[ae μ] g<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<GOAL>∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ<VAR>hf_nonneg : 0 ≤ᶠ[ae μ] f<VAR>hg_nonneg : 0 ≤ᶠ[ae μ] g<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ<GOAL>∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ<VAR>hf_nonneg : 0 ≤ᶠ[ae μ] f<VAR>hg_nonneg : 0 ≤ᶠ[ae μ] g<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ<VAR>h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ<GOAL>∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ<VAR>hf_nonneg : 0 ≤ᶠ[ae μ] f<VAR>hg_nonneg : 0 ≤ᶠ[ae μ] g<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ<VAR>h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ<VAR>h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ<GOAL>∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g✝ : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>ν : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ<VAR>hf_nonneg : 0 ≤ᶠ[ae μ] f<VAR>hg_nonneg : 0 ≤ᶠ[ae μ] g<VAR>hf : Memℒp f (ENNReal.ofReal p) μ<VAR>hg : Memℒp g (ENNReal.ofReal q) μ<VAR>h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ<VAR>h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ<VAR>h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ<GOAL>∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<GOAL>s.card * t.card ≤ Eₘ[s, t]
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<GOAL>(s ×ˢ t).card ≤ Eₘ[s, t]
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a : α × α<VAR>x✝¹ : a ∈ ↑(s ×ˢ t)<VAR>b : α × α<VAR>x✝ : b ∈ ↑(s ×ˢ t)<GOAL>(fun x => ((x.1, x.1), x.2, x.2)) a = (fun x => ((x.1, x.1), x.2, x.2)) b → a = b
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s s₁ s₂ t t₁ t₂ : Finset α<VAR>a : α × α<VAR>x✝¹ : a ∈ ↑(s ×ˢ t)<VAR>b : α × α<VAR>x✝ : b ∈ ↑(s ×ˢ t)<GOAL>a.1 = b.1 → a.2 = b.2 → a = b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a✝ b : R<VAR>hx : AlgebraicIndependent R x<VAR>a : A<GOAL>(↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(aeval fun o => o.elim a x)