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 α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
rcases :
  ∀ (ν : Measure α) (hν : IsFiniteMeasure ν) (hμν : μ ≪ ν),
    ∃ (t : Set (α × ℝ)),
      t.Countable ∧
        (∀ p ∈ t, p.1 ∈ s) ∧
          (∀ p ∈ t, p.2 ∈ f p.1) ∧
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
              t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
⊢ ∃ (t : Set (α × ℝ)),
    t.Countable ∧
      (∀ p ∈ t, p.1 ∈ s) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2

Tactic:
rcases exists_isFiniteMeasure_absolutelyContinuous μ with ⟨ν, hν, hμν, -⟩

Premises used: MeasureTheory.exists_isFiniteMeasure_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
ν : Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
rcases :
  ∀ (t : Set (α × ℝ)) (t_count : t.Countable) (ts : ∀ p ∈ t, p.1 ∈ s) (tr : ∀ p ∈ t, p.2 ∈ f p.1)
    (tν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞))
    (tdisj : t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2),
    ∃ (t : Set (α × ℝ)),
      t.Countable ∧
        (∀ p ∈ t, p.1 ∈ s) ∧
          (∀ p ∈ t, p.2 ∈ f p.1) ∧
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
              t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
⊢ ∃ (t : Set (α × ℝ)),
    t.Countable ∧
      (∀ p ∈ t, p.1 ∈ s) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2

Tactic:
rcases exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux ν f s hf with
    ⟨t, t_count, ts, tr, tν, tdisj⟩

Premises used: Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
ν : Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
t : Set (α × ℝ)
t_count : t.Countable
ts : ∀ p ∈ t, p.1 ∈ s
tr : ∀ p ∈ t, p.2 ∈ f p.1
tν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
⊢ ∃ (t : Set (α × ℝ)),
    t.Countable ∧
      (∀ p ∈ t, p.1 ∈ s) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2

Tactic:
⟨t, t_count, ts, tr, hμν tν, tdisj⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
ν : Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
t : Set (α × ℝ)
t_count : t.Countable
ts : ∀ p ∈ t, p.1 ∈ s
tr : ∀ p ∈ t, p.2 ∈ f p.1
tν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
tdisj : t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
⊢ ∃ (t : Set (α × ℝ)),
    t.Countable ∧
      (∀ p ∈ t, p.1 ∈ s) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2

Tactic:
exact ⟨t, t_count, ts, tr, hμν tν, tdisj⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
x : α
hx : x ∈ s
δ : ℝ
δpos : δ > 0
rcases : ∀ (r : ℝ) (hr : r ∈ f x ∩ Ioo 0 (min δ (R x))), (g x ∩ Ioo 0 δ).Nonempty
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
rcases hf x hx (min δ (R x)) (lt_min δpos (hR x hx)) with ⟨r, hr⟩

Premises used: lt_min, Min.min
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
x : α
hx : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
hr : r ∈ f x ∩ Ioo 0 (min δ (R x))
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
⟨r, ⟨⟨hr.1, hr.2.1, hr.2.2.trans_le (min_le_right _ _)⟩,
      ⟨hr.2.1, hr.2.2.trans_le (min_le_left _ _)⟩⟩⟩

Premises used: min_le_left, Set.Nonempty, And.right, And.left, LT.lt.trans_le, And.intro, min_le_right, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
x : α
hx : x ∈ s
δ : ℝ
δpos : δ > 0
r : ℝ
hr : r ∈ f x ∩ Ioo 0 (min δ (R x))
⊢ (g x ∩ Ioo 0 δ).Nonempty

Tactic:
exact ⟨r, ⟨⟨hr.1, hr.2.1, hr.2.2.trans_le (min_le_right _ _)⟩,
      ⟨hr.2.1, hr.2.2.trans_le (min_le_left _ _)⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
⊢ ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty

Tactic:
have hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty := fun x hx δ δpos ↦ by
    rcases hf x hx (min δ (R x)) (lt_min δpos (hR x hx)) with ⟨r, hr⟩
    exact ⟨r, ⟨⟨hr.1, hr.2.1, hr.2.2.trans_le (min_le_right _ _)⟩,
      ⟨hr.2.1, hr.2.2.trans_le (min_le_left _ _)⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
