awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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
refine_4 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ F '' t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (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:
refine ⟨F '' t, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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))
x : α
hx : x ∈ t
⊢ (F x).1 ∈ s

Tactic:
ts hx
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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))
x : α
hx : x ∈ t
⊢ (F x).1 ∈ s

Tactic:
exact ts hx
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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))
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : F x ≠ F y
⊢ Function.onFun (β := Set α) Disjoint (fun (p : α × Set α) ↦ p.2) (F x) (F y)

Tactic:
tdisj hx hy (ne_of_apply_ne F hxy)

Premises used: setOf, ne_of_apply_ne, Metric.closedBall
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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))
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : F x ≠ F y
⊢ Function.onFun (β := Set α) Disjoint (fun (p : α × Set α) ↦ p.2) (F x) (F y)

Tactic:
exact tdisj hx hy (ne_of_apply_ne F hxy)

Premises used: ne_of_apply_ne
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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))
x : α
hx : x ∈ t
⊢ (F x).2 ∈ f (F x).1

Tactic:
(tg x hx).1.2

Premises used: Set.Mem, setOf, And.right, And.left, Metric.closedBall
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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))
x : α
hx : x ∈ t
⊢ (F x).2 ∈ f (F x).1

Tactic:
exact (tg x hx).1.2

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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_4 refine_4₁ refine_4₂ refine_4₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ y ∈ t, (F y).2) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ F '' t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [biUnion_image]

Premises used: 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 μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
⊢ ∃ ε > 0, ∀ a ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x, a ⊆ closedBall x ε → a ∈ s

Tactic:
(VitaliFamily.mem_filterAt_iff _).1 hs

Premises used: VitaliFamily.mem_filterAt_iff, Iff.mp
-- 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 μ
x : α
s : Set (Set α)
hs : s ∈ VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x
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)
⊢ 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

Premises used: VitaliFamily.mem_filterAt_iff, Iff.mp
-- 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 μ
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
h : ∀ (_r : ℝ) (hr : _r ∈ Ioc 0 ε), Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s) _r
⊢ Membership.mem (γ := Filter ℝ) (𝓝[>] 0) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s)

Tactic:
filter_upwards [Ioc_mem_nhdsGT εpos] with _r hr

Premises used: Ioc_mem_nhdsGT
-- 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 μ
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
h₁ : (fun (r : ℝ) ↦ closedBall x r) _r ⊆ closedBall x ε
⊢ Membership.mem (γ := Set ℝ) ((fun (r : ℝ) ↦ closedBall x r) ⁻¹' s) _r

Tactic:
apply hε
-- 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 μ
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 ε
⊢ (fun (r : ℝ) ↦ closedBall x r) _r ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x

Tactic:
mem_image_of_mem _ hr.1

Premises used: Set.Mem, setOf, And.left, Set.mem_image_of_mem, Set.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 μ
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 ε
⊢ (fun (r : ℝ) ↦ closedBall x r) _r ∈ VitaliFamily.setsAt (Besicovitch.vitaliFamily μ) x

Tactic:
exact mem_image_of_mem _ hr.1

Premises used: And.left, Set.mem_image_of_mem
-- 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 μ
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 ε
⊢ (fun (r : ℝ) ↦ closedBall x r) _r ⊆ closedBall x ε

Tactic:
closedBall_subset_closedBall hr.2

Premises used: And.right, Metric.closedBall_subset_closedBall
-- 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 μ
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 ε
⊢ (fun (r : ℝ) ↦ closedBall x r) _r ⊆ closedBall x ε

Tactic:
exact closedBall_subset_closedBall hr.2

Premises used: And.right, Metric.closedBall_subset_closedBall
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
ρ μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
inst_6 : IsLocallyFiniteMeasure ρ
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))
⊢ ∀ᵐ (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

Premises used: Besicovitch.vitaliFamily, VitaliFamily.ae_tendsto_rnDeriv
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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 : β
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:
hx.comp (tendsto_filterAt μ x)

Premises used: Besicovitch.tendsto_filterAt, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
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 : β
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:
exact hx.comp (tendsto_filterAt μ x)

Premises used: Besicovitch.tendsto_filterAt, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
h :
  ∀ (a : β),
    Tendsto (β := ℝ≥0∞)
        (fun (a : Set β) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
            ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
        (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) a) (𝓝 (s.indicator 1 a)) →
      Tendsto (β := ℝ≥0∞)
        (fun (r : ℝ) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall a r) : ℝ≥0∞)
            ((μ : (a : Set β) → ℝ≥0∞) (closedBall a r) : ℝ≥0∞))
        (𝓝[>] 0) (𝓝 (s.indicator 1 a))
