ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u<VAR>inst✝² : DecidableEq α✝<VAR>β : Type v<VAR>inst✝¹ : Fintype α✝<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>σ : α → Perm β<VAR>a : α<VAR>b : β<VAR>a' : α<VAR>l : List α<VAR>ih : l.Nodup → a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨ a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)<VAR>hl : (a' :: l).Nodup<VAR>not_mem_l : a ∉ l<VAR>prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)<GOAL>a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨ a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<GOAL>LinearMap.range (toLin' (diagonal w)) = ⨆ i ∈ {i | w i ≠ 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<GOAL>LinearMap.range (toLin' (diagonal w)) = ⨆ i, ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<GOAL>⨆ i, Submodule.map (toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i)) = ⨆ i, ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<GOAL>(fun i => Submodule.map (toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i))) = fun i => ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<VAR>i : m<GOAL>Submodule.map (toLin' (diagonal w)) (LinearMap.range (LinearMap.stdBasis K (fun a => K) i)) = ⨆ (_ : w i ≠ 0), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hq : q.Monic<VAR>this : DecidableEq R := Classical.decEq R<VAR>hp : ¬p = 0<GOAL>p.leadingCoeff * q.leadingCoeff ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<GOAL>UnifTight (f - g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<VAR>hg : UnifTight g p μ<VAR>hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ<GOAL>UnifTight (f + -g) p μ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x y : A<VAR>x✝¹ : Homogeneous 𝒜 x<VAR>x✝ : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ asIdeal f_deg hm q<VAR>nx : ℕ<VAR>hnx : x ∈ 𝒜 nx<VAR>ny : ℕ<VAR>hny : y ∈ 𝒜 ny<GOAL>(∀ (i : ℕ), HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) x ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal) ∨ ∀ (i : ℕ), HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) y ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x y : A<VAR>x✝¹ : Homogeneous 𝒜 x<VAR>x✝ : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ asIdeal f_deg hm q<VAR>nx : ℕ<VAR>hnx : x ∈ 𝒜 nx<VAR>ny : ℕ<VAR>hny : y ∈ 𝒜 ny<GOAL>HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal ∨ HomogeneousLocalization.mk { deg := m * ny, num := ⟨(proj 𝒜 ny) y ^ m, ⋯⟩, den := ⟨f ^ ny, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x y : A<VAR>x✝¹ : Homogeneous 𝒜 x<VAR>x✝ : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ asIdeal f_deg hm q<VAR>nx : ℕ<VAR>hnx : x ∈ 𝒜 nx<VAR>ny : ℕ<VAR>hny : y ∈ 𝒜 ny<GOAL>∀ (b : ℕ), b ≠ ny → HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) y ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x y : A<VAR>x✝¹ : Homogeneous 𝒜 x<VAR>x✝ : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ asIdeal f_deg hm q<VAR>nx : ℕ<VAR>hnx : x ∈ 𝒜 nx<VAR>ny : ℕ<VAR>hny : y ∈ 𝒜 ny<GOAL>∀ (b : ℕ), b ≠ nx → HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) x ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Nontrivial M<VAR>h : ⊤ = Ideal.ofList [] • ⊤<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Nontrivial M<VAR>h : Subsingleton (Submodule R M)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p✝ q p : R[X]<VAR>hq : q ≠ 0<GOAL>p.degree ≤ (p * q).degree
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>φ : G ≃g G'<VAR>v : V<VAR>v' : V'<VAR>C : G.ConnectedComponent<GOAL>G.connectedComponentMk (φ.symm v') = C ↔ G'.connectedComponentMk v' = map (RelIso.toRelEmbedding φ).toRelHom C
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>φ : G ≃g G'<VAR>v : V<VAR>v' : V'<VAR>C : G.ConnectedComponent<VAR>u : V<GOAL>G.connectedComponentMk (φ.symm v') = G.connectedComponentMk u ↔ G'.connectedComponentMk v' = map (RelIso.toRelEmbedding φ).toRelHom (G.connectedComponentMk u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s ∩ r.dom<GOAL>x ∈ r.preimage (r.image s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s ∧ x ∈ {x | ∃ y, r x y}<GOAL>x ∈ r.preimage (r.image s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : β<VAR>rxy : r x y<GOAL>x ∈ r.preimage (r.image s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : β<VAR>rxy : r x y<GOAL>y ∈ r.image s ∧ r.inv y x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : β<VAR>rxy : r x y<GOAL>(∃ x ∈ s, r x y) ∧ r.inv y x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<GOAL>Odd (m + n) ↔ (Odd n ↔ Even m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hf : (s ∩ mulSupport f).Finite<VAR>hg : (s ∩ mulSupport g).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>hf : (mulSupport (s.mulIndicator f)).Finite<VAR>hg : (mulSupport (s.mulIndicator g)).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : l₂.length ≤ l₁.length<GOAL>(l₁.zip l₂).unzip.2 = l₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : l₂.length ≤ l₁.length<GOAL>(l₂.zip l₁).unzip.swap.2 = l₂
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 0<VAR>hb : b % 2 = 1<VAR>hc : a / 4 = c<VAR>hr : jacobiSymNat c b = r<GOAL>jacobiSymNat a b = r
<VAR>a b c : ℕ<VAR>r : ℤ<VAR>ha : a % 4 = 0<VAR>hb : b % 2 = 1<VAR>hc : a / 4 = c<VAR>hr : jacobiSymNat c b = r<GOAL>jacobiSym (↑a) b = jacobiSym (↑a / 4) b
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<VAR>p q : R⟦X⟧<VAR>h : (rescale a) p = (rescale a) q<GOAL>p = q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<VAR>p q : R⟦X⟧<VAR>h : ∀ (n : ℕ), (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)<GOAL>∀ (n : ℕ), (coeff R n) p = (coeff R n) q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<VAR>p q : R⟦X⟧<VAR>n : ℕ<VAR>h : (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)<GOAL>(coeff R n) p = (coeff R n) q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<VAR>p q : R⟦X⟧<VAR>n : ℕ<VAR>h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0<GOAL>(coeff R n) p = (coeff R n) q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<VAR>p q : R⟦X⟧<VAR>n : ℕ<VAR>h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0<GOAL>¬a ^ n = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<VAR>p q : R⟦X⟧<VAR>n : ℕ<VAR>h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0<VAR>h' : a ^ n = 0<GOAL>False
<VAR>α✝ : Type u_1<VAR>inst✝⁵ : DistribLattice α✝<VAR>inst✝⁴ : OrderBot α✝<VAR>inst✝³ : Fintype α✝<VAR>inst✝² : DecidablePred SupIrred<VAR>α : Type u<VAR>inst✝¹ : Finite α<VAR>inst✝ : DistribLattice α<GOAL>∃ β x x_1 f, Injective ⇑f
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>inst✝ : (j : Fin (n + 1)) → One (α j)<VAR>i : Fin (n + 1)<VAR>x : α i<GOAL>x = Pi.mulSingle i x i ∧ 1 = fun i_1 => Pi.mulSingle i x (i.succAbove i_1)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : μ s ≤ 0<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : IsEmpty α<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<VAR>A : s = ⋃ i, s ∩ v i<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<VAR>A : s = ⋃ i, s ∩ v i<VAR>S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<VAR>A : s = ⋃ i, s ∩ v i<VAR>S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)<VAR>i : Fin N<VAR>hi : μ s / ↑N ≤ μ (s ∩ v i)<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<VAR>A : s = ⋃ i, s ∩ v i<VAR>S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)<VAR>i : Fin N<VAR>hi : μ s / (↑N + 1) < μ (s ∩ v i)<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>β : Type u<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>N : ℕ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>hN : IsEmpty (SatelliteConfig α N τ)<VAR>s : Set α<VAR>r : α → ℝ<VAR>rpos : ∀ x ∈ s, 0 < r x<VAR>rle : ∀ x ∈ s, r x ≤ 1<VAR>hμs : 0 < μ s<VAR>h✝ : Nonempty α<VAR>Npos : N ≠ 0<VAR>o : Set α<VAR>so : s ⊆ o<VAR>omeas : MeasurableSet o<VAR>μo : μ o = μ s<VAR>a : BallPackage (↑s) α := { c := fun x => ↑x, r := fun x => r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }<VAR>u : Fin N → Set ↑s<VAR>hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j => closedBall (a.c j) (a.r j)<VAR>hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)<VAR>u_count : ∀ (i : Fin N), (u i).Countable<VAR>v : Fin N → Set α := fun i => ⋃ x ∈ u i, closedBall (↑x) (r ↑x)<VAR>A : s = ⋃ i, s ∩ v i<VAR>S : ∑ _i : Fin N, μ s / ↑N ≤ ∑ i : Fin N, μ (s ∩ v i)<VAR>i : Fin N<VAR>hi : μ s / (↑N + 1) < μ (s ∩ v i)<VAR>B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))<GOAL>∃ t, ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun x => closedBall x (r x)