rcases :
  ∀ (v : Set (α × ℝ)) (v_count : v.Countable) (vs : ∀ p ∈ v, p.1 ∈ s) (vg : ∀ p ∈ v, p.2 ∈ g p.1)
    (μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞))
    (v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2),
    ∃ (t : Set α) (r : α → ℝ),
      t.Countable ∧
        t ⊆ s ∧
          (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
              t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
⊢ ∃ (t : Set α) (r : α → ℝ),
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
rcases exists_disjoint_closedBall_covering_ae_aux μ g s hg with ⟨v, v_count, vs, vg, μv, v_disj⟩

Premises used: Besicovitch.exists_disjoint_closedBall_covering_ae_aux
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
v : Set (α × ℝ)
v_count : v.Countable
vs : ∀ p ∈ v, p.1 ∈ s
vg : ∀ p ∈ v, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
⊢ ∀ p ∈ v, 0 ≤ p.2

Tactic:
have I : ∀ p ∈ v, 0 ≤ p.2 := fun p hp => (vg p hp).2.1.le
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
v : Set (α × ℝ)
v_count : v.Countable
vs : ∀ p ∈ v, p.1 ∈ s
vg : ∀ p ∈ v, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
I : ∀ p ∈ v, 0 ≤ p.2
rw : InjOn Prod.fst v
⊢ ∃ (r : α → ℝ) (t : Set α), v = graphOn r t

Tactic:
rw [exists_eq_graphOn]

Premises used: Set.exists_eq_graphOn
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
v : Set (α × ℝ)
v_count : v.Countable
vs : ∀ p ∈ v, p.1 ∈ s
vg : ∀ p ∈ v, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
I : ∀ p ∈ v, 0 ≤ p.2
⊢ InjOn Prod.fst v

Tactic:
fun x hx y hy heq ↦ v_disj.eq hx hy <| not_disjoint_iff.2 ⟨x.1, ?_⟩

Premises used: Iff.mpr, Prod.fst, Set.not_disjoint_iff, Exists.intro, Set.Pairwise.eq, Set.InjOn
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
v : Set (α × ℝ)
v_count : v.Countable
vs : ∀ p ∈ v, p.1 ∈ s
vg : ∀ p ∈ v, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
I : ∀ p ∈ v, 0 ≤ p.2
refine :
  ∀ (x : α × ℝ) (hx : x ∈ v) (y : α × ℝ) (hy : y ∈ v) (heq : x.1 = y.1),
    Membership.mem (γ := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) x) x.1 ∧
      Membership.mem (γ := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) y) x.1
⊢ InjOn Prod.fst v

Tactic:
refine fun x hx y hy heq ↦ v_disj.eq hx hy <| not_disjoint_iff.2 ⟨x.1, ?_⟩

