ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>(∀ (x : ℕ), μ (s ∩ spanningSets μ x) = 0) ↔ μ s = 0
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<VAR>h : f = divided_by_X_pow_order hf<GOAL>IsUnit (divided_by_X_pow_order hf)
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<VAR>h : IsUnit f<GOAL>f = divided_by_X_pow_order hf
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<VAR>h : IsUnit f<VAR>this : f.order.get ⋯ = 0<GOAL>f = divided_by_X_pow_order hf
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<VAR>h : IsUnit f<VAR>this : f.order.get ⋯ = 0<GOAL>divided_by_X_pow_order hf = X ^ f.order.get ⋯ * divided_by_X_pow_order hf
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<GOAL>V ∈ 𝓝 (x, x)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>w_sub : w ○ w ⊆ V<GOAL>V ∈ 𝓝 (x, x)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>w_sub : w ○ w ⊆ V<VAR>this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)<GOAL>V ∈ 𝓝 (x, x)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>w_sub : w ○ w ⊆ V<VAR>this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)<GOAL>ball x w ×ˢ ball x w ⊆ V
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<VAR>w : Set (α × α)<VAR>w_in : w ∈ 𝓤 α<VAR>w_symm : SymmetricRel w<VAR>w_sub : w ○ w ⊆ V<VAR>this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)<VAR>u v : α<VAR>u_in : (u, v).1 ∈ ball x w<VAR>v_in : (u, v).2 ∈ ball x w<GOAL>(u, v) ∈ V
<VAR>α : Type u_1<VAR>n : Nat<VAR>f : α → Fin n → α<VAR>x : α<GOAL>foldl n f x = List.foldl f x (list n)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : M<GOAL>⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i : α, c i • v i = x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝⁶ : Fintype α<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>S : Type u_4<VAR>inst✝² : Semiring S<VAR>inst✝¹ : Module S M<VAR>inst✝ : SMulCommClass R S M<VAR>v : α → M<VAR>x : M<GOAL>⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), x ∈ span R (Set.range v)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<GOAL>round (-2⁻¹) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>n : ℕ<GOAL>↑(B ^ n).card ≤ (↑(A / B).card / ↑A.card) ^ n * ↑A.card
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<VAR>hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<VAR>hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ<VAR>wπ : f' ≫ cokernel.π (kernel.ι γ) = 0<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<VAR>hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ<VAR>wπ : f' ≫ cokernel.π (kernel.ι γ) = 0<VAR>e : Abelian.image S.f ≅ kernel γ := S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<VAR>hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ<VAR>wπ : f' ≫ cokernel.π (kernel.ι γ) = 0<VAR>e : Abelian.image S.f ≅ kernel γ := S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))<VAR>he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<VAR>hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ<VAR>wπ : f' ≫ cokernel.π (kernel.ι γ) = 0<VAR>e : Abelian.image S.f ≅ kernel γ := S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))<VAR>he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel<VAR>fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ<GOAL>S.LeftHomologyData
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f<VAR>f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯<VAR>hf' : f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ<VAR>wπ : f' ≫ cokernel.π (kernel.ι γ) = 0<VAR>e : Abelian.image S.f ≅ kernel γ := S.abelianImageToKernelIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (kernel.ι S.g ≫ cokernel.π S.f) 0))<VAR>he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel<VAR>fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ<VAR>hπ : IsColimit (CokernelCofork.ofπ (cokernel.π (kernel.ι γ)) wπ)<GOAL>S.LeftHomologyData
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x x' : M<VAR>h : x' ∈ (extChartAt I x).source<VAR>ht : t ∈ 𝓝[s] x'<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x'
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<VAR>m' : M'<GOAL>mk' f m s = m' ↔ f m = s • m'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : List α<GOAL>s ∈ t.sublists ↔ s <+ t
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : Algebra S K<VAR>inst✝² : NoZeroSMulDivisors R K<VAR>inst✝¹ : IsFractionRing S K<VAR>inst✝ : IsScalarTower R S K<GOAL>Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : Algebra S K<VAR>inst✝² : NoZeroSMulDivisors R K<VAR>inst✝¹ : IsFractionRing S K<VAR>inst✝ : IsScalarTower R S K<GOAL>(∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁷ : Monoid α<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : MulAction α β<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : SMulPosStrictMono α β<VAR>inst✝ : SMulPosReflectLT α β<VAR>hb : 0 < b<GOAL>b < a • b ↔ 1 • b < a • b
<VAR>n d a : Int<VAR>a0 : a ≠ 0<GOAL>n * a /. (d * a) = n /. d
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : Fintype l<VAR>inst✝ : CommRing R<VAR>A : Matrix (l ⊕ l) (l ⊕ l) R<GOAL>A ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<GOAL>∀ (l : List α), mapIdx f l = List.oldMapIdx f l
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<GOAL>mapIdx f [] = List.oldMapIdx f []
<VAR>α : Type u<VAR>β : Type v<VAR>f : ℕ → α → β<GOAL>∀ (l : List α) (e : α), mapIdx f l = List.oldMapIdx f l → mapIdx f (l ++ [e]) = List.oldMapIdx f (l ++ [e])
<VAR>x✝ y✝ x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>√(x / y) = √x / √y
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype p<VAR>inst✝ : NonUnitalCommSemiring R<VAR>A : Matrix m n R<VAR>B : Matrix n p R<VAR>C : Matrix p m R<GOAL>(A * (B * C)).trace = (C * (A * B)).trace
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>f : R →+* A<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : eval₂ f z p = 0<VAR>hz : f x * z = f y<GOAL>x ∣ y ^ p.natDegree
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>f : R →+* A<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : eval₂ f z p = 0<VAR>hz : f x * z = f y<GOAL>y ^ (p.scaleRoots x).natDegree ∈ span {x}
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>f : R →+* A<VAR>hf : Function.Injective ⇑f<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : eval₂ f z p = 0<VAR>hz : f x * z = f y<GOAL>(p.scaleRoots x).IsRoot y
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>f : R →+* A<VAR>hf : ∀ (a : R), f a = 0 ↔ a = 0<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : eval₂ f z p = 0<VAR>hz : f x * z = f y<GOAL>(p.scaleRoots x).IsRoot y
<VAR>R : Type u<VAR>A : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing A<VAR>f : R →+* A<VAR>hf : ∀ (a : R), f a = 0 ↔ a = 0<VAR>p : R[X]<VAR>hp : p.Monic<VAR>x y : R<VAR>z : A<VAR>h : eval₂ f z p = 0<VAR>hz : f x * z = f y<VAR>this : eval₂ f (f x * z) (p.scaleRoots x) = 0<GOAL>(p.scaleRoots x).IsRoot y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢￢(a ⊔ b) ≤ ￢￢a ⊔ ￢￢b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>Codisjoint (a ⊔ b) (￢(a ⊔ b))
<VAR>s b p : ℝ<VAR>hp : 1 < p<VAR>hb : 0 < b<GOAL>(fun x => x ^ s * rexp (-b * x ^ p)) =o[atTop] fun x => rexp (-(1 / 2) * x)
<VAR>s b p : ℝ<VAR>hp : 1 < p<VAR>hb : 0 < b<GOAL>(fun x => x ^ s * rexp (-x)) =o[atTop] fun x => rexp (-(1 / 2) * x)
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>H : minpoly G F x = 1<VAR>this : Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0<GOAL>1 = 0
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P : Sheaf J D<GOAL>((sheafificationAdjunction J D).counit.app P).val = (((sheafificationAdjunction J D).homEquiv P.val { val := P.val, cond := ⋯ }).symm (𝟙 P.val)).val
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P : Sheaf J D<GOAL>((sheafificationAdjunction J D).counit.app P).val = ((presheafToSheaf J D).map (𝟙 P.val) ≫ (sheafificationAdjunction J D).counit.app { val := P.val, cond := ⋯ }).val
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>v : Fin (n + 2) → F<VAR>N : 0 < n + 2<GOAL>∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (applyComposition (fun k => if k < n + 2 then p.rightInv i k else 0) c v) = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i).applyComposition c v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>v : Fin (n + 2) → F<VAR>N : 0 < n + 2<VAR>c : Composition (n + 2)<VAR>hc : c ∈ {c | 1 < c.length}.toFinset<VAR>j : ℕ<VAR>hj1 hj2 : j < c.length<GOAL>applyComposition (fun k => if k < n + 2 then p.rightInv i k else 0) c v ⟨j, hj1⟩ = (p.rightInv i).applyComposition c v ⟨j, hj2⟩
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>v : Fin (n + 2) → F<VAR>N : 0 < n + 2<VAR>c : Composition (n + 2)<VAR>hc : c ∈ {c | 1 < c.length}.toFinset<VAR>j : ℕ<VAR>hj1 hj2 : j < c.length<VAR>this : ∀ (k : Fin c.length), c.blocksFun k < n + 2<GOAL>applyComposition (fun k => if k < n + 2 then p.rightInv i k else 0) c v ⟨j, hj1⟩ = (p.rightInv i).applyComposition c v ⟨j, hj2⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 4<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>φ : R₁ ⟶ R₂<VAR>h₀ : Epi (φ.app 0)<VAR>h₁ : IsIso (φ.app 1)<VAR>h₂ : IsIso (φ.app ⟨3, ⋯⟩)<VAR>h₃ : Mono (φ.app ⟨4, ⋯⟩)<GOAL>IsIso (app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 4<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>φ : R₁ ⟶ R₂<VAR>h₀ : Epi (φ.app 0)<VAR>h₁ : IsIso (φ.app 1)<VAR>h₂ : IsIso (φ.app ⟨3, ⋯⟩)<VAR>h₃ : Mono (φ.app ⟨4, ⋯⟩)<VAR>this : Mono (app' φ 2 ⋯)<GOAL>IsIso (app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 4<VAR>hR₁ : R₁.Exact<VAR>hR₂ : R₂.Exact<VAR>φ : R₁ ⟶ R₂<VAR>h₀ : Epi (φ.app 0)<VAR>h₁ : IsIso (φ.app 1)<VAR>h₂ : IsIso (φ.app ⟨3, ⋯⟩)<VAR>h₃ : Mono (φ.app ⟨4, ⋯⟩)<VAR>this✝ : Mono (app' φ 2 ⋯)<VAR>this : Epi (app' φ 2 ⋯)<GOAL>IsIso (app' φ 2 ⋯)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H K : Subgroup N<VAR>hH : H ≤ f.range<VAR>hK : K ≤ f.range<GOAL>map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
<VAR>n k : ℕ<GOAL>k + 2 ≠ 1
<VAR>n k : ℕ<GOAL>1 < k + 2
<VAR>n k : ℕ<GOAL>0 < k + 1
<VAR>x✝ y z x : ℝ<GOAL>x ^ 1 = x
<VAR>x : ℤ[i]<GOAL>0 < norm x ↔ x ≠ 0
<VAR>x : ℤ[i]<GOAL>0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulWithZero α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosStrictMono α β<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a • b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>S : Set β'<VAR>k : κ<VAR>hk : UniformEquicontinuousOn F S<GOAL>UniformEquicontinuousOn F S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>S : Set β'<VAR>k : κ<VAR>hk : UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S<GOAL>UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>S : Set β'<VAR>k : κ<VAR>hk : UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S<GOAL>Tendsto (fun x => ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2)) (𝓤 β' ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>u : κ → UniformSpace β'<VAR>F : ι → β' → α<VAR>S : Set β'<VAR>k : κ<VAR>hk : UniformContinuousOn (⇑UniformFun.ofFun ∘ swap F) S<GOAL>Tendsto (fun x => ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2)) ((⨅ i, 𝓤 β') ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α))
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → M₁ i<VAR>i : ι<VAR>x : M₁ i<GOAL>f (update m i (-x)) + f (update m i x) = 0
<VAR>E✝ : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedSpace ℝ E✝<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f✝ g✝ : E✝ → G<VAR>C : ℝ<VAR>s : Set E✝<VAR>x✝ y : E✝<VAR>f' g' : E✝ → E✝ →L[𝕜] G<VAR>φ : E✝ →L[𝕜] G<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : E → G<VAR>hf : Differentiable 𝕜 f<VAR>hg : Differentiable 𝕜 g<VAR>hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x<VAR>x : E<VAR>hfgx : f x = g x<VAR>A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E<GOAL>f = g
<VAR>E✝ : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E✝<VAR>inst✝⁸ : NormedSpace ℝ E✝<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedSpace 𝕜 E✝<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>f✝ g✝ : E✝ → G<VAR>C : ℝ<VAR>s : Set E✝<VAR>x✝ y : E✝<VAR>f' g' : E✝ → E✝ →L[𝕜] G<VAR>φ : E✝ →L[𝕜] G<VAR>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f g : E → G<VAR>hf : Differentiable 𝕜 f<VAR>hg : Differentiable 𝕜 g<VAR>hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x<VAR>x : E<VAR>hfgx : f x = g x<VAR>A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E<GOAL>EqOn f g univ
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : f =ᶠ[atTop] g<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : f =ᶠ[cofinite] g<VAR>hf : LSeriesSummable f s<GOAL>LSeriesSummable g s
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : f =ᶠ[cofinite] g<VAR>hf : LSeriesSummable f s<GOAL>∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>h : f =ᶠ[cofinite] g<VAR>hf : LSeriesSummable f s<VAR>this : term f s =ᶠ[cofinite] term g s<GOAL>∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>l : (i : ι) → G i<VAR>s : Finset ι<GOAL>‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>l : (i : ι) → G i<VAR>s : Finset ι<VAR>this : ↑‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ↑‖l i‖ ^ 2<GOAL>‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>D : ℝ<VAR>x : E<VAR>Dpos : 0 < D<GOAL>y D x ≤ 1