ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) =ᶠ[ae (μ.trim hm)] ↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>StronglyMeasurable (↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g))
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑(lpMeasSubgroupToLpTrim F p μ hm (f + g)) =ᶠ[ae μ] ↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑↑(f + g) =ᶠ[ae μ] ↑↑(lpMeasSubgroupToLpTrim F p μ hm f) + ↑↑(lpMeasSubgroupToLpTrim F p μ hm g)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑↑(f + g) =ᶠ[ae μ] fun x => ↑↑↑f x + ↑↑↑g x
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>ι : Type u_6<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f g : ↥(lpMeasSubgroup F m p μ)<GOAL>↑↑↑f + ↑↑↑g =ᶠ[ae μ] fun x => ↑↑↑f x + ↑↑↑g x
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<VAR>p : Submodule K V₁<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hp : p ≠ ⊥<GOAL>IsCompl (LinearMap.ker f) p
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<VAR>p : Submodule K V₁<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hp : p ≠ ⊥<GOAL>finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V₁<VAR>f : Dual K V₁<VAR>hf : f ≠ 0<VAR>p : Submodule K V₁<VAR>hpf : Disjoint (LinearMap.ker f) p<VAR>hp : p ≠ ⊥<VAR>this : finrank K ↥(LinearMap.ker f ⊔ p) = finrank K ↥(LinearMap.ker f) + finrank K ↥p<GOAL>finrank K ↥⊤ ≤ finrank K ↥(LinearMap.ker f ⊔ p)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y Z : C<GOAL>(BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫ ((ℬ (tensorObj ℬ X Y) Z).isLimit.conePointUniqueUpToIso (ℬ Z (tensorObj ℬ X Y)).isLimit.swapBinaryFan).hom ≫ (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv = (ℬ X (ℬ Z Y).cone.pt).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X) (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫ ((ℬ Y Z).isLimit.conePointUniqueUpToIso (ℬ Z Y).isLimit.swapBinaryFan).hom)) ≫ (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫ (ℬ (ℬ Z X).cone.pt Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫ ((ℬ X Z).isLimit.conePointUniqueUpToIso (ℬ Z X).isLimit.swapBinaryFan).hom) (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y Z : C<GOAL>∀ (j : Discrete WalkingPair), ((BinaryFan.associatorOfLimitCone ℬ X Y Z).inv ≫ ((ℬ (tensorObj ℬ X Y) Z).isLimit.conePointUniqueUpToIso (ℬ Z (tensorObj ℬ X Y)).isLimit.swapBinaryFan).hom ≫ (BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) ≫ (ℬ (ℬ Z X).cone.pt Y).cone.π.app j = ((ℬ X (ℬ Z Y).cone.pt).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ Y Z).cone.pt).cone ≫ 𝟙 X) (BinaryFan.snd (ℬ X (ℬ Y Z).cone.pt).cone ≫ ((ℬ Y Z).isLimit.conePointUniqueUpToIso (ℬ Z Y).isLimit.swapBinaryFan).hom)) ≫ (BinaryFan.associatorOfLimitCone ℬ X Z Y).inv ≫ (ℬ (ℬ Z X).cone.pt Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X Z).cone.pt Y).cone ≫ ((ℬ X Z).isLimit.conePointUniqueUpToIso (ℬ Z X).isLimit.swapBinaryFan).hom) (BinaryFan.snd (ℬ (ℬ X Z).cone.pt Y).cone ≫ 𝟙 Y))) ≫ (ℬ (ℬ Z X).cone.pt Y).cone.π.app j
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>e' : PartialHomeomorph Y Z<VAR>f'' : Z ≃ₜ Z'<GOAL>(e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G✝ : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>w ∈ Gᶜ.neighborSet v ↔ w ∈ (G.neighborSet v)ᶜ \ {v}
<VAR>α : Type u_1<VAR>a : α<VAR>m n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>(l.set m a).get? n = if m = n then some a else l.get? n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>(map (fun r => X + C r) s).prod.coeff k = s.esymm (card s - k)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>s.esymm (card s - k) = (∑ j ∈ Finset.range (card s + 1), C (s.esymm j) * X ^ (card s - j)).coeff k
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>s.esymm (card s - k) = ∑ x ∈ Finset.range (card s + 1), if k = card s - x then s.esymm x else 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>s.esymm (card s - k) = if k = card s - (card s - k) then s.esymm (card s - k) else 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>∀ b ∈ Finset.range (card s + 1), b ≠ card s - k → (if k = card s - b then s.esymm b else 0) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>s : Multiset R<VAR>k : ℕ<VAR>h : k ≤ card s<GOAL>card s - k ∈ Finset.range (card s + 1)
<VAR>α : Type u_1<VAR>l : List α<VAR>inst✝ : DecidableEq α<VAR>a x✝¹ : { x // x ∈ l }<VAR>x✝ : x✝¹ ∈ l.attach<GOAL>(x✝¹ == a) = true ↔ (↑x✝¹ == ↑a) = true
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>update x i a ≤ x ↔ a ≤ x i
<VAR>x : EReal<GOAL>x + ⊤ = ⊤ ↔ x ≠ ⊥
<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>P : Type u_6<VAR>inst✝³ : Group N<VAR>inst✝² : Group P<VAR>K✝ : Subgroup G<VAR>G₁ : Type u_7<VAR>G₂ : Type u_8<VAR>inst✝¹ : Group G₁<VAR>inst✝ : Group G₂<VAR>K : Subgroup G₂<VAR>f : G₁ →* G₂<VAR>h : f.range ≤ K<VAR>k : ↥K<GOAL>k ∈ f.range.subgroupOf K ↔ k ∈ (f.codRestrict K ⋯).range
<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>P : Type u_6<VAR>inst✝³ : Group N<VAR>inst✝² : Group P<VAR>K✝ : Subgroup G<VAR>G₁ : Type u_7<VAR>G₂ : Type u_8<VAR>inst✝¹ : Group G₁<VAR>inst✝ : Group G₂<VAR>K : Subgroup G₂<VAR>f : G₁ →* G₂<VAR>h : f.range ≤ K<VAR>k : ↥K<GOAL>∀ (a : G₁), f a = K.subtype k ↔ (f.codRestrict K ⋯) a = k
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy0 : 0 ≤ y<GOAL>x ^ y = ⊤ → x = ⊤
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy0 : 0 ≤ y<GOAL>x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y → 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✝⁴ : FunLike F α β<VAR>inst✝³ : Inf α<VAR>inst✝² : Inf β<VAR>inst✝¹ : Inf γ<VAR>inst✝ : Inf δ<VAR>g : InfHom β γ<VAR>f₁ f₂ : InfHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Cycle α<VAR>hs : s.Nodup<VAR>x : α<VAR>hx : x ∈ s<GOAL>s.next hs x hx ∈ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>a✝ : List α<VAR>hs : Nodup (Quot.mk Setoid.r a✝)<VAR>hx : x ∈ Quot.mk Setoid.r a✝<GOAL>next (Quot.mk Setoid.r a✝) hs x hx ∈ Quot.mk Setoid.r a✝
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>a✝ : List α<VAR>hs : Nodup (Quot.mk Setoid.r a✝)<VAR>hx : x ∈ Quot.mk Setoid.r a✝<GOAL>x ∈ a✝
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t s₁ s₂ t₁✝ t₂✝ u : Set E<VAR>x y : E<VAR>s t₁ t₂ : Set E<GOAL>convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f✝ : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f : X ⟶ Z<GOAL>f ≫ 𝟙 Z = 𝟙 X ≫ f
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>x y : ↥S.leftInv<GOAL>↑({ toFun := S.fromLeftInv, map_one' := ⋯ }.toFun (x * y)) = ↑({ toFun := S.fromLeftInv, map_one' := ⋯ }.toFun x * { toFun := S.fromLeftInv, map_one' := ⋯ }.toFun y)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto (fun a => a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Subsingleton ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<VAR>i : ι<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Subsingleton ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<VAR>i : ι<VAR>s : Set α<VAR>left✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hfε : eLpNorm (sᶜ.indicator (f i)) p μ < ↑ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p : ℝ≥0∞<VAR>inst✝ : Subsingleton ι<VAR>hp_top : p ≠ ⊤<VAR>f : ι → α → β<VAR>hf : ∀ (i : ι), Memℒp (f i) p μ<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>hε_top : ¬↑ε = ⊤<VAR>i : ι<VAR>s : Set α<VAR>left✝ : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>hfε : eLpNorm (sᶜ.indicator (f i)) p μ < ↑ε<VAR>j : ι<GOAL>eLpNorm (sᶜ.indicator (f j)) p μ ≤ ↑ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>¬Nonempty ↑s ↔ s = ∅
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddGroup (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommGroup γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂<GOAL>(f - g).sum h = f.sum h - g.sum h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddGroup (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommGroup γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂<VAR>this : (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) (f - g) = (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) f - (liftAddHom fun a => AddMonoidHom.ofMapSub (h a) ⋯) g<GOAL>(f - g).sum h = f.sum h - g.sum h
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddGroup (β i)<VAR>inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝ : AddCommGroup γ<VAR>f g : Π₀ (i : ι), β i<VAR>h : (i : ι) → β i → γ<VAR>h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂<VAR>this : ((f - g).sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) = (f.sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)) - g.sum fun x => ⇑(AddMonoidHom.ofMapSub (h x) ⋯)<GOAL>(f - g).sum h = f.sum h - g.sum h
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t s : Set α<VAR>ht : NullMeasurableSet t μ<GOAL>μ (s ∩ t) + μ (s \ t) = μ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t s : Set α<VAR>ht : NullMeasurableSet t μ<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t s : Set α<VAR>ht : NullMeasurableSet t μ<VAR>s' : Set α<VAR>hsub : s ⊆ s'<VAR>hs'm : MeasurableSet s'<VAR>hs' : μ s' = μ s<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t s : Set α<VAR>ht : NullMeasurableSet t μ<VAR>s' : Set α<VAR>hsub : s ⊆ s'<VAR>hs' : μ s' = μ s<VAR>hs'm : NullMeasurableSet s' μ<GOAL>μ (s ∩ t) + μ (s \ t) ≤ μ s
<VAR>α : Type u_1<VAR>l : List α<GOAL>(toList ⟨l, ⋯⟩).Nodup ↔ Function.Injective (get ⟨l, ⋯⟩)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra S B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S B<VAR>U V : Subalgebra S A<VAR>H : restrictScalars R U = restrictScalars R V<VAR>x : A<GOAL>x ∈ U ↔ x ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<GOAL>∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<GOAL>∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<GOAL>∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<GOAL>∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<GOAL>∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<GOAL>∀ (x : α × ι), (∀ᶠ (y : ι) in p, (F ((Equiv.prodAssoc α ι ι) (x, y)).swap.1.1 ((Equiv.prodAssoc α ι ι) (x, y)).swap.2, F ((Equiv.prodAssoc α ι ι) (x, y)).swap.1.2 ((Equiv.prodAssoc α ι ι) (x, y)).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) (x, y)).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) (x, y)).swap.2))) → (f x.swap.2, F x.swap.1 x.swap.2) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<GOAL>∀ (a : α) (b : ι), (∀ᶠ (x : ι) in p, (F b a, F x a) ∈ t) → Tendsto (fun n => F n a) p (𝓝 (f a)) → (f a, F b a) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<VAR>x : α<VAR>n : ι<VAR>hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t<VAR>hm' : Tendsto (fun n => F n x) p (𝓝 (f x))<GOAL>(f x, F n x) ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t<VAR>htmem : t ○ t ⊆ u<VAR>hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))<VAR>this : ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p, (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2, F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈ t ∧ Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))<VAR>x : α<VAR>n : ι<VAR>hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t<VAR>hm' : Tendsto (fun n => F n x) p (𝓝 (f x))<GOAL>∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t