ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module.Free R M₁<VAR>cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')<GOAL>Nonempty (M ≃ₗ[R] M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module.Free R M₁<VAR>cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')<VAR>α : Type v<VAR>B : Basis α R M<GOAL>Nonempty (M ≃ₗ[R] M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module.Free R M₁<VAR>cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')<VAR>α : Type v<VAR>B : Basis α R M<VAR>β : Type v'<VAR>B' : Basis β R M'<GOAL>Nonempty (M ≃ₗ[R] M')
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : StrongRankCondition R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module.Free R M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module.Free R M'<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module.Free R M₁<VAR>cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')<VAR>α : Type v<VAR>B : Basis α R M<VAR>β : Type v'<VAR>B' : Basis β R M'<VAR>this : lift.{v', v} #α = lift.{v, v'} #β<GOAL>Nonempty (M ≃ₗ[R] M')
<VAR>ι : Type u_1<VAR>x : ℕ<VAR>t : Finset ι<VAR>s : ι → ℕ<GOAL>x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>m : (i : ι) → E i<GOAL>(tprodL 𝕜).toMultilinearMap m = (tprod 𝕜) m
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<GOAL>CompleteLattice.IsCompactElement (span R {x})
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<GOAL>∀ (s : Set (Submodule R M)), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → span R {x} ≤ sSup s → ∃ x_1 ∈ s, span R {x} ≤ x_1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>d : Set (Submodule R M)<VAR>hemp : d.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>hsup : span R {x} ≤ sSup d<GOAL>∃ x_1 ∈ d, span R {x} ≤ x_1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>d : Set (Submodule R M)<VAR>hemp : d.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>hsup : span R {x} ≤ sSup d<VAR>this : x ∈ sSup d<GOAL>∃ x_1 ∈ d, span R {x} ≤ x_1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<VAR>d : Set (Submodule R M)<VAR>hemp : d.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>hsup : span R {x} ≤ sSup d<VAR>this : x ∈ sSup d<VAR>y : Submodule R M<VAR>hyd : y ∈ d<VAR>hxy : x ∈ y<GOAL>∃ x_1 ∈ d, span R {x} ≤ x_1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : Ring k<VAR>inst✝ : Module k V<VAR>b : AffineBasis ι k P<VAR>s : Finset ι<VAR>i j : ι<VAR>e : ι ≃ ι'<VAR>hi : i ∉ s<VAR>w : ι → k<VAR>hw : s.sum w = 1<GOAL>(b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : IsPreconnected J<VAR>r : J → J → Prop<VAR>hr : _root_.Equivalence r<VAR>h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂<VAR>j₁ j₂ : J<GOAL>r j₁ j₂
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : IsPreconnected J<VAR>r : J → J → Prop<VAR>hr : _root_.Equivalence r<VAR>h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂<VAR>j₁ j₂ : J<VAR>z : ∀ (j : J), r j₁ j<GOAL>r j₁ j₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<GOAL>∫ (x : X) in univ, f x ∂μ = ∫ (x : X), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s✝ t : Finset ι<VAR>f✝ : ι → α<VAR>i✝ i : ι<VAR>f : ι → α<VAR>s : Finset ι<VAR>hs : s ⊆ {i}<VAR>j : ι<VAR>hji : j ∈ {i}<VAR>hj : j ∉ s<GOAL>Disjoint (f j) (s.sup f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝¹ : Lattice α<VAR>inst✝ : OrderBot α<VAR>s✝ t : Finset ι<VAR>f✝ : ι → α<VAR>i✝ i : ι<VAR>f : ι → α<VAR>s : Finset ι<VAR>hs : s ⊆ {i}<VAR>j : ι<VAR>hji : j ∈ {i}<VAR>hj : j ∉ s<GOAL>Disjoint (f j) ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ s<GOAL>(insert a s).card = s.card
<VAR>x✝ y : ℂ<VAR>x : ℝ<GOAL>(cexp (↑x * I)).im = Real.sin x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.coeff 1 = f.nextCoeff
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.coeff ((revAt f.natDegree) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
<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>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>hA : EquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<VAR>x : X<VAR>hx : x ∈ S<GOAL>Continuous (eval x ∘ u)
<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 z : P<VAR>hx : x ∈ s<VAR>t : R<VAR>ht0 : 0 ≤ t<GOAL>s.WSameSide ((lineMap x z) t) z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>g : t ↪r u<GOAL>∀ {a b : α × γ}, Prod.Lex s u ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } a) ({ toFun := Prod.map ⇑f ⇑g, inj' := ⋯ } b) ↔ Prod.Lex r t a b
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>π₀ : Prepartition I<VAR>hc₁ : π₀.distortion ≤ c<VAR>hc₂ : π₀.compl.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>π₀ : Prepartition I<VAR>hc₁ : π₀.distortion ≤ c<VAR>hc₂ : π₀.compl.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : TaggedPrepartition I<VAR>hle : π.toPrepartition ≤ π₀<VAR>hH : π.IsHenstock<VAR>hr : π.IsSubordinate r<VAR>hd : π.distortion = π₀.distortion<VAR>hU : π.iUnion = π₀.iUnion<GOAL>∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>π₀ : Prepartition I<VAR>hc₁ : π₀.distortion ≤ c<VAR>hc₂ : π₀.compl.distortion ≤ c<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π : TaggedPrepartition I<VAR>hle : π.toPrepartition ≤ π₀<VAR>hH : π.IsHenstock<VAR>hr : π.IsSubordinate r<VAR>hd : π.distortion = π₀.distortion<VAR>hU : π.iUnion = π₀.iUnion<VAR>x✝ : l.bDistortion = true<GOAL>π₀.compl.iUnion = ↑I \ π.iUnion
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ F : Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>whiskerRightIso (F.mapId a) (F.map f) = (F.mapComp (𝟙 a) f).symm ≪≫ F.map₂Iso (λ_ f) ≪≫ (λ_ (F.map f)).symm
<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>n : ℕ<VAR>H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<GOAL>Cardinal.mk ↑s ≤ ↑n
<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>n : ℕ<VAR>H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<GOAL>∀ (s_1 : Finset ↑s), s_1.card ≤ n
<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>n : ℕ<VAR>H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<GOAL>t.card ≤ n
<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>n : ℕ<VAR>H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<GOAL>(Finset.map (Embedding.subtype s) t).card ≤ n
<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>n : ℕ<VAR>H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<GOAL>AlgebraicIndependent R fun i => ↑i
<VAR>x y : ℝ<VAR>h : 0 ≤ x<GOAL>√x * √x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v w : VectorMeasure α M<GOAL>v = w ↔ ∀ (i : Set α), ↑v i = ↑w i
<VAR>k : ℕ<GOAL>riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)
<GOAL>riemannZeta (-↑0) = -↑(bernoulli' (0 + 1)) / (↑0 + 1)
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>this : TopologicalSpace α := TopologicalSpace.induced f t<GOAL>IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<VAR>this : TopologicalSpace α := TopologicalSpace.induced f t<GOAL>(∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen t_1ᶜ ∧ f ⁻¹' t_1 = s
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>w₀ : { w // w.IsComplex }<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : x ∈ convexBodyLT' K f w₀<GOAL>-x ∈ convexBodyLT' K f w₀
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>w₀ : { w // w.IsComplex }<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>hx : (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧ ∀ (a : InfinitePlace K) (b : a.IsComplex), x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)<GOAL>(∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧ ∀ (a : InfinitePlace K) (b : a.IsComplex), -x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : β → α<VAR>hf : mulSupport f ⊆ Set.range g<GOAL>∏' (c : γ), f (g c) = ∏' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : β → α<VAR>hf : mulSupport f ⊆ Set.range g<VAR>this : mulSupport f = g '' mulSupport (f ∘ g)<GOAL>∏' (c : γ), f (g c) = ∏' (b : β), f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : β → α<VAR>hf : mulSupport f ⊆ Set.range g<VAR>this : mulSupport f = g '' mulSupport (f ∘ g)<GOAL>tprod (f ∘ g) = ∏' (b : β), f b
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : Away r S<GOAL>(IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom = RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : Away r S<GOAL>((IsLocalization.Away.auxInv S r).comp (IsLocalization.Away.auxHom S r).toRingHom).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) = (RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})).comp (Ideal.Quotient.mk (Ideal.span {C r * X () - 1}))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>abs (invInterpStrip f z ε) = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>abs ((↑ε + ↑(sSupNormIm f 0)) ^ (z - 1)) * abs ((↑ε + ↑(sSupNormIm f 1)) ^ (-z)) = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>abs (↑(ε + sSupNormIm f 0) ^ (z - 1)) * abs (↑(ε + sSupNormIm f 1) ^ (-z)) = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℂ → E<VAR>z : ℂ<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>(ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : AEStronglyMeasurable f μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : AEStronglyMeasurable f μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I<GOAL>Tendsto (fun c => ∫⁻ (x : α) in φ c, ↑‖f x‖₊ ∂μ) l (𝓝 (∫⁻ (a : α), ↑‖f a‖₊ ∂μ))
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0<VAR>x : E<GOAL>↑‖x‖₊ / ↑r ≤ egauge 𝕜 (closedBall 0 ↑r) x
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x✝ y : E<VAR>r : ℝ≥0<VAR>x : E<GOAL>∀ (c : 𝕜), x ∈ c • closedBall 0 ↑r → ↑‖x‖₊ / ↑r ≤ ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c✝ : 𝕜<VAR>s t : Set E<VAR>x y✝ : E<VAR>r : ℝ≥0<VAR>c : 𝕜<VAR>y : E<VAR>hy : y ∈ closedBall 0 ↑r<GOAL>↑‖(fun x => c • x) y‖₊ / ↑r ≤ ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c✝ : 𝕜<VAR>s t : Set E<VAR>x y✝ : E<VAR>r : ℝ≥0<VAR>c : 𝕜<VAR>y : E<VAR>hy : ‖y‖₊ ≤ r<GOAL>↑‖(fun x => c • x) y‖₊ / ↑r ≤ ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c✝ : 𝕜<VAR>s t : Set E<VAR>x y✝ : E<VAR>r : ℝ≥0<VAR>c : 𝕜<VAR>y : E<VAR>hy : ‖y‖₊ ≤ r<GOAL>↑‖c‖₊ * ↑‖y‖₊ / ↑r ≤ ↑‖c‖₊
<VAR>𝕜 : Type u_1<VAR>inst✝² : NormedField 𝕜<VAR>α : Type u_2<VAR>E : Type u_3<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c✝ : 𝕜<VAR>s t : Set E<VAR>x y✝ : E<VAR>r : ℝ≥0<VAR>c : 𝕜<VAR>y : E<VAR>hy : ‖y‖₊ ≤ r<GOAL>↑‖c‖₊ * ↑‖y‖₊ ≤ ↑‖c‖₊ * ↑r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel (α × β) γ<VAR>a : β × α<VAR>g : γ → ℝ≥0∞<GOAL>∫⁻ (c : γ), g c ∂κ.swapLeft a = ∫⁻ (c : γ), g c ∂κ a.swap
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>(coeff R n) (φ * ψ) = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>(coeff R n) (φ * ψ) = ∑ p ∈ antidiagonal n, 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>∑ p ∈ antidiagonal n, (coeff R p.1) φ * (coeff R p.2) ψ = ∑ p ∈ antidiagonal n, 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>∀ x ∈ antidiagonal n, (coeff R x.1) φ * (coeff R x.2) ψ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<VAR>x : ℕ × ℕ<VAR>hx : x ∈ antidiagonal n<GOAL>(coeff R x.1) φ * (coeff R x.2) ψ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<VAR>x : ℕ × ℕ<VAR>hx : x ∈ antidiagonal n<GOAL>↑x.2 ≤ ↑n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>n : ℕ<VAR>h : ↑n < ψ.order<VAR>x : ℕ × ℕ<VAR>hx : x.1 + x.2 = n<GOAL>↑x.2 ≤ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : CommMonoid β<VAR>f : (a : α) → p a → β<VAR>g : (a : α) → ¬p a → β<GOAL>∏ a : α, dite (p a) (f a) (g a) = (∏ a : { a // p a }, f ↑a ⋯) * ∏ a : { a // ¬p a }, g ↑a ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Fintype α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : CommMonoid β<VAR>f : (a : α) → p a → β<VAR>g : (a : α) → ¬p a → β<GOAL>(∏ x : { x // x ∈ filter p univ }, f ↑x ⋯) * ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x ⋯ = (∏ a : { a // p a }, f ↑a ⋯) * ∏ a : { a // ¬p a }, g ↑a ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<GOAL>(s.erase x).min ≠ ↑x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>e_1✝ : WithTop α = WithBot αᵒᵈ<GOAL>(s.erase x).min = ((map toDual.toEmbedding s).erase (toDual x)).max
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>e_1✝¹ : WithTop α = WithBot αᵒᵈ<VAR>e_1✝ : α = αᵒᵈ<VAR>a✝ : α<GOAL>a✝ ∈ s ↔ a✝ ∈ map toDual.toEmbedding s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>s : Finset α<VAR>e_1✝¹ : WithTop α = WithBot αᵒᵈ<VAR>e_1✝ : α = αᵒᵈ<VAR>a✝ : α<GOAL>a✝ ∈ s ↔ toDual.symm a✝ ∈ s
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>X Y : ModuleCat R<VAR>f : X ⟶ Y<VAR>M : Type v<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Epi f ↔ Function.Surjective ⇑f
<VAR>ι : Type u_1<VAR>β : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : {i : ι} → β i → β i → Prop<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝ : (i : ι) → PartialOrder (β i)<VAR>x y : (i : ι) → β i<VAR>i : ι<VAR>a : β i<GOAL>toLex x ≤ toLex (update x i a) ↔ x i ≤ a
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ℝ<GOAL>volume (Icc a b) = ofReal (b - a)