ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)<VAR>this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, (1 - x) * x ^ i) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this✝ : HasSum (fun i => (1 - x) * x ^ i) ((1 - x) * ∑' (b : ℕ), x ^ b)<VAR>this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)<VAR>x✝ : ℕ<GOAL>1 - x ^ x✝ = ∑ i ∈ Finset.range x✝, (1 - x) * x ^ i
<VAR>s : String<GOAL>s.get 0 = s.data.headD default
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>i j : J<VAR>f : i ⟶ j<VAR>x✝ : F.toEventualRanges.obj j<VAR>x : F.obj j<VAR>hx : x ∈ F.eventualRange j<GOAL>∃ a, F.toEventualRanges.map f a = ⟨x, hx⟩
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>i j : J<VAR>f : i ⟶ j<VAR>x✝ : F.toEventualRanges.obj j<VAR>y : F.obj i<VAR>hy : y ∈ F.eventualRange i<VAR>hx : F.map f y ∈ F.eventualRange j<GOAL>∃ a, F.toEventualRanges.map f a = ⟨F.map f y, hx⟩
<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 : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<VAR>pred : ι → Prop<VAR>inst✝ : DecidablePred pred<GOAL>(((Finset.subtype pred s).weightedVSubOfPoint (fun i => p ↑i) b) fun i => w ↑i) = ((filter pred s).weightedVSubOfPoint p b) w
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.48420, u_2} D<VAR>E : Type u_3<VAR>inst✝⁶ : Category.{?u.48427, u_3} E<VAR>M : Type u_4<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : HasShift E M<VAR>X Y Z T : C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (a : M), (shiftFunctor C a).PreservesZeroMorphisms<VAR>a : M<VAR>β : ShiftedHom X Y a<VAR>b c : M<VAR>h : b + a = c<GOAL>β.comp 0 h = 0
<VAR>z : ℝ<GOAL>z + 2 * π = z + ↑1 * (2 * π)
<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✝⁵ : OrderedRing 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>a x b c : E<GOAL>a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c
<VAR>α✝ α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → ℤ<GOAL>∃ β t sgn g, (∀ (b : β), g b ∈ s) ∧ t.card = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
<VAR>α✝ α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → ℤ<GOAL>(univ.sigma fun a => range (f ↑a).natAbs).card = ∑ a ∈ s, (f a).natAbs
<VAR>α✝ α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>f : α → ℤ<GOAL>∀ a ∈ s, (∑ b ∈ univ.sigma fun a => range (f ↑a).natAbs, if (fun a => ↑a.fst) b = a then ↑((fun a => sign (f ↑a.fst)) b) else 0) = f a
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : ℝ → E<VAR>w : ℝ<GOAL>𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ Z✝ : C<VAR>f : Y✝ ⟶ X✝<VAR>S R : Sieve X✝<VAR>I : Type u_1<VAR>Y : I → C<VAR>Z X : C<VAR>g : Z ⟶ X<GOAL>(ofObjects Y X).arrows g ↔ ∃ i, Nonempty (Z ⟶ Y i)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{u₂, u₁} C<VAR>inst✝ : GaloisCategory C<VAR>X : C<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<GOAL>∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
<VAR>α : Type u<VAR>c✝ d : Cardinal.{u}<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>↑(toNat c) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<GOAL>p.leadingCoeff = 0 ↔ p.degree = ⊥
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>f₂ : (i : ι) → β i → β₁ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>hf₂ : ∀ (i : ι), f₂ i 0 = 0<VAR>h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0<VAR>g : Π₀ (i : ι), β i<VAR>i✝ : ι<GOAL>(mapRange (fun i => f i ∘ f₂ i) h g) i✝ = (mapRange f hf (mapRange f₂ hf₂ g)) i✝
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>f₂ : (i : ι) → β i → β₁ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>hf₂ : ∀ (i : ι), f₂ i 0 = 0<VAR>h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0<VAR>g : Π₀ (i : ι), β i<VAR>i✝ : ι<GOAL>(f i✝ ∘ f₂ i✝) (g i✝) = f i✝ (f₂ i✝ (g i✝))
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>α : Type u_4<VAR>f : α → M<GOAL>mrange (FreeMonoid.lift f) = closure (Set.range f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq0_lt : 0 < q<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ = eLpNorm' f q μ ^ q
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq0_lt : 0 < q<GOAL>q ≠ 0
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j x : Fin n<VAR>y : Fin (n + 1)<VAR>h : x.castSucc < y<VAR>h' : optParam (y.succAbove x ≠ last n) ⋯<GOAL>(y.succAbove x).castPred h' = x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hf : f 0 = 0<GOAL>seminormFromConst_seq c f 0 = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hf : f 0 = 0<GOAL>(fun n => f (0 * c ^ n) / f c ^ n) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hf : f 0 = 0<VAR>n : ℕ<GOAL>f (0 * c ^ n) / f c ^ n = 0 n
<VAR>x y : ℕ<GOAL>↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
<VAR>x y : ℕ<VAR>this : Nat.P x y (x.xgcdAux 1 0 y 0 1)<GOAL>↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<GOAL>{i | (f i).Nonempty}.Finite
<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✝² : Fintype n<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>e : m ≃ n<VAR>M : Matrix m n α<GOAL>M.submatrix id ⇑e * Mᵀ.submatrix (⇑e) id = M * Mᵀ
<VAR>s n : Nat<GOAL>(range' s (n + 1)).reverse = map (fun x => s + (n + 1) - 1 - x) (range (n + 1))
<VAR>s n : Nat<GOAL>[s + n].reverse ++ (range' s n).reverse = (s + n - 0) :: map ((fun x => s + n - x) ∘ succ) (range n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.eraseLead.natDegree ≤ f.natDegree - 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>h : f.eraseLead.natDegree < f.natDegree<GOAL>f.eraseLead.natDegree ≤ f.natDegree - 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>h : f.eraseLead = 0<GOAL>f.eraseLead.natDegree ≤ f.natDegree - 1
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n : ℤ<VAR>x : R<VAR>h : a < 0<GOAL>↑a ≤ -1
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n : ℤ<VAR>x : R<VAR>h : a < 0<GOAL>a ≤ -1
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>f : α → β → β<VAR>xs : t α<VAR>x : β<GOAL>foldr f x xs = (Foldr.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>Tendsto f (𝓟 s) (𝓟 t) ↔ ∀ a ∈ s, f a ∈ t
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>hN : IsTorsion R N<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>hN : IsTorsion R N<VAR>I : Type u<VAR>fI : Fintype I<VAR>w✝ : DecidableEq I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>hN : IsTorsion R N<VAR>I : Type u<VAR>fI : Fintype I<VAR>w✝ : DecidableEq I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)<VAR>this : Fintype I<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>h' : Finite R N<VAR>hN : IsTorsion R N<VAR>I : Type u<VAR>fI : Fintype I<VAR>w✝ : DecidableEq I<VAR>p : I → R<VAR>hp : ∀ (i : I), Irreducible (p i)<VAR>e : I → ℕ<VAR>h : DirectSum.IsInternal fun i => torsionBy R N (p i ^ e i)<VAR>this✝ : Fintype I<VAR>this : ∀ (i : I), ∃ d k, Nonempty (↥(torsionBy R N (p i ^ e i)) ≃ₗ[R] ⨁ (j : Fin d), R ⧸ span R {p i ^ k j})<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ span R {p i ^ e i})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>∫⁻ (a : α), f a ∂Measure.sum μ = ∑' (i : ι), ∫⁻ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>⨆ x, ⨆ s, ∑ i ∈ s, (↑x).lintegral (μ i) = ⨆ s, ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>⨆ j, ⨆ i, ∑ i_1 ∈ j, (↑i).lintegral (μ i_1) = ⨆ s, ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>(fun j => ⨆ i, ∑ i_1 ∈ j, (↑i).lintegral (μ i_1)) = fun s => ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<VAR>s : Finset ι<GOAL>⨆ i, ∑ i_1 ∈ s, (↑i).lintegral (μ i_1) = ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>⨆ i, ∑ i_1 ∈ ∅, (↑i).lintegral (μ i_1) = ∑ i ∈ ∅, ⨆ x, (↑x).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>hs : ⨆ i, ∑ i_1 ∈ s, (↑i).lintegral (μ i_1) = ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)<GOAL>⨆ i_1, ∑ i ∈ insert i s, (↑i_1).lintegral (μ i) = ∑ i ∈ insert i s, ⨆ x, (↑x).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>hs : ⨆ i, ∑ i_1 ∈ s, (↑i).lintegral (μ i_1) = ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)<GOAL>⨆ i_1, (↑i_1).lintegral (μ i) + ∑ i ∈ s, (↑i_1).lintegral (μ i) = (⨆ x, (↑x).lintegral (μ i)) + ⨆ i, ∑ i_1 ∈ s, (↑i).lintegral (μ i_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>hs : ⨆ i, ∑ i_1 ∈ s, (↑i).lintegral (μ i_1) = ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)<GOAL>∀ (i_1 j : { i // ↑i ≤ fun a => f a }), ∃ k, (↑i_1).lintegral (μ i) + ∑ i ∈ s, (↑j).lintegral (μ i) ≤ (↑k).lintegral (μ i) + ∑ i ∈ s, (↑k).lintegral (μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>ι : Type u_5<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>hs : ⨆ i, ∑ i_1 ∈ s, (↑i).lintegral (μ i_1) = ∑ i ∈ s, ⨆ x, (↑x).lintegral (μ i)<VAR>φ ψ : { i // ↑i ≤ fun a => f a }<GOAL>∃ k, (↑φ).lintegral (μ i) + ∑ i ∈ s, (↑ψ).lintegral (μ i) ≤ (↑k).lintegral (μ i) + ∑ i ∈ s, (↑k).lintegral (μ i)
<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>f : F[X]<VAR>h : Irreducible f<GOAL>f.natSepDegree ∣ f.natDegree
<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>f : F[X]<VAR>h : Irreducible f<VAR>q : ℕ<VAR>h✝ : ExpChar F q<GOAL>f.natSepDegree ∣ f.natDegree
<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>f : F[X]<VAR>h : Irreducible f<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>hf : HasSeparableContraction q f<GOAL>f.natSepDegree ∣ f.natDegree
<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>f : F[X]<VAR>h : Irreducible f<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>hf : HasSeparableContraction q f<GOAL>hf.degree ∣ f.natDegree
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P' Q' : Fin 3 → R<VAR>u v : Rˣ<GOAL>W'.add ((fun m => m • P') u) ((fun m => m • Q') v) ≈ W'.add P' Q'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝ : TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 0<GOAL>u ∈ comap (gauge s) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝ : TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 0<VAR>r : ℝ<VAR>hr₀ : r > 0<VAR>hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u<GOAL>u ∈ comap (gauge s) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝ : TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 0<VAR>r : ℝ<VAR>hr₀ : r > 0<VAR>hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u<VAR>x : E<VAR>hx : gauge s x < r⁻¹<GOAL>x ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝ : TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 0<VAR>r : ℝ<VAR>hr₀ : r > 0<VAR>hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u<VAR>c : ℝ<VAR>hc₀ : 0 < c<VAR>hcr : c < r⁻¹<VAR>y : E<VAR>hy : y ∈ s<VAR>hx : gauge s ((fun x => c • x) y) < r⁻¹<GOAL>(fun x => c • x) y ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝ : TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 0<VAR>r : ℝ<VAR>hr₀ : r > 0<VAR>hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u<VAR>c : ℝ<VAR>hc₀ : 0 < c<VAR>hcr : c < r⁻¹<VAR>y : E<VAR>hy : y ∈ s<VAR>hx : gauge s ((fun x => c • x) y) < r⁻¹<VAR>hrc : r < c⁻¹<GOAL>(fun x => c • x) y ∈ u
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>inst✝ : TopologicalSpace E<VAR>ha : Absorbent ℝ s<VAR>hb : Bornology.IsVonNBounded ℝ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝 0<VAR>r : ℝ<VAR>hr₀ : r > 0<VAR>hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u<VAR>c : ℝ<VAR>hc₀ : 0 < c<VAR>hcr : c < r⁻¹<VAR>hrc : r < c⁻¹<VAR>z : E<VAR>hz : z ∈ u<VAR>hy : (fun x => c⁻¹ • x) z ∈ s<VAR>hx : gauge s ((fun x => c • x) ((fun x => c⁻¹ • x) z)) < r⁻¹<GOAL>(fun x => c • x) ((fun x => c⁻¹ • x) z) ∈ u
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → PseudoMetricSpace (β i)<VAR>x y : PiLp ⊤ β<GOAL>dist x y = ⨆ i, dist (x i) (y i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>b0 : a * b ≠ 0<GOAL>a ≤ a * b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ClosedIicTopology α<VAR>f : β → α<VAR>a b : α<VAR>s : Set α<GOAL>BddAbove (closure s) ↔ BddAbove s
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>h : Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 l)<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : Tendsto (ofReal' ∘ fun n => ∑ i ∈ range n, f i) atTop (𝓝 ↑l)<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : Tendsto (fun x => ↑(∑ i ∈ range x, f i)) atTop (𝓝 ↑l)<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : Tendsto (fun x => ∑ i ∈ range x, ↑(f i)) atTop (𝓝 ↑l)<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : Tendsto (fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) (Filter.map ofReal' (𝓝[<] 1)) (𝓝 ↑l)<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : Tendsto ((fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal') (𝓝[<] 1) (𝓝 ↑l)<GOAL>Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Set.Iio 1 → dist x 1 < δ → dist (((fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal') x) ↑l < ε<GOAL>∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Set.Iio 1 → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Set.Iio 1 → dist x 1 < δ → dist (((fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal') x) ↑l < ε<VAR>a✝⁴ : ℝ<VAR>a✝³ : a✝⁴ > 0<VAR>x✝ a✝² : ℝ<VAR>a✝¹ : a✝² ∈ Set.Iio 1<VAR>a✝ : dist a✝² 1 < x✝<GOAL>dist (∑' (n : ℕ), f n * a✝² ^ n) l = dist (((fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal') a✝²) ↑l
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Set.Iio 1 → dist x 1 < δ → dist (((fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal') x) ↑l < ε<VAR>a✝⁴ : ℝ<VAR>a✝³ : a✝⁴ > 0<VAR>x✝ a✝² : ℝ<VAR>a✝¹ : a✝² ∈ Set.Iio 1<VAR>a✝ : dist a✝² 1 < x✝<GOAL>‖∑' (n : ℕ), f n * a✝² ^ n - l‖ = ‖∑' (n : ℕ), ↑(f n) * ↑a✝² ^ n - ↑l‖
<VAR>f : ℕ → ℝ<VAR>l : ℝ<VAR>m : Filter.map ofReal' (𝓝 l) ≤ 𝓝 ↑l<VAR>h : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, x ∈ Set.Iio 1 → dist x 1 < δ → dist (((fun z => ∑' (n : ℕ), ↑(f n) * z ^ n) ∘ ofReal') x) ↑l < ε<VAR>a✝⁴ : ℝ<VAR>a✝³ : a✝⁴ > 0<VAR>x✝ a✝² : ℝ<VAR>a✝¹ : a✝² ∈ Set.Iio 1<VAR>a✝ : dist a✝² 1 < x✝<GOAL>‖∑' (n : ℕ), f n * a✝² ^ n - l‖ = ‖↑(∑' (n : ℕ), f n * a✝² ^ n - l)‖
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<GOAL>↑(closure s) = List.prod '' {l | ∀ x ∈ l, x ∈ s}
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<GOAL>Set.range ⇑(FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>x : β<VAR>ht : t ∈ 𝓝 x<GOAL>a • t ∈ 𝓝 (a • x)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>inst✝ : ContinuousConstSMul α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>x : β<VAR>ht : t ∈ 𝓝 x<VAR>u : Set β<VAR>ut : u ⊆ t<VAR>u_open : IsOpen u<VAR>hu : x ∈ u<GOAL>a • t ∈ 𝓝 (a • x)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<VAR>h : p₁ -ᵥ p₂ = 0<GOAL>p₁ = p₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s