awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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)) : α)))
⊢ HMul.hMul (β := ℝ≥0∞) (1 / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o)
have bc : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ≤
  (μ : (a : Set α) → ℝ≥0∞) ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o)
Tactic: rw [one_div, mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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)) : α)))
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ≤
    (μ : (a : Set α) → ℝ≥0∞) ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o)
have apply : Eq (α := ℝ≥0∞)
  (∑ x ∈ w, (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o) :
    ℝ≥0∞)
Tactic: apply hw.le.trans (le_of_eq _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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)) : α)))
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ w,
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o) :
      ℝ≥0∞)
have hd : (↑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: rw [← Finset.set_biUnion_coe, inter_comm _ o, inter_iUnion₂, Finset.set_biUnion_coe,
          measure_biUnion_finset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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)) : α)))
hd :
  (↑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)) : α))
⊢ Eq (α := ℝ≥0∞)
    (∑ x ∈ w,
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o) :
      ℝ≥0∞)
have hm : ∀ b ∈ w, MeasurableSet (o ∩ closedBall (↑(↑b : (↑s : Type u_1)) : α) (r (↑(↑b : (↑s : Type u_1)) : α)))
Tactic: rw [← Finset.set_biUnion_coe, inter_comm _ o, inter_iUnion₂, Finset.set_biUnion_coe,
          measure_biUnion_finset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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 (x : (↑(u i) : Type u_1)) ↦
    o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))
have 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)) : α))
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ closedBall x (r x)) k l
have 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
Tactic: obtain ⟨k', _, rfl⟩ : ∃ k' : u i, k' ∈ w ∧ ↑k' = k := by
      simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hk
Cleared hypotheses: k, hk, hkl
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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)) : α)))
l : α
hl : l ∈ (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
k' : (↑(u i) : Type u_1)
left : 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
have inr : ∀ l' ∈ w,
  ∀
    (hl :
      (↑(↑l' : (↑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' : (↑s : Type u_1)) : α)),
    Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ closedBall x (r x)) (↑(↑k' : (↑s : Type u_1)) : α)
      (↑(↑l' : (↑s : Type u_1)) : α)
Tactic: obtain ⟨l', _, rfl⟩ : ∃ l' : u i, l' ∈ w ∧ ↑l' = l := by
      simpa only [mem_image, Finset.mem_coe, Finset.coe_image] using hl
Cleared hypotheses: l, hl, hkl
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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_1 : 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)
left : k' ∈ w
hk :
  (↑(↑k' : (↑s : Type u_1)) : α) ∈
    (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
l' : (↑(u i) : Type u_1)
left_1 : l' ∈ w
hl :
  (↑(↑l' : (↑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' : (↑s : Type u_1)) : α)
h : (↑k' : (↑s : Type u_1)) = (↑l' : (↑s : Type u_1))
⊢ False
have hkl₁ : (↑(↑l' : (↑s : Type u_1)) : α) ≠ (↑(↑l' : (↑s : Type u_1)) : α)
Tactic: rw [h] at hkl
Cleared hypotheses: hkl, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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)
left : k' ∈ w
hk :
  (↑(↑k' : (↑s : Type u_1)) : α) ∈
    (↑(Finset.image (fun (x : (↑(u i) : Type u_1)) ↦ (↑(↑x : (↑s : Type u_1)) : α)) w) : Set α)
l' : (↑(u i) : Type u_1)
left_1 : l' ∈ w
hl :
  (↑(↑l' : (↑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' : (↑s : Type u_1)) : α)
⊢ Function.onFun (β := Set α) Disjoint (fun (x : α) ↦ closedBall x (r x)) (↑(↑k' : (↑s : Type u_1)) : α)
    (↑(↑l' : (↑s : Type u_1)) : α)
have k'nel' : (↑k' : (↑s : Type u_1)) ≠ (↑l' : (↑s : Type u_1))
Tactic: have k'nel' : (k' : s) ≠ l' := by intro h; rw [h] at hkl; exact hkl rfl