⊢ ∀ᵐ (x : β) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 (s.indicator 1 x))

Tactic:
filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet
      (Besicovitch.vitaliFamily μ) hs]

Premises used: Besicovitch.vitaliFamily, VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
x : β
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set β) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 (s.indicator 1 x))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (s.indicator 1 x))

Tactic:
hx.comp (tendsto_filterAt μ x)

Premises used: Besicovitch.tendsto_filterAt, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
hs : MeasurableSet s
x : β
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set β) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 (s.indicator 1 x))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (s.indicator 1 x))

Tactic:
exact hx.comp (tendsto_filterAt μ x)

Premises used: Besicovitch.tendsto_filterAt, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
x : β
hx :
  Tendsto (β := ℝ≥0∞)
    (fun (a : Set β) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 1)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
        ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 1)

Tactic:
hx.comp (tendsto_filterAt μ x)

Premises used: Besicovitch.tendsto_filterAt, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Covering.Besicovitch
Goal:
β : Type u
inst : MetricSpace β
inst_1 : MeasurableSpace β
inst_2 : BorelSpace β
inst_3 : SecondCountableTopology β
inst_4 : HasBesicovitchCovering β
μ : Measure β
inst_5 : IsLocallyFiniteMeasure μ
s : Set β
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Tendsto (β := ℝ≥0∞)
                    (fun (a : Set β) ↦
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
                        ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
                    (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 1))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Tendsto (β := ℝ≥0∞)
                    (fun (r : ℝ) ↦
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
                        ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
                    (𝓝[>] 0) (𝓝 1))
                x}
            x}
      a
h₁ h₂ :
  ∀ (x : β)
    (hx :
      Tendsto (β := ℝ≥0∞)
        (fun (a : Set β) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ a) : ℝ≥0∞)
            ((μ : (a : Set β) → ℝ≥0∞) a : ℝ≥0∞))
        (VitaliFamily.filterAt (Besicovitch.vitaliFamily μ) x) (𝓝 1)),
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 1)
⊢ ∀ᵐ (x : β) ∂μ.restrict s,
    Tendsto (β := ℝ≥0∞)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) (s ∩ closedBall x r) : ℝ≥0∞)
          ((μ : (a : Set β) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞))
      (𝓝[>] 0) (𝓝 1)

Tactic:
filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div (Besicovitch.vitaliFamily μ) s] with x
    hx using hx.comp (tendsto_filterAt μ x)

Premises used: Besicovitch.vitaliFamily, VitaliFamily.ae_tendsto_measure_inter_div
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin N.succ
⊢ 0 < (a.r (last N))⁻¹ * a.r i

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
simp :
  (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
      (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
      (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
⊢ (a.r (last N))⁻¹ * a.r i ≤
        dist ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ((a.r (last N))⁻¹ • (a.c j - a.c (last N))) ∧
      (a.r (last N))⁻¹ * a.r j ≤ τ * ((a.r (last N))⁻¹ * a.r i) ∨
    (a.r (last N))⁻¹ * a.r j ≤
        dist ((a.r (last N))⁻¹ • (a.c j - a.c (last N))) ((a.r (last N))⁻¹ • (a.c i - a.c (last N))) ∧
      (a.r (last N))⁻¹ * a.r i ≤ τ * ((a.r (last N))⁻¹ * a.r j)

Tactic:
simp (disch := positivity) only [dist_smul₀, dist_sub_right, mul_left_comm τ,
      Real.norm_of_nonneg]

Premises used: dist_sub_right, mul_left_comm, dist_smul₀, Real.norm_of_nonneg