ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>S✝ : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁹ : Semiring R✝<VAR>inst✝¹⁸ : Semiring S✝<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : AddCommMonoid M₃<VAR>inst✝¹³ : AddCommMonoid N₁<VAR>inst✝¹² : AddCommMonoid N₂<VAR>inst✝¹¹ : AddCommMonoid N₃<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M₂<VAR>inst✝⁸ : Module S✝ M₃<VAR>σ : R✝ →+* S✝<VAR>fₗ gₗ : M →ₗ[R✝] M₂<VAR>f✝ g : M →ₛₗ[σ] M₃<VAR>R : Type u_17<VAR>S : Type u_18<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : SMul R M<VAR>inst✝⁵ : Module S M<VAR>inst✝⁴ : SMul R M₂<VAR>inst✝³ : Module S M₂<VAR>inst✝² : SMul R S<VAR>inst✝¹ : CompatibleSMul M M₂ R S<VAR>inst✝ : IsScalarTower R S M₂<VAR>f : M →ₗ[S] M₂<VAR>hf : Injective ⇑f<VAR>r : R<VAR>s : S<VAR>x✝ : M<GOAL>f ((r • s) • x✝) = f (r • s • x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>this : 0 ≤ ∫ (a : α), ‖↑↑(condexpIndL1Fin hm hs hμs x) a‖ ∂μ<GOAL>‖condexpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>this : 0 ≤ ∫ (a : α), ‖↑↑(condexpIndL1Fin hm hs hμs x) a‖ ∂μ<GOAL>∫⁻ (x_1 : α), ↑‖↑↑(condexpIndL1Fin hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ENNReal.ofReal ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>this : 0 ≤ ∫ (a : α), ‖↑↑(condexpIndL1Fin hm hs hμs x) a‖ ∂μ<GOAL>Integrable (↑↑(condexpIndL1Fin hm hs hμs x)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>this : 0 ≤ ∫ (a : α), ‖↑↑(condexpIndL1Fin hm hs hμs x) a‖ ∂μ<VAR>h_eq : ∫⁻ (a : α), ↑‖↑↑(condexpIndL1Fin hm hs hμs x) a‖₊ ∂μ = ∫⁻ (a : α), ↑‖↑↑(condexpIndSMul hm hs hμs x) a‖₊ ∂μ<GOAL>∫⁻ (x_1 : α), ↑‖↑↑(condexpIndL1Fin hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ENNReal.ofReal ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<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>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>this : 0 ≤ ∫ (a : α), ‖↑↑(condexpIndL1Fin hm hs hμs x) a‖ ∂μ<VAR>h_eq : ∫⁻ (a : α), ↑‖↑↑(condexpIndL1Fin hm hs hμs x) a‖₊ ∂μ = ∫⁻ (a : α), ↑‖↑↑(condexpIndSMul hm hs hμs x) a‖₊ ∂μ<GOAL>∫⁻ (a : α), ↑‖↑↑(condexpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p q : R[X]<VAR>inst✝³ : CommRing T<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<GOAL>rootSet 1 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 a : α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>IsGreatest (↑(insert a s)) (max (s.max' H) 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 a : α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>IsGreatest (insert a ↑s) (max a (s.max' H))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : autoParam s.Finite _auto✝<GOAL>(s \ {a}).ncard < s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : autoParam s.Finite _auto✝<GOAL>(s \ {a}).ncard < (s \ {a}).ncard + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>hne : a ≠ b<GOAL>{a, b} \ {a} = {b}
<VAR>α : Type u<VAR>inst✝ : CommMonoid α<VAR>x y : α<VAR>u : αˣ<GOAL>x /ₚ u * y = x * y /ₚ u
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>x z : ℂ<GOAL>z * x = x * z
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<GOAL>P.parts.card ≤ s.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<GOAL>P.parts.card ≤ ⊥.parts.card
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : PseudoMetricSpace P<VAR>inst✝⁵ : NormedAddTorsor V P<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : MetricSpace Q<VAR>inst✝² : NormedAddTorsor W Q<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : NormedSpace ℝ W<VAR>p₁ p₂ p₃ p₄ : V<GOAL>dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝² : Category.{u_4, u_3} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>K : HomologicalComplex C c<VAR>e : c.Embedding c'<VAR>i' j' : ι'<VAR>i j : ι<VAR>hi : e.f i = i'<VAR>hj : e.f j = j'<GOAL>(K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0<GOAL>LinearMap.range g.toLinearPMap.toFun = map (LinearMap.snd R E F) g
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>2 * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) + ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) = ↑C.u⁻¹ ^ 4 * (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (W.a₁ ^ 2 + 4 * W.a₂) + 6 * C.r ^ 2)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p q : ℝ<VAR>f g : ι → ℝ≥0<VAR>hp : 1 ≤ p<VAR>hf_sum : Summable fun a => f a ^ p<VAR>hg_sum : Summable fun a => g a ^ p<GOAL>(Summable fun a => (f a + g a) ^ p) ∧ (∑' (a : ι), (f a + g a) ^ p) ^ (1 / p) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) + (∑' (a : ι), g a ^ p) ^ (1 / p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t : Set α<VAR>f✝ g : α → M<VAR>a : α<VAR>s : Set α<VAR>f : α → M<GOAL>(s ∩ mulSupport f).mulIndicator f = s.mulIndicator f
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>f : X → Bool<VAR>b : Bool<GOAL>Continuous f ↔ IsClopen (f ⁻¹' {b})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MonoidWithZero α<VAR>a : α<VAR>h : a ~ᵤ 0<GOAL>a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MonoidWithZero α<VAR>a : α<VAR>h✝ : a ~ᵤ 0<VAR>u : αˣ<VAR>h : 0 * ↑u = a<GOAL>a = 0
<VAR>α : Sort u_1<VAR>n m : Nat<VAR>f : α → Fin (n + 1) → α<VAR>x : α<VAR>h : m < n + 1<GOAL>foldl.loop (n + 1) f x m = foldl.loop n (fun x i => f x i.succ) (f x ⟨m, h⟩) m
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>M : Type ?u.50075<VAR>inst✝ : Monoid M<VAR>x : M<VAR>hx : IsOfFinOrder x<GOAL>x * x ^ (orderOf x - 1) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>M : Type ?u.50075<VAR>inst✝ : Monoid M<VAR>x : M<VAR>hx : IsOfFinOrder x<GOAL>x ^ (orderOf x - 1) * x = 1
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ι → ℂ<GOAL>∫ (v : ι → ℝ), cexp (-b * ∑ i : ι, ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i)) = (↑π / b) ^ (↑(Fintype.card ι) / 2) * cexp ((∑ i : ι, c i ^ 2) / (4 * b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hw₁ : ↑s w = 0<VAR>hw₂ : w ⊆ u<VAR>hwt : v ⊆ w<GOAL>↑s v = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hw₁ : ↑s w = 0<VAR>hw₂ : w ⊆ u<VAR>hwt : v ⊆ w<VAR>this : ↑s v + ↑s (w \ v) = 0<GOAL>↑s v = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hw₁ : ↑s w = 0<VAR>hw₂ : w ⊆ u<VAR>hwt : v ⊆ w<VAR>this : ↑s v + ↑s (w \ v) = 0<VAR>h₁ : 0 ≤ ↑s v<GOAL>↑s v = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hw₁ : ↑s w = 0<VAR>hw₂ : w ⊆ u<VAR>hwt : v ⊆ w<VAR>this : ↑s v + ↑s (w \ v) = 0<VAR>h₁ : 0 ≤ ↑s v<VAR>h₂ : 0 ≤ ↑s (w \ v)<GOAL>↑s v = 0
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>N : Matroid α<VAR>h : N <r M<GOAL>N = M ↾ N.E
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>hy : y ≤ x<VAR>h : x \ y = z<GOAL>x \ z = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ↪o β<VAR>he : (range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Ioo x y = Ioo (e x) (e y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>h : ∀ x ∈ s, f x ∈ t<GOAL>t.disjiUnion (fun a => filter (fun x => f x = a) s) ⋯ = s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : 0 < ‖k‖<GOAL>k • p.closedBall 0 r = p.closedBall 0 (‖k‖ * r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : 0 < ‖k‖<GOAL>p.closedBall 0 (‖k‖ * r) ⊆ k • p.closedBall 0 r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : 0 < ‖k‖<VAR>x : E<GOAL>x ∈ p.closedBall 0 (‖k‖ * r) → x ∈ k • p.closedBall 0 r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : 0 < ‖k‖<VAR>x : E<GOAL>p x ≤ ‖k‖ * r → ∃ y ∈ p.closedBall 0 r, k • y = x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>hk : 0 < ‖k‖<VAR>x : E<VAR>hx : p x ≤ ‖k‖ * r<GOAL>k • k⁻¹ • x = x
<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>f g : ContinuousMultilinearMap 𝕜 E F<VAR>x✝ : ⨂[𝕜] (i : ι), E i<GOAL>((fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) (f + g)) x✝ = ((fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) f + (fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯) g) x✝
<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>a : 𝕜<VAR>f : ContinuousMultilinearMap 𝕜 E F<VAR>x✝ : ⨂[𝕜] (i : ι), E i<GOAL>({ toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯ }.toFun (a • f)) x✝ = ((RingHom.id 𝕜) a • { toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯ }.toFun f) x✝
<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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<VAR>x : (i : ι) → E i<GOAL>‖(lift.symm ↑l) x‖ ≤ ‖l‖ * ∏ i : ι, ‖x 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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<VAR>x : (i : ι) → E i<GOAL>‖l ((tprod 𝕜) x)‖ ≤ ‖l‖ * ∏ i : ι, ‖x 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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<VAR>x : (i : ι) → E i<GOAL>‖(tprod 𝕜) x‖ ≤ ∏ i : ι, ‖x 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>f : ContinuousMultilinearMap 𝕜 E F<VAR>x : (i : ι) → E i<GOAL>((fun l => (lift.symm ↑l).mkContinuous ‖l‖ ⋯) ({ toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯, map_smul' := ⋯ }.toFun f)) x = f x
<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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<GOAL>{ toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun l => (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l) = l
<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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<GOAL>↑({ toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun l => (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l)) = ↑l
<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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<GOAL>(↑({ toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun l => (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l))).compMultilinearMap (tprod 𝕜) = (↑l).compMultilinearMap (tprod 𝕜)
<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>l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F<VAR>m : (i : ι) → E i<GOAL>((↑({ toFun := fun f => (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯, map_add' := ⋯, map_smul' := ⋯ }.toFun ((fun l => (lift.symm ↑l).mkContinuous ‖l‖ ⋯) l))).compMultilinearMap (tprod 𝕜)) m = ((↑l).compMultilinearMap (tprod 𝕜)) m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌈1⌉ = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : FiniteDimensional k V<VAR>p : ι → P<VAR>hi : AffineIndependent k p<VAR>a✝ : Nontrivial ι<VAR>inhabited_h : Inhabited ι<GOAL>_root_.Finite ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : FiniteDimensional k V<VAR>p : ι → P<VAR>a✝ : Nontrivial ι<VAR>inhabited_h : Inhabited ι<VAR>hi : LinearIndependent k fun i => p ↑i -ᵥ p default<GOAL>_root_.Finite ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>inst✝ : FiniteDimensional k V<VAR>p : ι → P<VAR>a✝ : Nontrivial ι<VAR>inhabited_h : Inhabited ι<VAR>hi : LinearIndependent k fun i => p ↑i -ᵥ p default<VAR>this : IsNoetherian k V := IsNoetherian.iff_fg.mpr inferInstance<GOAL>_root_.Finite ι
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<GOAL>∀ᵐ (x : E) ∂μ, lineDeriv ℝ f x (∑ i ∈ s, a i • v i) = ∑ i ∈ s, a i • lineDeriv ℝ f x (v i)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<GOAL>∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ = ∫ (x : E), g x • ∑ i ∈ s, (a i • fun x => lineDeriv ℝ f x (v i)) x ∂μ