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 μ
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
x : α
hx : x ∈ s
h'x : x ∈ s'
i : Fin N
y : (↑s' : Type u_1)
ySi : y ∈ S i
xy : x ∈ ball (↑y : α) (r1 (↑y : α))
this : (↑y : α) ∈ s'
pos : x ∈ closedBall (↑y : α) (r1 (↑y : α))
⊢ x ∈ closedBall (↑y : α) (r (↑y : α))

Tactic:
simp only [r, if_pos this]

Premises used: if_pos
-- 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
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
x : α
hx : x ∈ s
h'x : x ∈ s'
i : Fin N
y : (↑s' : Type u_1)
ySi : y ∈ S i
xy : x ∈ ball (↑y : α) (r1 (↑y : α))
this : (↑y : α) ∈ s'
⊢ x ∈ closedBall (↑y : α) (r1 (↑y : α))

Tactic:
ball_subset_closedBall xy

Premises used: Metric.ball_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 μ
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
x : α
hx : x ∈ s
h'x : x ∈ s'
i : Fin N
y : (↑s' : Type u_1)
ySi : y ∈ S i
xy : x ∈ ball (↑y : α) (r1 (↑y : α))
this : (↑y : α) ∈ s'
⊢ x ∈ closedBall (↑y : α) (r1 (↑y : α))

Tactic:
exact ball_subset_closedBall xy

Premises used: Metric.ball_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 μ
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
x : α
hx : x ∈ s
h'x : x ∉ s'
⊢ ∃ y ∈ t0, x ∈ closedBall y (r0 y)

Tactic:
simpa [s', hx, -mem_closedBall] using h'x

Premises used: Metric.mem_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 μ
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
x : α
hx : x ∈ s
h'x : x ∉ s'
neg :
  ∀ (y : α) (yt0 : y ∈ t0) (hxy : x ∈ closedBall y (r0 y)),
    Membership.mem (γ := Set α)
      (⋃ x ∈ t0 ∪ ⋃ (i : Fin N), Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i, closedBall x (r x)) x
⊢ Membership.mem (γ := Set α)
    (⋃ x ∈ t0 ∪ ⋃ (i : Fin N), Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i, closedBall x (r x)) x

Tactic:
obtain ⟨y, yt0, hxy⟩ : ∃ y : α, y ∈ t0 ∧ x ∈ closedBall y (r0 y) := by
        simpa [s', hx, -mem_closedBall] using h'x
-- 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
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
x : α
hx : x ∈ s
h'x : x ∉ s'
y : α
yt0 : y ∈ t0
hxy : x ∈ closedBall y (r0 y)
⊢ Membership.mem (γ := Set α)
    (⋃ x ∈ t0 ∪ ⋃ (i : Fin N), Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i, closedBall x (r x)) x

Tactic:
mem_iUnion₂.2 ⟨y, Or.inl yt0, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro, Or.inl
-- 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
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
x : α
hx : x ∈ s
h'x : x ∉ s'
y : α
yt0 : y ∈ t0
hxy : x ∈ closedBall y (r0 y)
neg : x ∈ closedBall y (r y)
⊢ Membership.mem (γ := Set α)
    (⋃ x ∈ t0 ∪ ⋃ (i : Fin N), Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i, closedBall x (r x)) x

Tactic:
refine mem_iUnion₂.2 ⟨y, Or.inl yt0, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, 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 μ
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
x : α
hx : x ∈ s
h'x : x ∉ s'
y : α
yt0 : y ∈ t0
hxy neg neg₁ neg₂ neg₃ : x ∈ closedBall y (r0 y)
⊢ x ∈ closedBall y (r y)

Tactic:
rwa [r_t0 _ yt0]
-- 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
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
e_f :
  Eq.{u_1 + 1} (α := (↑t0 : Type u_1) → ℝ≥0∞)
    (fun (x : (↑t0 : Type u_1)) ↦ (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))))
    fun (x : (↑t0 : Type u_1)) ↦ (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α)))
⊢ Eq (α := ℝ≥0∞) (∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))))
    (∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α))))

Tactic:
congr 1
-- 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
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
e_f :
  ∀ (x : (↑t0 : Type u_1)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α))) : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := (↑t0 : Type u_1) → ℝ≥0∞)
    (fun (x : (↑t0 : Type u_1)) ↦ (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))))
    fun (x : (↑t0 : Type u_1)) ↦ (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α)))

Tactic:
ext x
-- 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
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
x : (↑t0 : Type u_1)
e_f e_f₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α))) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α))) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r0 (↑x : α))) : ℝ≥0∞)

Tactic:
rw [r_t0 x x.2]

Premises used: Subtype.val, Subtype.property