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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ (↑t : Set (α × ℝ))
q : α × ℝ
hq : Membership.mem (γ := Set (α × ℝ)) ((fun (x : α) ↦ (x, r x)) '' (↑v : Set α)) q
hpq : p ≠ q
refine_1 :
  ∀ (q' : α) (q'v : q' ∈ (↑v : Set α))
    (hq : Membership.mem (γ := Set (α × ℝ)) ((fun (x : α) ↦ (x, r x)) '' (↑v : Set α)) (q', r q'))
    (hpq : p ≠ (q', r q')), Disjoint (closedBall p.1 p.2) (closedBall (q', r q').1 (q', r q').2)
⊢ Disjoint (closedBall p.1 p.2) (closedBall q.1 q.2)

Tactic:
rcases (mem_image _ _ _).1 hq with ⟨q', q'v, rfl⟩

Premises used: Set.mem_image, Iff.mp, 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ (↑t : Set (α × ℝ))
q' : α
q'v : q' ∈ (↑v : Set α)
hq : Membership.mem (γ := Set (α × ℝ)) ((fun (x : α) ↦ (x, r x)) '' (↑v : Set α)) (q', r q')
hpq : p ≠ (q', r q')
apply : closedBall p.1 p.2 ⊆ B
⊢ Disjoint (closedBall p.1 p.2) (closedBall (q', r q').1 (q', r q').2)

Tactic:
apply disjoint_of_subset_left _ (hr q' (vs' q'v)).2

Premises used: Set.disjoint_of_subset_left, And.right
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ (↑t : Set (α × ℝ))
q' : α
q'v : q' ∈ (↑v : Set α)
hq : Membership.mem (γ := Set (α × ℝ)) ((fun (x : α) ↦ (x, r x)) '' (↑v : Set α)) (q', r q')
hpq : p ≠ (q', r q')
rw : closedBall p.1 p.2 ⊆ ⋃ x ∈ (↑t : Set (α × ℝ)), closedBall x.1 x.2
⊢ closedBall p.1 p.2 ⊆ B

Tactic:
rw [hB, ← Finset.set_biUnion_coe]

Premises used: Finset.set_biUnion_coe
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ (↑t : Set (α × ℝ))
q' : α
q'v : q' ∈ (↑v : Set α)
hq : Membership.mem (γ := Set (α × ℝ)) ((fun (x : α) ↦ (x, r x)) '' (↑v : Set α)) (q', r q')
hpq : p ≠ (q', r q')
⊢ closedBall p.1 p.2 ⊆ ⋃ x ∈ (↑t : Set (α × ℝ)), closedBall x.1 x.2

Tactic:
subset_biUnion_of_mem (u := fun x : α × ℝ => closedBall x.1 x.2) hp

Premises used: Set.subset_biUnion_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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ (↑t : Set (α × ℝ))
q' : α
q'v : q' ∈ (↑v : Set α)
hq : Membership.mem (γ := Set (α × ℝ)) ((fun (x : α) ↦ (x, r x)) '' (↑v : Set α)) (q', r q')
hpq : p ≠ (q', r q')
⊢ closedBall p.1 p.2 ⊆ ⋃ x ∈ (↑t : Set (α × ℝ)), closedBall x.1 x.2

Tactic:
exact subset_biUnion_of_mem (u := fun x : α × ℝ => closedBall x.1 x.2) hp

Premises used: Set.subset_biUnion_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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
refine_2 : ∀ (h'p : p ∈ t), p.1 ∈ s
refine_2₁ : ∀ (h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) p), p.1 ∈ s
⊢ p.1 ∈ s

Tactic:
rcases Finset.mem_union.1 hp with (h'p | h'p)

Premises used: Iff.mp, Finset.mem_union
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : p ∈ t
⊢ p.1 ∈ s

Tactic:
ht.2.1 p h'p

Premises used: And.right, And.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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : p ∈ t
⊢ p.1 ∈ s

Tactic:
exact ht.2.1 p h'p

Premises used: And.right, And.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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) p
refine_2 :
  ∀ (p' : α) (p'v : p' ∈ v) (hp : (p', r p') ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v)
    (h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) (p', r p')), (p', r p').1 ∈ s
⊢ p.1 ∈ s

Tactic:
rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩

Premises used: Finset.mem_image, Iff.mp, 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p' : α
p'v : p' ∈ v
hp : (p', r p') ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) (p', r p')
⊢ (p', r p').1 ∈ s

Tactic:
((mem_diff _).1 (vs' (Finset.mem_coe.2 p'v))).1

Premises used: Iff.mpr, Set.Mem, And.left, Set.mem_diff, Iff.mp, Finset.mem_coe
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p' : α
p'v : p' ∈ v
hp : (p', r p') ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) (p', r p')
⊢ (p', r p').1 ∈ s

Tactic:
exact ((mem_diff _).1 (vs' (Finset.mem_coe.2 p'v))).1

Premises used: Iff.mpr, And.left, Set.mem_diff, Iff.mp, Finset.mem_coe
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
refine_3 : ∀ (h'p : p ∈ t), p.2 ∈ f p.1
refine_3₁ : ∀ (h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) p), p.2 ∈ f p.1
⊢ p.2 ∈ f p.1

Tactic:
rcases Finset.mem_union.1 hp with (h'p | h'p)

Premises used: Iff.mp, Finset.mem_union
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : p ∈ t
⊢ p.2 ∈ f p.1

Tactic:
ht.2.2 p h'p

Premises used: And.right
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : p ∈ t
⊢ p.2 ∈ f p.1

Tactic:
exact ht.2.2 p h'p

Premises used: And.right
-- 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p : α × ℝ
hp : p ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) p
refine_3 :
  ∀ (p' : α) (p'v : p' ∈ v) (hp : (p', r p') ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v)
    (h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) (p', r p')),
    (p', r p').2 ∈ f (p', r p').1
⊢ p.2 ∈ f p.1

Tactic:
rcases Finset.mem_image.1 h'p with ⟨p', p'v, rfl⟩

Premises used: Finset.mem_image, Iff.mp, 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 : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun (t : Finset (α × ℝ)) ↦
    ((↑t : Set (α × ℝ)).PairwiseDisjoint (α := Set α) fun (p : α × ℝ) ↦ closedBall p.1 p.2) ∧
      (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : (x : α) → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : (↑v : Set α) ⊆ s'
hμv :
  (μ : (a : Set α) → ℝ≥0∞) (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
hv : (↑v : Set α).PairwiseDisjoint (α := Set α) fun (x : α) ↦ closedBall x (r x)
p' : α
p'v : p' ∈ v
hp : (p', r p') ∈ t ∪ Finset.image (fun (x : α) ↦ (x, r x)) v
h'p : Membership.mem (γ := Finset (α × ℝ)) (Finset.image (fun (x : α) ↦ (x, r x)) v) (p', r p')
⊢ (p', r p').2 ∈ f (p', r p').1

Tactic:
(hr p' (vs' p'v)).1.1

Premises used: Set.Mem, And.left