ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ x<GOAL>inversion x R x ∈ perpBisector x (inversion x R y) ↔ dist x y = dist y x ∧ x ≠ x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<VAR>hx : x ≠ c<GOAL>inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c
<GOAL>¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a}.Nonempty
<GOAL>{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a} = ∅
<VAR>x✝ : ℝ<GOAL>x✝ ∈ {x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x => ↑x) → x ≤ a} ↔ x✝ ∈ ∅
<GOAL>Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
<VAR>h : HasDerivAt Gammaℝ (-(↑γ + Complex.log (4 * ↑π)) / 2) 1<GOAL>Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<GOAL>Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this : Tendsto ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2 / Gammaℝ 1))<GOAL>Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this : Tendsto ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<GOAL>Tendsto (fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this : Tendsto ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<GOAL>(fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this✝ : Tendsto ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this : {z | 0 < z.re} ∈ 𝓝 1<GOAL>(fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun s => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this✝ : Tendsto ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this : {z | 0 < z.re} ∈ 𝓝 1<GOAL>∀ᶠ (x : ℂ) in 𝓝 1, x ∈ {1}ᶜ → ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)
<VAR>h : Tendsto (fun b => (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this✝ : Tendsto ((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))<VAR>this : {z | 0 < z.re} ∈ 𝓝 1<VAR>a : ℂ<VAR>ha : 0 < a.re<VAR>a✝ : a ∈ {1}ᶜ<GOAL>((fun b => (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
<VAR>r : ℝ<VAR>n : ℕ<GOAL>↑(r ^ n) = ↑r ^ n
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<GOAL>minpoly A ((algebraMap A B) a) = X - C a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<GOAL>(Polynomial.aeval ((algebraMap A B) a)) (X - C a) = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<GOAL>∀ (q : A[X]), q.degree < (X - C a).degree → q = 0 ∨ (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<GOAL>∀ (q : A[X]), q.degree < (X - C a).degree → ¬q = 0 → (Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<VAR>q : A[X]<VAR>hl : q.degree < (X - C a).degree<VAR>h0 : ¬q = 0<GOAL>(Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<VAR>q : A[X]<VAR>hl : q.natDegree = 0<VAR>h0 : ¬q = 0<GOAL>(Polynomial.aeval ((algebraMap A B) a)) q ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>a : A<VAR>hf : Injective ⇑(algebraMap A B)<VAR>a✝ : Nontrivial A<VAR>q : A[X]<VAR>hl : q.natDegree = 0<VAR>h0 : ¬C (q.coeff 0) = 0<GOAL>(Polynomial.aeval ((algebraMap A B) a)) (C (q.coeff 0)) ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>n : ℕ<GOAL>↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>B C : Finset α<VAR>n : ℕ<VAR>hAB : ∀ A' ⊆ ∅, (∅ * B).card * A'.card ≤ (A' * B).card * ∅.card<GOAL>↑(∅ * B ^ n).card ≤ (↑(∅ * B).card / ↑∅.card) ^ n * ↑∅.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>n : ℕ<VAR>hA : A.Nonempty<GOAL>↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>hA : A.Nonempty<VAR>n : ℕ<VAR>ih : ↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card<GOAL>↑(A * B ^ (n + 1)).card ≤ (↑(A * B).card / ↑A.card) ^ (n + 1) * ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>hA : A.Nonempty<VAR>n : ℕ<VAR>ih : ↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card<GOAL>↑((A * B * B ^ n).card * A.card) ≤ ↑(A * B).card * ((↑(A * B).card / ↑A.card) ^ n * ↑A.card)
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>hA : A.Nonempty<VAR>n : ℕ<VAR>ih : ↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card<GOAL>0 < ↑A.card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>hA : A.Nonempty<VAR>n : ℕ<VAR>ih : ↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card<GOAL>↑((A * B).card * (A * B ^ n).card) ≤ ↑(A * B).card * ((↑(A * B).card / ↑A.card) ^ n * ↑A.card)
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>hA : A.Nonempty<VAR>n : ℕ<VAR>ih : ↑(A * B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card<GOAL>↑(A * B).card * ↑(A * B ^ n).card ≤ ↑(A * B).card * ((↑(A * B).card / ↑A.card) ^ n * ↑A.card)
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i j : (Quotient.out (aleph 1).ord).α<VAR>h : j < i<VAR>t : Set α<VAR>ht : t ∈ generateMeasurableRec s j<GOAL>tᶜ ∈ let i := i; let S := ⋃ j, generateMeasurableRec s ↑j; s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ∀ (x : α), ∃ y ∈ s, x ≤ y<GOAL>atTop = generate (Ici '' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ∀ (x : α), ∃ y ∈ s, x ≤ y<GOAL>generate (range Ici) = generate (Ici '' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ∀ (x : α), ∃ y ∈ s, x ≤ y<GOAL>generate (range Ici) ≤ generate (Ici '' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ∀ (x : α), ∃ y ∈ s, x ≤ y<GOAL>generate (Ici '' s) ≤ generate (range Ici)
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace 𝕜 E✝<VAR>inst✝⁷ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E✝<VAR>inst✝⁶ : HasOrthogonalProjection K<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection p<VAR>inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)<VAR>x : E<GOAL>f ↑((orthogonalProjection p) x) = ↑((orthogonalProjection (Submodule.map f.toLinearMap p)) (f x))
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace 𝕜 E✝<VAR>inst✝⁷ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E✝<VAR>inst✝⁶ : HasOrthogonalProjection K<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection p<VAR>inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)<VAR>x : E<GOAL>f ↑((orthogonalProjection p) x) ∈ Submodule.map f.toLinearMap p
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace 𝕜 E✝<VAR>inst✝⁷ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E✝<VAR>inst✝⁶ : HasOrthogonalProjection K<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection p<VAR>inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)<VAR>x : E<VAR>y : E'<VAR>hy : y ∈ Submodule.map f.toLinearMap p<GOAL>⟪f x - f ↑((orthogonalProjection p) x), y⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : _root_.RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E✝<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace 𝕜 E✝<VAR>inst✝⁷ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E✝<VAR>inst✝⁶ : HasOrthogonalProjection K<VAR>E : Type u_4<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>f : E →ₗᵢ[𝕜] E'<VAR>p : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection p<VAR>inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)<VAR>x x' : E<VAR>hx' : x' ∈ ↑p<GOAL>⟪f x - f ↑((orthogonalProjection p) x), f x'⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>∫⁻ (x : α) in s, ↑‖g x‖₊ ∂μ ≤ ∫⁻ (x : α) in s, ↑‖f x‖₊ ∂μ
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<GOAL>0 ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<GOAL>4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<VAR>hm : 0 ≤ 1 - (↑m)⁻¹<GOAL>4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<VAR>hm : 0 ≤ 1 - (↑m)⁻¹<VAR>hε : 0 ≤ 1 - ε / 10<GOAL>4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUV : U ≠ V<VAR>hunif : ¬G.IsUniform ε U V<VAR>hm : 0 ≤ 1 - (↑m)⁻¹<VAR>hε : 0 ≤ 1 - ε / 10<VAR>hε₀ : 0 < ε<GOAL>4 / 5 * ε ≤ ↑(star hP G ε hU V).card / 4 ^ P.parts.card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addRightEmbedding c) (Icc a b) = Icc (a + c) (b + c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addRightEmbedding c) '' Set.Icc a b = Set.Icc (a + c) (b + c)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x : LocalizedModule S M<VAR>m : M<VAR>s : ↥S<GOAL>0 + mk m s = mk m s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>g : X → Y<VAR>h : f =ᶠ[𝓝 x] g<GOAL>ContinuousAt f x ↔ ContinuousAt g x
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>3 / 4 * ε ≤ |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card) - (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<GOAL>3 / 4 * ε ≤ |(∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card) - (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / (4 ^ P.parts.card * 4 ^ P.parts.card)|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>p : ℝ := (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card)<VAR>q : ℝ := (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / (4 ^ P.parts.card * 4 ^ P.parts.card)<VAR>r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))<VAR>s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))<VAR>t : ℝ := ↑(G.edgeDensity U V)<GOAL>3 / 4 * ε ≤ |p - q|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>p : ℝ := (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card)<VAR>q : ℝ := (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / (4 ^ P.parts.card * 4 ^ P.parts.card)<VAR>r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))<VAR>s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))<VAR>t : ℝ := ↑(G.edgeDensity U V)<VAR>hrs : |r - s| ≤ ε / 5<GOAL>3 / 4 * ε ≤ |p - q|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>p : ℝ := (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card)<VAR>q : ℝ := (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / (4 ^ P.parts.card * 4 ^ P.parts.card)<VAR>r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))<VAR>s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))<VAR>t : ℝ := ↑(G.edgeDensity U V)<VAR>hrs : |r - s| ≤ ε / 5<VAR>hst : ε ≤ |s - t|<GOAL>3 / 4 * ε ≤ |p - q|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>p : ℝ := (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card)<VAR>q : ℝ := (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / (4 ^ P.parts.card * 4 ^ P.parts.card)<VAR>r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))<VAR>s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))<VAR>t : ℝ := ↑(G.edgeDensity U V)<VAR>hrs : |r - s| ≤ ε / 5<VAR>hst : ε ≤ |s - t|<VAR>hpr : |p - r| ≤ ε ^ 5 / 49<GOAL>3 / 4 * ε ≤ |p - q|
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hUVne : U ≠ V<VAR>hUV : ¬G.IsUniform ε U V<VAR>p : ℝ := (∑ ab ∈ (star hP G ε hU V).product (star hP G ε hV U), ↑(G.edgeDensity ab.1 ab.2)) / (↑(star hP G ε hU V).card * ↑(star hP G ε hV U).card)<VAR>q : ℝ := (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / (4 ^ P.parts.card * 4 ^ P.parts.card)<VAR>r : ℝ := ↑(G.edgeDensity ((star hP G ε hU V).biUnion id) ((star hP G ε hV U).biUnion id))<VAR>s : ℝ := ↑(G.edgeDensity (G.nonuniformWitness ε U V) (G.nonuniformWitness ε V U))<VAR>t : ℝ := ↑(G.edgeDensity U V)<VAR>hrs : |r - s| ≤ ε / 5<VAR>hst : ε ≤ |s - t|<VAR>hpr : |p - r| ≤ ε ^ 5 / 49<VAR>hqt : |q - t| ≤ ε ^ 5 / 49<GOAL>3 / 4 * ε ≤ |p - q|