ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hv : ¬v = 0<VAR>hc : ¬c = 0<VAR>e : ℝ ≃ᵐ ℝ := (Homeomorph.mulLeft₀ c hc).symm.toMeasurableEquiv<VAR>he' : ∀ (x : ℝ), HasDerivAt (⇑e) ((fun x => c⁻¹) x) x<VAR>s' : Set ℝ<VAR>hs' : MeasurableSet s'<VAR>x : ℝ<GOAL>|c| ≠ 0
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ i : ι, ‖x i‖ ^ (ENNReal.ofReal p).toReal) ^ (1 / (ENNReal.ofReal p).toReal)<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℂ), ‖x‖ = 0 ↔ x = 0<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℂ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℂ), ‖-x‖ = ‖x‖<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>nm_zero : ‖0‖ = 0<VAR>eq_zero : ∀ (x : ι → ℂ), ‖x‖ = 0 ↔ x = 0<VAR>nm_neg : ∀ (x : ι → ℂ), ‖-x‖ = ‖x‖<VAR>nm_add : ∀ (x y : ι → ℂ), ‖x + y‖ ≤ ‖x‖ + ‖y‖<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), ‖r • x‖ ≤ ‖r‖ * ‖x‖<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : 0 < p<VAR>eq_norm : ∀ (x : ι → ℂ), ‖x‖ = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>this : Fact (1 ≤ ENNReal.ofReal p)<VAR>eq_zero : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) = 0 ↔ x = 0<VAR>nm_zero : (∑ x : ι, ‖0 x‖ ^ p) ^ (1 / p) = 0<VAR>nm_neg : ∀ (x : ι → ℂ), (∑ x_1 : ι, ‖(-x) x_1‖ ^ p) ^ (1 / p) = (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p)<VAR>nm_add : ∀ (x y : ι → ℂ), (∑ x_1 : ι, ‖(x + y) x_1‖ ^ p) ^ (1 / p) ≤ (∑ x_1 : ι, ‖x x_1‖ ^ p) ^ (1 / p) + (∑ x : ι, ‖y x‖ ^ p) ^ (1 / p)<VAR>nm_smul : ∀ (r : ℝ) (x : ι → ℂ), (∑ x_1 : ι, abs ((r • x) x_1) ^ p) ^ (1 / p) ≤ ‖r‖ * (∑ x_1 : ι, abs (x x_1) ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) ≤ r} = ENNReal.ofReal r ^ (2 * card ι) * ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>this : pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)<GOAL>xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>this : { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } = ↑(2 * a) * { re := ↑(xn a1 (n + 1)), im := ↑(yn a1 (n + 1)) }<GOAL>xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<VAR>this : { re := ↑(xn a1 (n + 2)), im := ↑(yn a1 (n + 2)) } + { re := ↑(xn a1 n), im := ↑(yn a1 n) } = { re := ↑(2 * a) * ↑(xn a1 (n + 1)), im := ↑(2 * a) * ↑(yn a1 (n + 1)) }<GOAL>xn a1 (n + 2) + xn a1 n = 2 * a * xn a1 (n + 1) ∧ yn a1 (n + 2) + yn a1 n = 2 * a * yn a1 (n + 1)
<VAR>a b c d m✝ n✝¹ k✝ : ℕ<VAR>p q P✝ Q : ℕ → Prop<VAR>inst✝¹ : DecidablePred P✝<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>m n k : ℕ<VAR>hmk : m.le k<VAR>ih : findGreatest P m ≤ findGreatest P k<GOAL>findGreatest P m ≤ findGreatest P k.succ
<VAR>a b c d m✝ n✝¹ k✝ : ℕ<VAR>p q P✝ Q : ℕ → Prop<VAR>inst✝¹ : DecidablePred P✝<VAR>n✝ : ℕ<VAR>P : ℕ → Prop<VAR>inst✝ : DecidablePred P<VAR>m n k : ℕ<VAR>hmk : m.le k<VAR>ih : findGreatest P m ≤ findGreatest P k<GOAL>findGreatest P m ≤ if P (k + 1) then k + 1 else findGreatest P k
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K : Multifork I<VAR>b : I.R<GOAL>K.π.app (WalkingMulticospan.right b) = K.ι (I.sndTo b) ≫ I.snd b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MulticospanIndex C<VAR>K : Multifork I<VAR>b : I.R<GOAL>K.π.app (WalkingMulticospan.left (I.sndTo b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.snd b) = K.ι (I.sndTo b) ≫ I.snd b
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>f : G → ℝ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hf : support f ⊆ ball 0 R<VAR>hnf : ∀ (x : G), 0 ≤ f x<VAR>hintf : ∫ (x : G), f x ∂μ = 1<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<GOAL>dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>f : G → ℝ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hf : support f ⊆ ball 0 R<VAR>hnf : ∀ (x : G), 0 ≤ f x<VAR>hintf : ∫ (x : G), f x ∂μ = 1<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hif : Integrable f μ<GOAL>dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>f : G → ℝ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hf : support f ⊆ ball 0 R<VAR>hnf : ∀ (x : G), 0 ≤ f x<VAR>hintf : ∫ (x : G), f x ∂μ = 1<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hif : Integrable f μ<GOAL>z₀ = ∫ (t : G), ((lsmul ℝ ℝ) (f t)) z₀ ∂μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : SecondCountableTopology G<VAR>inst✝⁴ : μ.IsAddLeftInvariant<VAR>inst✝³ : SFinite μ<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : CompleteSpace E'<VAR>f : G → ℝ<VAR>x₀ : G<VAR>R ε : ℝ<VAR>z₀ : E'<VAR>hε : 0 ≤ ε<VAR>hf : support f ⊆ ball 0 R<VAR>hnf : ∀ (x : G), 0 ≤ f x<VAR>hintf : ∫ (x : G), f x ∂μ = 1<VAR>hmg : AEStronglyMeasurable g μ<VAR>hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε<VAR>hif : Integrable f μ<GOAL>(‖lsmul ℝ ℝ‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε ≤ ε
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y : P<VAR>hne : y ≠ x<VAR>h : Wbtw R x y x<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y : P<VAR>hne : y ≠ x<VAR>h : y = x<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Injective ⇑f<VAR>p : R[X]<VAR>hp : (map f p).Monic<GOAL>f p.leadingCoeff = f 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>f : α → β<VAR>inst✝ : WellFoundedLT β<VAR>hf : StrictMono f<VAR>s : Set α<VAR>hne : s.Nonempty<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>f : α → β<VAR>inst✝ : WellFoundedLT β<VAR>hf : StrictMono f<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hs' : (f '' s).Nonempty<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>f : α → β<VAR>inst✝ : WellFoundedLT β<VAR>hf : StrictMono f<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hs' : (f '' s).Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>hex : f x = ⋯.min (f '' s) hs'<GOAL>∃ m ∈ s, ∀ x ∈ s, ¬x < m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>f : α → β<VAR>inst✝ : WellFoundedLT β<VAR>hf : StrictMono f<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hs' : (f '' s).Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>hex : f x = ⋯.min (f '' s) hs'<VAR>y : α<VAR>hy : y ∈ s<VAR>hlt : y < x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>f : α → β<VAR>inst✝ : WellFoundedLT β<VAR>hf : StrictMono f<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hs' : (f '' s).Nonempty<VAR>x : α<VAR>hx : x ∈ s<VAR>hex : f x = ⋯.min (f '' s) hs'<VAR>y : α<VAR>hy : y ∈ s<VAR>hlt : y < x<GOAL>f y < ⋯.min (f '' s) hs'
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β<VAR>a : α<VAR>s : Stream' α<VAR>x✝ : a ∈ s<VAR>n : ℕ<VAR>h : (fun b => a = b) (s.get n)<GOAL>(fun b => f a = b) ((map f s).get n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>n : ℤ<GOAL>a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosMono α<VAR>hb : 0 ≤ b<VAR>h : a ≤ 1<GOAL>a * b ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : CommSemiring β<VAR>inst✝ : ContinuousMul β<VAR>hf : SuperpolynomialDecay l k f<VAR>c : β<VAR>z : ℕ<GOAL>Tendsto (fun a => k a ^ z * (fun n => f n * c) a) l (𝓝 0)
<VAR>α : Sort u_1<VAR>σ : α → Sort u_2<VAR>P Q R : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b c : α<VAR>A : P → α<VAR>B : ¬P → α<GOAL>((∃ h, a = c) ∨ ∃ h, b = c) ↔ P ∧ a = c ∨ ¬P ∧ b = c
<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>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>s : Finset ι<VAR>hp : ↑s.card * p ≤ 1<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : ι) → A i<GOAL>∫⁻ (t : A i), f (update x i t) ^ (1 - ↑s.card * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p ∂μ i ≤ ((∫⋯∫⁻_{i}, f ∂μ) ^ (1 - (↑s.card - 1) * p) * ∏ i_1 ∈ s, (∫⋯∫⁻_{i_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) ^ p) x
<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>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>s : Finset ι<VAR>hp : ↑s.card * p ≤ 1<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : ι) → A i<GOAL>∫⁻ (t : A i), f (update x i t) ^ (1 - ↑s.card * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p ∂μ i ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑s.card - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) 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>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>s : Finset ι<VAR>hp : ↑s.card * p ≤ 1<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : ι) → A i<VAR>X : A i → (a : ι) → A a := update x i<GOAL>∫⁻ (t : A i), f (X t) ^ (1 - ↑s.card * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑s.card - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) 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>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>s : Finset ι<VAR>hp : ↑s.card * p ≤ 1<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : ι) → A i<VAR>X : A i → (a : ι) → A a := update x i<VAR>hF₁ : ∀ {j : ι}, Measurable fun t => (∫⋯∫⁻_{j}, f ∂μ) (X t)<GOAL>∫⁻ (t : A i), f (X t) ^ (1 - ↑s.card * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑s.card - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) 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>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>s : Finset ι<VAR>hp : ↑s.card * p ≤ 1<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>x : (i : ι) → A i<VAR>X : A i → (a : ι) → A a := update x i<VAR>hF₁ : ∀ {j : ι}, Measurable fun t => (∫⋯∫⁻_{j}, f ∂μ) (X t)<VAR>hF₀ : Measurable fun t => f (X t)<GOAL>∫⁻ (t : A i), f (X t) ^ (1 - ↑s.card * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (X t) ^ p ∂μ i ≤ (∫⋯∫⁻_{i}, f ∂μ) x ^ (1 - (↑s.card - 1) * p) * ∏ x_1 ∈ s, (∫⋯∫⁻_{x_1}, ∫⋯∫⁻_{i}, f ∂μ ∂μ) x ^ p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>hp' : ⨆ i ∈ s, p i = ⊤<GOAL>IsSemisimpleModule R M
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>hp' : ⨆ i ∈ s, p i = ⊤<VAR>i : ι<VAR>hi : i ∈ s<GOAL>ComplementedLattice ↑(Set.Iic (p i))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>Xs : Set (Set α)<VAR>hne : Xs.Nonempty<VAR>h : ∀ X ∈ Xs, M.Basis I X<GOAL>M.Basis I (⋃₀ Xs)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>Xs : Set (Set α)<VAR>hne : Xs.Nonempty<VAR>h : ∀ X ∈ Xs, M.Basis I X<GOAL>M.Basis I (⋃ i, ↑i)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>Xs : Set (Set α)<VAR>hne : Xs.Nonempty<VAR>h : ∀ X ∈ Xs, M.Basis I X<VAR>this : Nonempty ↑Xs<GOAL>M.Basis I (⋃ i, ↑i)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : HasColimitsOfShape J C<VAR>F : J ⥤ K ⥤ C<VAR>i j : K<VAR>f : i ⟶ j<GOAL>(colimit F).map f ≫ (colimitObjIsoColimitCompEvaluation F j).hom = (colimitObjIsoColimitCompEvaluation F i).hom ≫ colimMap (whiskerLeft F ((evaluation K C).map f))
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q : Karoubi C<VAR>f : P.Hom Q<GOAL>P.p ≫ f.f = f.f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x y z : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>openSegment 𝕜 x y ⊆ s ↔ [x-[𝕜]y] ⊆ s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x : P<VAR>h : s ⊆ t<GOAL>intrinsicClosure 𝕜 s ⊆ intrinsicClosure 𝕜 t
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x✝ : P<VAR>h : s ⊆ t<VAR>x : ↥(affineSpan 𝕜 s)<VAR>hx : x ∈ closure (Subtype.val ⁻¹' s)<GOAL>x ∈ Subtype.val ⁻¹' intrinsicClosure 𝕜 t
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x✝ : P<VAR>h : s ⊆ t<VAR>x : ↥(affineSpan 𝕜 s)<VAR>hx : x ∈ closure (Subtype.val ⁻¹' s)<GOAL>Set.inclusion ⋯ x ∈ closure (Subtype.val ⁻¹' t)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x✝ : P<VAR>h : s ⊆ t<VAR>x : ↥(affineSpan 𝕜 s)<VAR>hx : x ∈ closure (Subtype.val ⁻¹' s)<GOAL>Subtype.val ⁻¹' s ⊆ Set.inclusion ⋯ ⁻¹' (Subtype.val ⁻¹' t)
<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : EvenHom Q A<VAR>x : CliffordAlgebra Q<VAR>x_property : x ∈ even Q<VAR>val✝ : CliffordAlgebra Q<VAR>property✝ : val✝ ∈ even Q<GOAL>(aux f) (⟨x, x_property⟩ * ⟨val✝, property✝⟩) = (aux f) ⟨x, x_property⟩ * (aux f) ⟨val✝, property✝⟩