ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>∀ (r : R), (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (C r)) = (aeval fun o => o.elim a x) (C r)
<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>∀ (i : Option ι), (Polynomial.aeval a) (hx.mvPolynomialOptionEquivPolynomialAdjoin (X i)) = (aeval fun o => o.elim a x) (X i)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>f : M →ₗ[R] M'<VAR>hf_inj : Disjoint (span R (range v)) (LinearMap.ker f)<GOAL>LinearIndependent R (⇑f ∘ v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<VAR>f : M →ₗ[R] M'<VAR>hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) ≤ LinearMap.ker (Finsupp.total ι M R v)<GOAL>LinearIndependent R (⇑f ∘ v)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥<VAR>f : M →ₗ[R] M'<VAR>hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) ≤ LinearMap.ker (Finsupp.total ι M R v)<GOAL>LinearMap.ker (Finsupp.total ι M' R (⇑f ∘ v)) = ⊥
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥<VAR>f : M →ₗ[R] M'<VAR>hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥<GOAL>LinearMap.ker (Finsupp.total ι M' R (⇑f ∘ v)) = ⊥
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥<VAR>f : M →ₗ[R] M'<VAR>hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥<VAR>this : Inhabited M<GOAL>LinearMap.ker (Finsupp.total ι M' R (⇑f ∘ v)) = ⊥
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearMap.ker (Finsupp.total ι M R v) = ⊥<VAR>f : M →ₗ[R] M'<VAR>hf_inj : comap (Finsupp.total ι M R v) (LinearMap.ker f) = ⊥<VAR>this : Inhabited M<GOAL>∀ (i : ι), f (v i) = f (v i)
<VAR>G : Type u_1<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : SecondCountableTopology G<VAR>K₀ : PositiveCompacts G<VAR>μ : Measure G<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>h : μ ↑K₀ = 1<GOAL>haarMeasure K₀ = μ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Fintype ι<VAR>b : Basis ι R M<VAR>inst✝¹ : Fintype R<VAR>inst✝ : Fintype M<GOAL>card M = card R ^ card ι
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : IsPreirreducible s<VAR>u : Set X<VAR>hu : IsOpen u<VAR>v : Set X<VAR>hv : IsOpen v<VAR>x✝ : X<VAR>hxs✝ : x✝ ∈ s<VAR>hxu✝ : ⟨x✝, hxs✝⟩ ∈ val ⁻¹' u<VAR>y : X<VAR>hys : y ∈ s<VAR>hyv : ⟨y, hys⟩ ∈ val ⁻¹' v<VAR>x : X<VAR>hxs : x ∈ s<VAR>hxu : x ∈ u<VAR>hxv : x ∈ v<GOAL>(univ ∩ (val ⁻¹' u ∩ val ⁻¹' v)).Nonempty
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>F : Discrete J ⥤ C<VAR>x y : J<VAR>f : { as := x } ⟶ { as := y }<GOAL>(({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun F => Discrete.functor F, map := fun {X Y} f => Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).map f ≫ ((fun j => Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun F => Discrete.functor F, map := fun {X Y} f => Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj j)) { as := y }).hom = ((fun j => Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun F => Discrete.functor F, map := fun {X Y} f => Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj j)) { as := x }).hom ≫ ((𝟭 (Discrete J ⥤ C)).obj F).map f
<VAR>J : Type u₂<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>F : Discrete J ⥤ C<VAR>x : J<VAR>f : { as := x } ⟶ { as := x }<GOAL>(({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun F => Discrete.functor F, map := fun {X Y} f => Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).map f ≫ ((fun j => Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun F => Discrete.functor F, map := fun {X Y} f => Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj j)) { as := x }).hom = ((fun j => Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙ { obj := fun F => Discrete.functor F, map := fun {X Y} f => Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj j)) { as := x }).hom ≫ ((𝟭 (Discrete J ⥤ C)).obj F).map f
<VAR>n : ℕ<GOAL>φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}
<VAR>n : ℕ<VAR>e : ↑{m | m < n ∧ n.Coprime m} ≃ { x // x ∈ filter n.Coprime (range n) } := { toFun := fun m => ⟨↑m, ⋯⟩, invFun := fun m => ⟨↑m, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }<GOAL>φ n = Nat.card ↑{m | m < n ∧ n.Coprime m}
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι ℝ F<GOAL>a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>a b : OrthonormalBasis ι ℝ F<GOAL>a.toBasis.det ⇑b ^ 2 = 1
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>c : Cardinal.{v'}<VAR>f : V →ₗ[K] V'<GOAL>c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndependent K fun (x : ↑s) => f ↑x
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>c : Cardinal.{v'}<VAR>f : V →ₗ[K] V'<VAR>g : ↥(range f) →ₗ[K] V<VAR>hg : f.rangeRestrict ∘ₗ g = id<GOAL>c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndependent K fun (x : ↑s) => f ↑x
<VAR>K : Type u<VAR>V V₁ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V'<VAR>inst✝ : Module K V'<VAR>c : Cardinal.{v'}<VAR>f : V →ₗ[K] V'<VAR>g : ↥(range f) →ₗ[K] V<VAR>hg : f.rangeRestrict ∘ₗ g = id<VAR>fg : LeftInverse ⇑f.rangeRestrict ⇑g<GOAL>c ≤ f.rank ↔ ∃ s, lift.{v', v} #↑s = lift.{v, v'} c ∧ LinearIndependent K fun (x : ↑s) => f ↑x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : l → o<VAR>e₂ : m ≃ o<VAR>M : Matrix m n α<GOAL>submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : l → o<VAR>e₂ : m ≃ o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<GOAL>submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : l → o<VAR>e₂ : m ≃ o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<VAR>A : Matrix o n α := M.submatrix (⇑e₂.symm) id<GOAL>submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : l → o<VAR>e₂ : m ≃ o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<VAR>A : Matrix o n α := M.submatrix (⇑e₂.symm) id<VAR>this : M = A.submatrix (⇑e₂) id<GOAL>submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Finite o<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq o<VAR>e₁ : l → o<VAR>e₂ : m ≃ o<VAR>M : Matrix m n α<VAR>val✝ : Fintype o<VAR>A : Matrix o n α := M.submatrix (⇑e₂.symm) id<VAR>this : M = A.submatrix (⇑e₂) id<GOAL>(1 * A).submatrix e₁ id = (A.submatrix (⇑e₂) id).submatrix (⇑e₂.symm ∘ e₁) id
<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>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiffWithinAt 𝕜 n (fun x => 0) s x
<GOAL>Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)
<GOAL>Tendsto (fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
<GOAL>Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)
<GOAL>Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>a ^ 2 = ↑(normSq a) ↔ a = ↑a.re
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>star a = a ∨ a = 0 ↔ star a = a
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<GOAL>constantCoeff (xInTermsOfW p R n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<GOAL>⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<GOAL>⅟↑p ^ n * ∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = ⅟↑p ^ n * 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<GOAL>∑ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<GOAL>∀ x ∈ range n, constantCoeff (C (↑p ^ x) * xInTermsOfW p R x ^ p ^ (n - x)) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<VAR>m : ℕ<VAR>H : m ∈ range n<GOAL>constantCoeff (C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<VAR>m : ℕ<VAR>H : m < n<GOAL>constantCoeff (C (↑p ^ m) * xInTermsOfW p R m ^ p ^ (n - m)) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<VAR>m : ℕ<VAR>H : m < n<GOAL>↑p ^ m * 0 ^ p ^ (n - m) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<VAR>IH : ∀ m < n, constantCoeff (xInTermsOfW p R m) = 0<VAR>m : ℕ<VAR>H : m < n<GOAL>p ^ (n - m) ≠ 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K L : CochainComplex C ℕ<VAR>φ : K ⟶ L<VAR>inst✝¹ : HomologicalComplex.HasHomology K 0<VAR>inst✝ : HomologicalComplex.HasHomology L 0<GOAL>HomologicalComplex.homologyMap φ 0 ≫ L.isoHomologyπ₀.inv = K.isoHomologyπ₀.inv ≫ HomologicalComplex.cyclesMap φ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Unique α<GOAL>krullDim α = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Unique α<GOAL>(LTSeries.longestOf α).length = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Unique α<VAR>q : LTSeries α<GOAL>q.length ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Unique α<VAR>q : LTSeries α<VAR>r : ¬q.length ≤ 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring R<VAR>inst✝ : Nontrivial R<VAR>m : Multiset R<VAR>l : List R<GOAL>0 < prod (Quot.mk Setoid.r l) ↔ ∀ x ∈ Quot.mk Setoid.r l, 0 < x
<VAR>R : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring R<VAR>inst✝ : Nontrivial R<VAR>m : Multiset R<VAR>l : List R<GOAL>0 < l.prod ↔ ∀ x ∈ ↑l, 0 < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<GOAL>⋃ y ∈ range f, f ⁻¹' {y} = univ
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G α<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : Finite α<VAR>S : Set (Equiv.Perm α)<VAR>hS : ∀ σ ∈ S, σ.IsSwap<VAR>inst✝ : IsPretransitive (↥(closure S)) α<GOAL>closure S = ⊤
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SSameSide (v +ᵥ x) y ↔ s.SSameSide x y
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) 1) = 1
<VAR>α : Type u_1<VAR>inst✝³ : SemilatticeInf α<VAR>inst✝² : OrderTop α<VAR>inst✝¹ : Finite α<VAR>s : { s // InfIrred s }<VAR>inst✝ : Fintype ↥↑s<GOAL>infIrredUpperSet.symm s = (↑↑s).toFinset.inf id
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>A B : V<VAR>f : A ⟶ B<GOAL>((single₀ V).map f).f 0 = f
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>A B : V<VAR>f : A ⟶ B<GOAL>(HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A).hom ≫ f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B).inv = f
<VAR>V : Type u<VAR>inst✝² : Category.{v, u} V<VAR>inst✝¹ : HasZeroMorphisms V<VAR>inst✝ : HasZeroObject V<VAR>A B : V<VAR>f : A ⟶ B<GOAL>𝟙 A ≫ f ≫ 𝟙 B = f
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>z : M<GOAL>z ∈ center M ↔ ∀ (g : M), g * z = z * g
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>z : M<GOAL>z ∈ center M ↔ z ∈ Set.center M
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>h : 1 + y ≠ 0<GOAL>x ^ (1 + y) = x * x ^ y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>X : Cᵒᵖ<VAR>x : F.obj X<VAR>property✝ : x ∈ G.obj X<GOAL>F.map (𝟙 X) x = x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>G G' : Subpresheaf F<VAR>X Y Z : Cᵒᵖ<VAR>i : X ⟶ Y<VAR>j : Y ⟶ Z<VAR>x : F.obj X<VAR>property✝ : x ∈ G.obj X<GOAL>F.map (i ≫ j) x = F.map j (F.map i x)
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>#((n : ℕ) × (L.sum L.skolem₁).Functions n) = #((n : ℕ) × L.BoundedFormula Empty (n + 1))
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>((sum fun i => lift.{max u v, u} #(L.Functions i)) + sum fun i => lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) = sum fun i => #(L.BoundedFormula Empty (i + 1))
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>((sum fun i => lift.{max u v, u} #(L.Functions i)) + sum fun i => #(L.BoundedFormula Empty (i + 1))) = sum fun i => #(L.BoundedFormula Empty (i + 1))
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>(sum fun i => lift.{max u v, u} #(L.Functions i)) ≤ sum fun i => #(L.BoundedFormula Empty (i + 1))
<VAR>L : Language<VAR>M : Type w<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : L.Structure M<GOAL>ℵ₀ ≤ sum fun i => #(L.BoundedFormula Empty (i + 1))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>α : Type u_5<VAR>β : Type u_6<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<GOAL>∀ (n : ℕ), μ (support ↑(0 n)) < ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : LinearOrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>a b : 𝕜<VAR>x y : E<GOAL>[x-[𝕜]y] ⊆ uIcc x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : LinearOrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>a b : 𝕜<VAR>x y : E<VAR>h : x ≤ y<GOAL>[x-[𝕜]y] ⊆ uIcc x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : LinearOrderedAddCommMonoid E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : OrderedSMul 𝕜 E<VAR>a b : 𝕜<VAR>x y : E<VAR>h : y ≤ x<GOAL>[x-[𝕜]y] ⊆ uIcc x y
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>x : α<VAR>r : ι → ℝ<VAR>hr : Tendsto r l atTop<GOAL>∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.closedBall x (r i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : OpensMeasurableSpace α<VAR>x : α<VAR>r : ι → ℝ<VAR>hr : Tendsto r l atTop<VAR>y : α<GOAL>∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<GOAL>∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x✝ x : 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x