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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
inst_6 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : (μ : (a : Set α) → ℝ≥0∞) u ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
R : (x : α) → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t0, closedBall x (r0 x)) : ℝ≥0∞) (0 : ℝ≥0∞)
t0_disj : t0.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : (μ : (a : Set α) → ℝ≥0∞) v ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) (ε / 2 / (↑N : ℝ≥0∞))
r1 : (x : α) → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s' : Type u_1) α :=
  { c := fun (x : (↑s' : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s' : Type u_1)) ↦ r1 (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
S : Fin N → Set (↑s' : Type u_1)
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint (α := Set α) fun (j : (↑s' : Type u_1)) ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : (x : α) → ℝ := fun (x : α) ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
B :
  ∀ (i : Fin N),
    ∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
      ε / 2 / (↑N : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2) + ε / 2 =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have rw : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2 + ε / 2) =
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: rw [add_assoc, ENNReal.add_halves]
-- 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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
inst_6 : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : (μ : (a : Set α) → ℝ≥0∞) u ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
R : (x : α) → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t0, closedBall x (r0 x)) : ℝ≥0∞) (0 : ℝ≥0∞)
t0_disj : t0.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : (μ : (a : Set α) → ℝ≥0∞) v ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) (ε / 2 / (↑N : ℝ≥0∞))
r1 : (x : α) → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s' : Type u_1) α :=
  { c := fun (x : (↑s' : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s' : Type u_1)) ↦ r1 (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
S : Fin N → Set (↑s' : Type u_1)
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint (α := Set α) fun (j : (↑s' : Type u_1)) ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : (x : α) → ℝ := fun (x : α) ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
B :
  ∀ (i : Fin N),
    ∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
      ε / 2 / (↑N : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2 + ε / 2) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2) + ε / 2 =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε =
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: rw [add_assoc, ENNReal.add_halves]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
⊢ (g x ∩ Ioo 0 δ).Nonempty
have obtain : ∀ (t : Set α) (tf : t ∈ f x) (ht : t ⊆ closedBall x (δ / 2)), (g x ∩ Ioo 0 δ).Nonempty
Tactic: obtain ⟨t, tf, ht⟩ : ∃ (t : Set α), t ∈ f x ∧ t ⊆ closedBall x (δ / 2) :=
        ffine x xs (δ / 2) (half_pos δpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
t : Set α
tf : t ∈ f x
ht : t ⊆ closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty
have obtain : ∀ (r : ℝ) (rpos : 0 < r) (tf : closedBall x r ∈ f x) (ht : closedBall x r ⊆ closedBall x (δ / 2)),
  (g x ∩ Ioo 0 δ).Nonempty
Tactic: obtain ⟨r, rpos, rfl⟩ : ∃ r : ℝ, 0 < r ∧ closedBall x r = t := by simpa using fsubset x xs tf
Cleared hypotheses: t, tf, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty
have inl : ∀ (H : r ≤ δ / 2), (g x ∩ Ioo 0 δ).Nonempty
Tactic: rcases le_total r (δ / 2) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
inl : ∀ (H : r ≤ δ / 2), (g x ∩ Ioo 0 δ).Nonempty
⊢ (g x ∩ Ioo 0 δ).Nonempty
have inr : ∀ (H : δ / 2 ≤ r), (g x ∩ Ioo 0 δ).Nonempty
Tactic: rcases le_total r (δ / 2) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
⊢ (g x ∩ Ioo 0 δ).Nonempty
have this : closedBall x r = closedBall x (δ / 2)
Tactic: have : closedBall x r = closedBall x (δ / 2) := Subset.antisymm ht (by gcongr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
x : α
xs : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
rpos : 0 < r
tf : closedBall x r ∈ f x
ht : closedBall x r ⊆ closedBall x (δ / 2)
H : δ / 2 ≤ r
this : closedBall x r = closedBall x (δ / 2)
⊢ (g x ∩ Ioo 0 δ).Nonempty
have tf₁ : closedBall x (δ / 2) ∈ f x
Tactic: rw [this] at tf
Cleared hypotheses: tf, ht, H, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
Tactic: have A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty := by
      intro x xs δ δpos
      obtain ⟨t, tf, ht⟩ : ∃ (t : Set α), t ∈ f x ∧ t ⊆ closedBall x (δ / 2) :=
        ffine x xs (δ / 2) (half_pos δpos)
      obtain ⟨r, rpos, rfl⟩ : ∃ r : ℝ, 0 < r ∧ closedBall x r = t := by simpa using fsubset x xs tf
      rcases le_total r (δ / 2) with (H | H)
      · exact ⟨r, ⟨rpos, tf⟩, ⟨rpos, H.trans_lt (half_lt_self δpos)⟩⟩
      · have : closedBall x r = closedBall x (δ / 2) := Subset.antisymm ht (by gcongr)
        rw [this] at tf
        exact ⟨δ / 2, ⟨half_pos δpos, tf⟩, ⟨half_pos δpos, half_lt_self δpos⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (t : Set α) (r : α → ℝ),
  t.Countable →
    ∀ (ts : t ⊆ s) (tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1)
      (μt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞))
      (tdisj : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)),
      ∃ (t : Set (α × Set α)),
        (∀ p ∈ t, p.1 ∈ s) ∧
          (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
            (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨t, r, _, ts, tg, μt, tdisj⟩ :
      ∃ (t : Set α) (r : α → ℝ),
        t.Countable ∧
          t ⊆ s ∧
            (∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1) ∧
              μ (s \ ⋃ x ∈ t, closedBall x (r x)) = 0 ∧
                t.PairwiseDisjoint fun x => closedBall x (r x) :=
      exists_disjoint_closedBall_covering_ae μ g s A (fun _ => 1) fun _ _ => zero_lt_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
t : Set α
r : α → ℝ
left : t.Countable
ts : t ⊆ s
tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1
μt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
F : α → α × Set α := fun (x : α) ↦ (x, closedBall x (r x))
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∀ p ∈ F '' t, p.1 ∈ s
Tactic: refine ⟨F '' t, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
t : Set α
r : α → ℝ
left : t.Countable
ts : t ⊆ s
tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1
μt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
F : α → α × Set α := fun (x : α) ↦ (x, closedBall x (r x))
refine_1 : ∀ p ∈ F '' t, p.1 ∈ s
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : (F '' t).PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2
Tactic: refine ⟨F '' t, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
t : Set α
r : α → ℝ
left : t.Countable
ts : t ⊆ s
tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1
μt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
F : α → α × Set α := fun (x : α) ↦ (x, closedBall x (r x))
refine_1 : ∀ p ∈ F '' t, p.1 ∈ s
refine_2 : (F '' t).PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_3 : ∀ p ∈ F '' t, p.2 ∈ f p.1
Tactic: refine ⟨F '' t, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
t : Set α
r : α → ℝ
left : t.Countable
ts : t ⊆ s
tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1
μt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
F : α → α × Set α := fun (x : α) ↦ (x, closedBall x (r x))
refine_1 : ∀ p ∈ F '' t, p.1 ∈ s
refine_2 : (F '' t).PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2
refine_3 : ∀ p ∈ F '' t, p.2 ∈ f p.1
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_4 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ F '' t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨F '' t, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
β : Type u
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
s : Set α
f : α → Set (Set α)
fsubset : ∀ x ∈ s, f x ⊆ (fun (r : ℝ) ↦ closedBall x r) '' Ioi 0
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : α → Set ℝ := fun (x : α) ↦ {r : ℝ | 0 < r ∧ closedBall x r ∈ f x}
A : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
t : Set α
r : α → ℝ
left : t.Countable
ts : t ⊆ s
tg : ∀ x ∈ t, r x ∈ g x ∩ Ioo 0 1
μt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
F : α → α × Set α := fun (x : α) ↦ (x, closedBall x (r x))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ F '' t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_4 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ y ∈ t, (F y).2) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [biUnion_image]
-- 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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
⊢ Membership.mem (γ := Filter ℝ) (𝓝[>] 0) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s)
have obtain : ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x, a ⊆ closedBall x ε → a ∈ s),
  Membership.mem (γ := Filter ℝ) (𝓝[>] 0) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s)
Tactic: obtain ⟨ε, εpos, hε⟩ :
    ∃ (ε : ℝ), ε > 0 ∧
      ∀ a : Set α, a ∈ (Besicovitch.vitaliFamily μ).setsAt x → a ⊆ closedBall x ε → a ∈ s :=
    (VitaliFamily.mem_filterAt_iff _).1 hs
-- 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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x, a ⊆ closedBall x ε → a ∈ s
⊢ Membership.mem (γ := Filter ℝ) (𝓝[>] 0) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s)
have h : ∀ (_r : ℝ) (hr : _r ∈ Ioc 0 ε), Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s) _r
Tactic: filter_upwards [Ioc_mem_nhdsGT εpos] with _r hr
-- 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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x, a ⊆ closedBall x ε → a ∈ s
_r : ℝ
hr : _r ∈ Ioc 0 ε
⊢ Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s) _r
have h : (fun (r : ℝ) ↦ closedBall x r) _r ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x
Tactic: apply hε
-- 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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
ε : ℝ
εpos : ε > 0
hε : ∀ a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x, a ⊆ closedBall x ε → a ∈ s
_r : ℝ
hr : _r ∈ Ioc 0 ε
h : (fun (r : ℝ) ↦ closedBall x r) _r ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x
⊢ Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s) _r
have h₁ : (fun (r : ℝ) ↦ closedBall x r) _r ⊆ closedBall x ε
Tactic: apply hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
ρ μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
inst_6 : IsLocallyFiniteMeasure ρ
⊢ ∀ᵐ (x : β) ∂μ,
    Tendsto
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))
have h : ∀ (x : β)
  (hx :
    Tendsto
      (fun (a : Set β) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
      (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 (ρ.rnDeriv μ x))),
  Tendsto
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (ρ.rnDeriv μ x))
Tactic: filter_upwards [VitaliFamily.ae_tendsto_rnDeriv (Besicovitch.vitaliFamily μ) ρ] with x hx