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∞)
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)) : α)))
k : (↑(u i) : Type u_1)
h_1 : k ∈ (↑w : Set (↑(u i) : Type u_1))
l : (↑(u i) : Type u_1)
_ :
  l ∈ (↑w : Set (↑(u i) : Type u_1)) →
    k ≠ l →
      Function.onFun (β := Set α) Disjoint
        (fun (b : (↑(u i) : Type u_1)) ↦ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))) k l
⊢ l ∈ (↑w : Set (↑(u i) : Type u_1)) →
    k ≠ l →
      Function.onFun (β := Set α) Disjoint
        (fun (b : (↑(u i) : Type u_1)) ↦ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))) k l

Tactic:
_
-- 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)) : α)))
k : (↑(u i) : Type u_1)
h_1 : k ∈ (↑w : Set (↑(u i) : Type u_1))
l : (↑(u i) : Type u_1)
h_2 : l ∈ (↑w : Set (↑(u i) : Type u_1))
hkl : k ≠ l
⊢ Function.onFun (β := Set α) Disjoint
    (fun (b : (↑(u i) : Type u_1)) ↦ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))) k l

Tactic:
hu i k.2 l.2 (Subtype.val_injective.ne hkl)

Premises used: Subtype.val_injective, Function.Injective.ne, Subtype.property
-- 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)) : α)))
k : (↑(u i) : Type u_1)
h_1 : k ∈ (↑w : Set (↑(u i) : Type u_1))
l : (↑(u i) : Type u_1)
h_2 : l ∈ (↑w : Set (↑(u i) : Type u_1))
hkl : k ≠ l
⊢ Function.onFun (β := Set α) Disjoint
    (fun (b : (↑(u i) : Type u_1)) ↦ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))) k l

Tactic:
exact hu i k.2 l.2 (Subtype.val_injective.ne hkl)

Premises used: Subtype.val_injective, Function.Injective.ne, Subtype.property
-- 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)) : α)))
⊢ (↑w : Set (↑(u i) : Type u_1)).PairwiseDisjoint (α := Set α) fun (b : (↑(u i) : Type u_1)) ↦
    closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))

Tactic:
have : (w : Set (u i)).PairwiseDisjoint
              fun b : u i => closedBall (b : α) (r (b : α)) := by
            intro k _ l _ hkl; exact hu i k.2 l.2 (Subtype.val_injective.ne hkl)
-- 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)) : α)))
this :
  (↑w : Set (↑(u i) : Type u_1)).PairwiseDisjoint (α := Set α) fun (b : (↑(u i) : Type u_1)) ↦
    closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))
⊢ (↑w : Set (↑(u i) : Type u_1)).PairwiseDisjoint (α := Set α) fun (x : (↑(u i) : Type u_1)) ↦
    o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))

Tactic:
this.mono fun k => inter_subset_right

Premises used: Set.PairwiseDisjoint.mono, Set.inter_subset_right
-- 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)) : α)))
this :
  (↑w : Set (↑(u i) : Type u_1)).PairwiseDisjoint (α := Set α) fun (b : (↑(u i) : Type u_1)) ↦
    closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α))
⊢ (↑w : Set (↑(u i) : Type u_1)).PairwiseDisjoint (α := Set α) fun (x : (↑(u i) : Type u_1)) ↦
    o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))

Tactic:
exact this.mono fun k => inter_subset_right

Premises used: Set.PairwiseDisjoint.mono, Set.inter_subset_right
-- 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)) : α)))
b : (↑(u i) : Type u_1)
hm : b ∈ w → MeasurableSet (o ∩ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α)))
⊢ b ∈ w → MeasurableSet (o ∩ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α)))

Tactic:
_
-- 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)) : α)))
b : (↑(u i) : Type u_1)
h_1 : b ∈ w
⊢ MeasurableSet (o ∩ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α)))

Tactic:
apply omeas.inter measurableSet_closedBall

Premises used: measurableSet_closedBall, MeasurableSet.inter
-- 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)) : α)))
k : α
hk : k ∈ (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
l : α
hl : l ∈ (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
hkl : k ≠ l
⊢ ∃ k' ∈ w, (↑(↑k' : (↑s : Type u_1)) : α) = k

Tactic:
simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hk

Premises used: Set.mem_image, Finset.coe_image, Finset.mem_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)) : α)))
k : α
hk : k ∈ (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
l : α
hl : l ∈ (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
hkl : k ≠ l
inr :
  ∀ k' ∈ w,
    ∀
      (hk :
        (↑(↑k' : (↑s : Type u_1)) : α) ∈
          (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α))
      (hkl : (↑(↑k' : (↑s : Type u_1)) : α) ≠ l),
      Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ closedBall x (r x)) (↑(↑k' : (↑s : Type u_1)) : α) l
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ closedBall x (r x)) k l

Tactic:
obtain ⟨k', _, rfl⟩ : ∃ k' : u i, k' ∈ w ∧ ↑k' = k := by
      simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hk

Premises used: rfl