ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>mapFun (⇑f) n.unaryCast = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∈ lowerClosure ↑s<VAR>ht : a ∈ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = s.truncatedSup a ⊔ t.truncatedSup a
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α✝ → β → β<VAR>op : α✝ → α✝ → α✝<VAR>inst✝³ : Monoid α✝<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α✝ β<VAR>α : Type u_6<VAR>inst✝ : CommMonoid α<VAR>s : Multiset α<GOAL>s.noncommProd ⋯ = s.prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α✝ → β → β<VAR>op : α✝ → α✝ → α✝<VAR>inst✝³ : Monoid α✝<VAR>inst✝² : Monoid β<VAR>inst✝¹ : FunLike F α✝ β<VAR>α : Type u_6<VAR>inst✝ : CommMonoid α<VAR>a✝ : List α<GOAL>noncommProd ⟦a✝⟧ ⋯ = prod ⟦a✝⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<VAR>B : Set ↑M.E<GOAL>(M.restrictSubtype M.E).Base B ↔ M.Base ↑B
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<GOAL>N.incl.ker = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : HasTrivialRadical R L<GOAL>IsLieAbelian ↥↑(radical R L)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : HasTrivialRadical R L<GOAL>IsLieAbelian ↥↑⊥
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S S' : C ⥤ D<VAR>f : CostructuredArrow S T<GOAL>(f.homMk' (𝟙 f.left)).left = (eqToHom ⋯).left
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E✝ : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E✝<VAR>E : Type u_3<VAR>inst✝ : PseudoMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>dist (f x) (f y) ≤ (eVariationOn f s).toReal
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E✝ : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E✝<VAR>E : Type u_3<VAR>inst✝ : PseudoMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>h : BoundedVariationOn f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>edist (f x) (f y) ≤ eVariationOn f s
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : H.IsComplement' K<GOAL>K.IsComplement' H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : H.IsComplement' K<VAR>ϕ : ↥H × ↥K ≃ ↥K × ↥H := { toFun := fun x => (x.2⁻¹, x.1⁻¹), invFun := fun x => (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }<GOAL>K.IsComplement' H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : H.IsComplement' K<VAR>ϕ : ↥H × ↥K ≃ ↥K × ↥H := { toFun := fun x => (x.2⁻¹, x.1⁻¹), invFun := fun x => (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }<VAR>ψ : G ≃ G := { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := ⋯, right_inv := ⋯ }<GOAL>K.IsComplement' H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : H.IsComplement' K<VAR>ϕ : ↥H × ↥K ≃ ↥K × ↥H := { toFun := fun x => (x.2⁻¹, x.1⁻¹), invFun := fun x => (x.2⁻¹, x.1⁻¹), left_inv := ⋯, right_inv := ⋯ }<VAR>ψ : G ≃ G := { toFun := fun g => g⁻¹, invFun := fun g => g⁻¹, left_inv := ⋯, right_inv := ⋯ }<GOAL>(⇑ψ ∘ fun x => ↑x.1 * ↑x.2) = (fun x => ↑x.1 * ↑x.2) ∘ ⇑ϕ
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : CommRing C<VAR>inst✝³ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝² : Fintype ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι'<VAR>b : ι → B<VAR>P : Matrix ι ι A<GOAL>discr A (P.map ⇑(algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f x✝)<VAR>g' : TangentSpace I' (f x✝) →L[𝕜] TangentSpace I'' (g (f x✝))<VAR>x : M<GOAL>(if MDifferentiableWithinAt I I' f univ x then fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x)) else 0) = if MDifferentiableAt I I' f x then fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x)) else 0
<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>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 ≤ s2<GOAL>s1.direction ≤ s2.direction
<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>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<VAR>h : s1 ≤ s2<GOAL>Submodule.span k (↑s1 -ᵥ ↑s1) ≤ Submodule.span k (↑s2 -ᵥ ↑s2)
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<GOAL>↑l = term I ho :: ↑l.Tail
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<GOAL>term I ho :: (↑l).tail = term I ho :: ↑l.Tail
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>m n : ZNum<GOAL>↑(m * n) = ↑m * ↑n
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(l.balance' x r).dual = r.dual.balance' x l.dual
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<GOAL>(if l.size + r.size ≤ 1 then l.node' x r else if delta * l.size < r.size then l.rotateL x r else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual = if l.size + r.size ≤ 1 then r.dual.node' x l.dual else if delta * r.size < l.size then r.dual.rotateL x l.dual else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : ¬l.size + r.size ≤ 1<VAR>h_1 : delta * l.size < r.size<VAR>h_2 : delta * r.size < l.size<GOAL>r.dual.rotateR x l.dual = r.dual.rotateL x l.dual
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : NullMeasurableSet s μ<VAR>hs₀ : μ s ≠ 0<VAR>hsc₀ : μ sᶜ ≠ 0<GOAL>⨍⁻ (x : α), f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (thickening R s) ≠ ⊤<GOAL>Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (closure s)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : ∃ R > 0, μ (thickening R s) ≠ ⊤<GOAL>Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ (⋂ δ, ⋂ (_ : 0 < δ), thickening δ s)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<GOAL>((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 E<VAR>inst✝³ : InnerProductSpace 𝕜 F<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>U : Submodule 𝕜 E<VAR>inst✝ : CompleteSpace ↥U<VAR>this : ((orthogonalProjection U).comp (T.comp (adjoint (orthogonalProjection U)))).IsPositive<GOAL>((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : CommRing α<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M : Matrix n n R<VAR>i k : n<GOAL>f.mapMatrix M.adjugate i k = (f.mapMatrix M).adjugate i k
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype m<VAR>inst✝² : CommRing α<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>M : Matrix n n R<VAR>i k : n<VAR>this : Pi.single i 1 = ⇑f ∘ Pi.single i 1<GOAL>f.mapMatrix M.adjugate i k = (f.mapMatrix M).adjugate i k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R S T : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>H : Symmetric R<VAR>H₁ : ∀ (x : α), x ∈ l → R x x<VAR>H₂ : Pairwise R l<GOAL>Pairwise (flip R) l
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Set α<GOAL>a ∈ stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Set α<VAR>h : a • s = s<VAR>b : α<GOAL>a • b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Set α<VAR>h : ∀ (b : α), a • b ∈ s ↔ b ∈ s<GOAL>a • s = s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Set α<VAR>h : ∀ (b : α), a • b ∈ s ↔ b ∈ s<GOAL>∀ (x : α), a⁻¹ • x ∈ s ↔ x ∈ s
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Ring R<VAR>i : V<GOAL>(lapMatrix R G *ᵥ fun x => 1) i = 0 i
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Ring R<VAR>i : V<GOAL>↑(G.degree i) * 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁₁ : X₁ ⟶ Y₁<VAR>f₁₂ : X₁ ⟶ Y₂<VAR>f₂₁ : X₂ ⟶ Y₁<VAR>f₂₂ : X₂ ⟶ Y₂<VAR>f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂<GOAL>ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst) (biprod.inr ≫ f ≫ biprod.snd) = f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>k : ℕ<GOAL>derivedSeries R (↥↑I) k = ⊥ ↔ derivedSeriesOfIdeal R L k I = ⊥
<VAR>θ : Angle<GOAL>θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>ι✝ : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ g : ℝ → E<VAR>μ : Measure ℝ<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℝ → E<VAR>h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b<GOAL>∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<VAR>h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1<VAR>y : E<GOAL>y ∈ ⊥ ↔ y ∈ ⊤
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<VAR>h : ∀ (x : E), finrank F ↥F⟮x⟯ = 1<VAR>y : E<GOAL>y ∈ ⊥
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<GOAL>HasSum (fun i => lp.single p i (↑f i)) f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<GOAL>HasSum (fun i => lp.single p i (↑f i)) f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<GOAL>HasSum (fun i => lp.single p i (↑f i)) f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : HasSum (fun i => ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)<GOAL>HasSum (fun i => lp.single p i (↑f i)) f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<GOAL>∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, lp.single p b (↑f b)) f < ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, lp.single p b (↑f b)) f < ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∀ (x : Finset α), dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal → dist (∑ b ∈ x, lp.single p b (↑f b)) f < ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : dist (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal<GOAL>dist (∑ b ∈ s, lp.single p b (↑f b)) f < ε
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : dist (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal<GOAL>dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : dist (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) < ε ^ p.toReal<GOAL>dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖↑f b‖ ^ p.toReal| < ε ^ p.toReal<GOAL>‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖↑f b‖ ^ p.toReal| < ε ^ p.toReal<VAR>H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal<GOAL>‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| < ε ^ p.toReal<VAR>H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal<GOAL>‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝⁵ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : NormedRing 𝕜<VAR>inst✝³ : (i : α) → Module 𝕜 (E i)<VAR>inst✝² : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fact (1 ≤ p)<VAR>hp : p ≠ ⊤<VAR>f : ↥(lp E p)<VAR>hp₀ : 0 < p<VAR>hp' : 0 < p.toReal<VAR>this✝ : ∀ ε > 0, ∀ᶠ (x : Finset α) in Filter.atTop, dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>s : Finset α<VAR>hs : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| < ε ^ p.toReal<VAR>H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal<VAR>this : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| = ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal<GOAL>‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
<VAR>num : Int<VAR>den g : Nat<VAR>den_nz : den ≠ 0<VAR>e : g = num.natAbs.gcd den<GOAL>(num.div ↑g).natAbs = num.natAbs / g
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂✝ : Type u_13<VAR>N₃✝ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹² : CommSemiring 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>N : Type u_17<VAR>N₂ : Type u_18<VAR>N₃ : Type u_19<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : AddCommMonoid N₃<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N₂<VAR>inst✝ : Module R N₃<VAR>e₁ : M ≃ₗ[R] N<VAR>e₂ : M₂ ≃ₗ[R] N₂<VAR>e₃ : M₃ ≃ₗ[R] N₃<VAR>f : M →ₗ[R] M₂<VAR>g : M₂ →ₗ[R] M₃<VAR>x✝ : N<GOAL>((e₁.arrowCongr e₃) (g ∘ₗ f)) x✝ = ((e₂.arrowCongr e₃) g ∘ₗ (e₁.arrowCongr e₂) f) x✝
<VAR>α : Type u_1<VAR>a : ℤ<VAR>ha : 0 < a<GOAL>0 < a / a
<VAR>α : Type u_1<VAR>a : ℤ<VAR>ha : 0 < a<GOAL>0 < 1
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<GOAL>Setoid.IsPartition (Set.range fun a => orbit G a)