ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x y : α<VAR>r : ℝ<VAR>h : dist x y ≤ K * r<VAR>rpos : 0 < r<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<VAR>H : closedBall y r ⊆ closedBall x (R / 4)<GOAL>∃ r_1, closedBall y r ⊆ closedBall x r_1 ∧ μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x y : α<VAR>r : ℝ<VAR>h : dist x y ≤ K * r<VAR>rpos : 0 < r<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<VAR>H : closedBall y r ⊆ closedBall x (R / 4)<VAR>hr : r ≤ R<GOAL>∃ r_1, closedBall y r ⊆ closedBall x r_1 ∧ μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : IsUnifLocDoublingMeasure μ<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>K : ℝ<VAR>x y : α<VAR>r : ℝ<VAR>h : dist x y ≤ K * r<VAR>rpos : 0 < r<VAR>R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)<VAR>H : closedBall y r ⊆ closedBall x (R / 4)<VAR>hr : R < r<GOAL>∃ r_1, closedBall y r ⊆ closedBall x r_1 ∧ μ (closedBall x (3 * r_1)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall y r)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set α<GOAL>TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set α<VAR>this : Finite ↑I<GOAL>TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
<VAR>K : Type ?u.613136<VAR>L : Type ?u.613139<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>hpq : Associated p q<GOAL>(aeval (root q)) p = 0
<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 n<VAR>inst✝³ : NonAssocSemiring α<VAR>inst✝² : NonAssocSemiring β<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : NonAssocSemiring S<VAR>f : R →+* S<VAR>v w : n → R<GOAL>f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j x✝ : Fin n<GOAL>↑((last n).succAbove x✝) = ↑x✝.castSucc
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<VAR>l : List α<GOAL>(b :: l).erase a = eraseP (fun x => a == x) (b :: l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : β → α → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>scanl f b (a :: l) = [b] ++ scanl f (f b a) l
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>F : ι → α × β<GOAL>BddAbove (range F) ↔ BddAbove (range (Prod.fst ∘ F)) ∧ BddAbove (range (Prod.snd ∘ F))
<VAR>m n✝ a✝ b✝ c d a b n : ℤ<GOAL>a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
<VAR>m n✝ a✝ b✝ c d a b n : ℤ<GOAL>n ∣ b - a ↔ ∃ t, b = a + n * t
<VAR>R : Type u_1<VAR>inst✝ : Semigroup R<VAR>a b : R<VAR>ab : IsLeftRegular (a * b)<GOAL>Function.Injective ((fun x => a * x) ∘ fun x => b * x)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<GOAL>count a s = card (filter (fun x => a = x) s)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CharP R p<VAR>x : 𝕎 (ZMod p)<GOAL>frobenius x = x
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>Φ : κ → Finset ι := fun k => (b.repr (v k)).support<GOAL>lift.{w', w} #ι ≤ lift.{w, w'} #κ
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>Φ : κ → Finset ι := fun k => (b.repr (v k)).support<VAR>w₁ : #ι ≤ #↑(range Φ)<GOAL>lift.{w', w} #ι ≤ lift.{w, w'} #κ
<VAR>ι✝¹ : Type u_1<VAR>ι' : Type u_2<VAR>R✝ : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M✝ : Type u_6<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Nontrivial R<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>ι : Type w<VAR>b : Basis ι R M<VAR>inst✝ : Infinite ι<VAR>κ : Type w'<VAR>v : κ → M<VAR>i : LinearIndependent R v<VAR>m : i.Maximal<VAR>Φ : κ → Finset ι := fun k => (b.repr (v k)).support<VAR>w₁ : #ι ≤ #↑(range Φ)<VAR>w₂ : lift.{w', w} #↑(range Φ) ≤ lift.{w, w'} #κ<GOAL>lift.{w', w} #ι ≤ lift.{w, w'} #κ
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>toOneHom✝¹ : OneHom M N<VAR>map_mul'✝¹ : ∀ (x y : M), toOneHom✝¹.toFun (x * y) = toOneHom✝¹.toFun x * toOneHom✝¹.toFun y<VAR>map_units'✝¹ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑y)<VAR>surj'✝¹ : ∀ (z : N), ∃ x, z * (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun ↑x.2 = (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x.1<VAR>exists_of_eq✝¹ : ∀ (x y : M), (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun x = (↑{ toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹ }).toFun y → ∃ c, ↑c * x = ↑c * y<VAR>toOneHom✝ : OneHom M N<VAR>map_mul'✝ : ∀ (x y : M), toOneHom✝.toFun (x * y) = toOneHom✝.toFun x * toOneHom✝.toFun y<VAR>map_units'✝ : ∀ (y : ↥S), IsUnit ((↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑y)<VAR>surj'✝ : ∀ (z : N), ∃ x, z * (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun ↑x.2 = (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x.1<VAR>exists_of_eq✝ : ∀ (x y : M), (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun x = (↑{ toOneHom := toOneHom✝, map_mul' := map_mul'✝ }).toFun y → ∃ c, ↑c * x = ↑c * y<VAR>h : ∀ (x : M), { toOneHom := toOneHom✝¹, map_mul' := map_mul'✝¹, map_units' := map_units'✝¹, surj' := surj'✝¹, exists_of_eq := exists_of_eq✝¹ }.toMap x = { toOneHom := toOneHom✝, map_mul' := map_mul'✝, map_units' := map_units'✝, surj' := surj'✝, exists_of_eq := exists_of_eq✝ }.toMap x<GOAL>toOneHom✝¹ = toOneHom✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : ClosedEmbedding g<GOAL>ClosedEmbedding (g ∘ f) ↔ ClosedEmbedding f
<VAR>x y : ℝ<GOAL>sin (x - y) = sin x * cos y - cos x * sin y
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_init : x ≤ f x<GOAL>lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h_init : x ≤ f x<VAR>a : Ordinal.{u}<VAR>h_a : a < (succ #α).ord<VAR>b : Ordinal.{u}<VAR>h_b : b < (succ #α).ord<VAR>h_nab : a ≠ b<VAR>h_fab : lfpApprox f x a = lfpApprox f x b<GOAL>lfpApprox f x (succ #α).ord ∈ fixedPoints ⇑f
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : Fintype ι✝<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>inst✝⁴ : FiniteDimensional ℝ F<VAR>inst✝³ : MeasurableSpace F<VAR>inst✝² : BorelSpace F<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : IsEmpty ι<GOAL>volume = dirac 0
<VAR>ι✝ : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : Fintype ι✝<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : InnerProductSpace ℝ F<VAR>inst✝⁴ : FiniteDimensional ℝ F<VAR>inst✝³ : MeasurableSpace F<VAR>inst✝² : BorelSpace F<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : IsEmpty ι<GOAL>dirac ((EuclideanSpace.measurableEquiv ι).symm 0) = dirac 0
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑C * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * (↑c * ∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p
<VAR>ι✝ : Type u_1<VAR>inst✝¹⁰ : Fintype ι✝<VAR>A : ι✝ → Type u_2<VAR>inst✝⁹ : (i : ι✝) → MeasurableSpace (A i)<VAR>μ✝ : (i : ι✝) → Measure (A i)<VAR>inst✝⁸ : ∀ (i : ι✝), SigmaFinite (μ✝ i)<VAR>F : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>E : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp✝ : (↑(finrank ℝ E)).IsConjExponent p<VAR>C : ℝ≥0 := lintegralPowLePowLIntegralFDerivConst μ p<VAR>ι : Type := Fin (finrank ℝ E)<VAR>hιcard : #ι = finrank ℝ E<VAR>this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)<VAR>e : E ≃L[ℝ] ι → ℝ := ContinuousLinearEquiv.ofFinrankEq this✝<VAR>this : (Measure.map (⇑e.symm) volume).IsAddHaarMeasure<VAR>hp : (↑#ι).IsConjExponent p<VAR>h0p : 0 ≤ p<VAR>c : ℝ≥0 := μ.addHaarScalarFactor (Measure.map (⇑e.symm) volume)<VAR>hc : 0 < c<VAR>h2c : μ = c • Measure.map (⇑e.symm) volume<VAR>h3c : ↑c ≠ 0<VAR>h0C : C = c * ‖↑e.symm‖₊ ^ p * (c ^ p)⁻¹<VAR>hC : C * c ^ p = c * ‖↑e.symm‖₊ ^ p<VAR>v : (ι → ℝ) → F := u ∘ ⇑e.symm<GOAL>↑c * ∫⁻ (a : E), ↑‖u a‖₊ ^ p ∂Measure.map (⇑e.symm) volume ≤ ↑C * (↑c * ∫⁻ (a : E), ↑‖fderiv ℝ u a‖₊ ∂Measure.map (⇑e.symm) volume) ^ p