awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
rw :
  HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))))
    (∑' (x : (↑(u i) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))))
⊢ HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      ((μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
        ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)

Tactic:
rw [B]
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
⊢ HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))))
    (∑' (x : (↑(u i) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))))

Tactic:
ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
⊢ HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))))
    (∑' (x : (↑(u i) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))))

Tactic:
exact ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
⊢ HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      ((μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
        ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)

Tactic:
have C : HasSum (fun x : u i => μ (o ∩ closedBall x (r x))) (μ (o ∩ v i)) := by
      rw [B]; exact ENNReal.summable.hasSum
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
C :
  HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      ((μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
        ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (o ∩ v i)

Tactic:
have : μ s / (N + 1) < μ (o ∩ v i) := hi.trans_le (measure_mono (inter_subset_inter_left _ so))
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
C :
  HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      ((μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
        ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
this :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (o ∩ v i)
⊢ ∃ (w : Finset (↑(u i) : Type u_1)),
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
      ∑ x ∈ w, (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α)))

Tactic:
((tendsto_order.1 C).1 _ this).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
C :
  HasSum (α := ℝ≥0∞)
    (fun (x : (↑(u i) : Type u_1)) ↦
      ((μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
        ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
this :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (o ∩ v i)
⊢ ∃ (w : Finset (↑(u i) : Type u_1)),
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
      ∑ x ∈ w, (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α)))

Tactic:
exact ((tendsto_order.1 C).1 _ this).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
inr :
  ∀ (w : Finset (↑(u i) : Type u_1))
    (hw :
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
        ∑ x ∈ w,
          (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α)))),
    ∃ (t : Finset α),
      (↑t : Set α) ⊆ s ∧
        (μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) ≤
            HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1)
              ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
          (↑t : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
⊢ ∃ (t : Finset α),
    (↑t : Set α) ⊆ s ∧
      (μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        (↑t : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
obtain ⟨w, hw⟩ :
    ∃ w : Finset (u i), μ s / (N + 1) <
      ∑ x ∈ w, μ (o ∩ closedBall (x : α) (r (x : α))) := by
    have C : HasSum (fun x : u i => μ (o ∩ closedBall x (r x))) (μ (o ∩ v i)) := by
      rw [B]; exact ENNReal.summable.hasSum
    have : μ s / (N + 1) < μ (o ∩ v i) := hi.trans_le (measure_mono (inter_subset_inter_left _ so))
    exact ((tendsto_order.1 C).1 _ this).exists

Premises used: Finset, Set.Elem, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
w : Finset (↑(u i) : Type u_1)
hw :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    ∑ x ∈ w, (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α)))
⊢ ∃ (t : Finset α),
    (↑t : Set α) ⊆ s ∧
      (μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        (↑t : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
⟨Finset.image (fun x : u i => x) w, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val, Finset.image
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
w : Finset (↑(u i) : Type u_1)
hw :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    ∑ x ∈ w, (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α)))
inr : (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α) ⊆ s
inr₁ :
  (μ : (a : Set α) → ℝ≥0∞)
      (s \
        ⋃ (x : α),
          ⋃ (_ :
            Membership.mem (γ := Finset α)
              (Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) x),
            closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
inr₂ :
  (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α).PairwiseDisjoint (α :=
    Set α) fun (x : α) ↦ closedBall x (r x)
⊢ ∃ (t : Finset α),
    (↑t : Set α) ⊆ s ∧
      (μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) ≤
          HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ∧
        (↑t : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
refine ⟨Finset.image (fun x : u i => x) w, ?_, ?_, ?_⟩