Premises used: Iff.mpr, Set.not_disjoint_iff, Exists.intro, Set.Pairwise.eq
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
v : Set (α × ℝ)
v_count : v.Countable
vs : ∀ p ∈ v, p.1 ∈ s
vg : ∀ p ∈ v, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
I : ∀ p ∈ v, 0 ≤ p.2
x : α × ℝ
hx : x ∈ v
y : α × ℝ
hy : y ∈ v
heq : x.1 = y.1
⊢ Membership.mem (γ := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) x) x.1 ∧
    Membership.mem (γ := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) y) x.1

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
v : Set (α × ℝ)
v_count : v.Countable
vs : ∀ p ∈ v, p.1 ∈ s
vg : ∀ p ∈ v, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ v, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : v.PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
obtain :
  ∀ (r : α → ℝ) (t : Set α) (v_count : (graphOn r t).Countable) (vs : ∀ p ∈ graphOn r t, p.1 ∈ s)
    (vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1)
    (μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞))
    (v_disj : (graphOn r t).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2),
    ∃ (t : Set α) (r : α → ℝ),
      t.Countable ∧
        t ⊆ s ∧
          (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
              t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
⊢ ∃ (t : Set α) (r : α → ℝ),
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
obtain ⟨r, t, rfl⟩ : ∃ (r : α → ℝ) (t : Set α), v = graphOn r t := by
    have I : ∀ p ∈ v, 0 ≤ p.2 := fun p hp => (vg p hp).2.1.le
    rw [exists_eq_graphOn]
    refine fun x hx y hy heq ↦ v_disj.eq hx hy <| not_disjoint_iff.2 ⟨x.1, ?_⟩
    simp [*]

Premises used: rfl, Set
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : (graphOn r t).Countable
vs : ∀ p ∈ graphOn r t, p.1 ∈ s
vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : (graphOn r t).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
⊢ InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t

Tactic:
have hinj : InjOn (fun x ↦ (x, r x)) t := LeftInvOn.injOn (f₁' := Prod.fst) fun _ _ ↦ rfl
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : (graphOn r t).Countable
vs : ∀ p ∈ graphOn r t, p.1 ∈ s
vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : (graphOn r t).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
hinj : InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t
⊢ ∀ ⦃x : α⦄, x ∈ t → x ∈ s

Tactic:
simp only [graphOn, forall_mem_image, biUnion_image, hinj.pairwiseDisjoint_image] at *

Premises used: Set.graphOn, Set.InjOn.pairwiseDisjoint_image, Set.forall_mem_image, Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : (graphOn r t).Countable
vs : ∀ p ∈ graphOn r t, p.1 ∈ s
vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : (graphOn r t).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
hinj : InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t
vs₁ : ∀ ⦃x : α⦄, x ∈ t → x ∈ s
⊢ ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x

Tactic:
simp only [graphOn, forall_mem_image, biUnion_image, hinj.pairwiseDisjoint_image] at *

Premises used: Set.graphOn, Set.InjOn.pairwiseDisjoint_image, Set.forall_mem_image, Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : (graphOn r t).Countable
vs : ∀ p ∈ graphOn r t, p.1 ∈ s
vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : (graphOn r t).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
hinj : InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t
vs₁ : ∀ ⦃x : α⦄, x ∈ t → x ∈ s
vg₁ : ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ y ∈ t, closedBall y (r y)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [graphOn, forall_mem_image, biUnion_image, hinj.pairwiseDisjoint_image] at *

Premises used: Set.graphOn, Set.InjOn.pairwiseDisjoint_image, Set.forall_mem_image, Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : (graphOn r t).Countable
vs : ∀ p ∈ graphOn r t, p.1 ∈ s
vg : ∀ p ∈ graphOn r t, p.2 ∈ g p.1
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ graphOn r t, closedBall p.1 p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : (graphOn r t).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2
hinj : InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t
vs₁ : ∀ ⦃x : α⦄, x ∈ t → x ∈ s
vg₁ : ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x
μv₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ y ∈ t, closedBall y (r y)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t.PairwiseDisjoint (α := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∘ fun (x : α) ↦ (x, r x))

Tactic:
simp only [graphOn, forall_mem_image, biUnion_image, hinj.pairwiseDisjoint_image] at *

Premises used: Set.graphOn, Set.InjOn.pairwiseDisjoint_image, Set.forall_mem_image, Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : Set.Countable (α := α × ℝ) ((fun (x : α) ↦ (x, r x)) '' t)
hinj : InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t
vs : ∀ ⦃x : α⦄, x ∈ t → x ∈ s
vg : ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ y ∈ t, closedBall y (r y)) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : t.PairwiseDisjoint (α := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∘ fun (x : α) ↦ (x, r x))
⊢ ∃ (t : Set α) (r : α → ℝ),
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
⟨t, r, countable_of_injective_of_countable_image hinj v_count, vs, vg, μv, v_disj⟩

Premises used: Set.countable_of_injective_of_countable_image, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
inst_4 : HasBesicovitchCovering α
μ : Measure α
inst_5 : SFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
g : (x : α) → Set ℝ := fun (x : α) ↦ f x ∩ Ioo 0 (R x)
hg : ∀ x ∈ s, ∀ δ > 0, (g x ∩ Ioo 0 δ).Nonempty
r : α → ℝ
t : Set α
v_count : Set.Countable (α := α × ℝ) ((fun (x : α) ↦ (x, r x)) '' t)
hinj : InjOn (β := α × ℝ) (fun (x : α) ↦ (x, r x)) t
vs : ∀ ⦃x : α⦄, x ∈ t → x ∈ s
vg : ∀ ⦃x : α⦄, x ∈ t → r x ∈ g x
μv : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ y ∈ t, closedBall y (r y)) : ℝ≥0∞) (0 : ℝ≥0∞)
v_disj : t.PairwiseDisjoint (α := Set α) ((fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∘ fun (x : α) ↦ (x, r x))
⊢ ∃ (t : Set α) (r : α → ℝ),
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Ioo 0 (R x)) ∧
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ x ∈ t, closedBall x (r x)) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)

Tactic:
exact ⟨t, r, countable_of_injective_of_countable_image hinj v_count, vs, vg, μv, v_disj⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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
⊢ ε / 2 ≠ 0

Tactic:
simpa only [or_false, Ne, ENNReal.div_eq_zero_iff, ENNReal.ofNat_ne_top] using hε

Premises used: ENNReal.ofNat_ne_top, Ne, ENNReal.div_eq_zero_iff, or_false