awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ min d (R (c a))
ax : B a ⊆ ball x (R x)
b : ι
bu : b ∈ u
ab : (B a ∩ B b).Nonempty
bdiam : r a ≤ 2 * r b
bv : b ∈ v
b' : (↑v : Type u_2) := Subtype.mk (p := fun (x : ι) ↦ x ∈ v) b bv
b'_notmem_w : b' ∉ w
b'' : { a : (↑v : Type u_2) // a ∉ w } := Subtype.mk (p := fun (a : (↑v : Type u_2)) ↦ a ∉ w) b' b'_notmem_w
zb : c a ∈ closedBall (c b) (3 * r b)
suffices :
  closedBall (c (↑(↑b'' : (↑v : Type u_2)) : ι)) (3 * r (↑(↑b'' : (↑v : Type u_2)) : ι)) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
⊢ Membership.mem (γ := Set α)
    (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι)))
    (c a)

Tactic:
suffices H : closedBall (c b'') (3 * r b'')
        ⊆ ⋃ a : { a // a ∉ w }, closedBall (c a) (3 * r a) from H zb
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ min d (R (c a))
ax : B a ⊆ ball x (R x)
b : ι
bu : b ∈ u
ab : (B a ∩ B b).Nonempty
bdiam : r a ≤ 2 * r b
bv : b ∈ v
b' : (↑v : Type u_2) := Subtype.mk (p := fun (x : ι) ↦ x ∈ v) b bv
b'_notmem_w : b' ∉ w
b'' : { a : (↑v : Type u_2) // a ∉ w } := Subtype.mk (p := fun (a : (↑v : Type u_2)) ↦ a ∉ w) b' b'_notmem_w
zb : c a ∈ closedBall (c b) (3 * r b)
⊢ closedBall (c (↑(↑b'' : (↑v : Type u_2)) : ι)) (3 * r (↑(↑b'' : (↑v : Type u_2)) : ι)) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))

Tactic:
subset_iUnion (fun a : { a // a ∉ w } => closedBall (c a) (3 * r a)) b''

Premises used: HMul.hMul, Set.subset_iUnion, Metric.closedBall, OfNat.ofNat, Subtype.val
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
k : Set α := ⋃ a ∈ w, B (↑a : ι)
k_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] k
d : ℝ
dpos : 0 < d
a : ι
hat : a ∈ t
hz : c a ∈ (s \ ⋃ a ∈ u, B a) ∩ ball x (R x)
z_notmem_k : c a ∉ k
this : ball x (R x) \ k ∈ 𝓝 (c a)
hd : closedBall (c a) d ⊆ ball x (R x) \ k
ad : r a ≤ min d (R (c a))
ax : B a ⊆ ball x (R x)
b : ι
bu : b ∈ u
ab : (B a ∩ B b).Nonempty
bdiam : r a ≤ 2 * r b
bv : b ∈ v
b' : (↑v : Type u_2) := Subtype.mk (p := fun (x : ι) ↦ x ∈ v) b bv
b'_notmem_w : b' ∉ w
b'' : { a : (↑v : Type u_2) // a ∉ w } := Subtype.mk (p := fun (a : (↑v : Type u_2)) ↦ a ∉ w) b' b'_notmem_w
zb : c a ∈ closedBall (c b) (3 * r b)
⊢ closedBall (c (↑(↑b'' : (↑v : Type u_2)) : ι)) (3 * r (↑(↑b'' : (↑v : Type u_2)) : ι)) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))

Tactic:
exact subset_iUnion (fun a : { a // a ∉ w } => closedBall (c a) (3 * r a)) b''

Premises used: HMul.hMul, Set.subset_iUnion, Metric.closedBall, OfNat.ofNat, Subtype.val
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
⊢ Countable.{u_2 + 1} (↑v : Type u_2)

Tactic:
haveI : Countable v := (u_count.mono vu).to_subtype
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((s \ ⋃ a ∈ u, B a) ∩ ball x (R x)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
          closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))) :
      ℝ≥0∞)

Tactic:
measure_mono M

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
          closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))) :
      ℝ≥0∞)
    (∑' (a : { a : (↑v : Type u_2) // a ∉ w }),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))) :
      ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ LE.le (α := ℝ≥0∞)
    (∑' (a : { a : (↑v : Type u_2) // a ∉ w }),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))))
    (∑' (a : { a : (↑v : Type u_2) // a ∉ w }),
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) : ℝ≥0∞))

Tactic:
(ENNReal.tsum_le_tsum fun a => μB a (ut (vu a.1.2)))

Premises used: ENNReal.tsum_le_tsum, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ ∑' (a : { a : (↑v : Type u_2) // a ∉ w }),
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) : ℝ≥0∞) =
    (↑C : ℝ≥0∞) * ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι))

Tactic:
ENNReal.tsum_mul_left

Premises used: ENNReal.tsum_mul_left
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ (↑C : ℝ≥0∞) * ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) ≤
    (↑C : ℝ≥0∞) * (ε / (↑C : ℝ≥0∞))

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB :
  ∀ a ∈ t,
    (μ : (a : Set α) → ℝ≥0∞) (closedBall (c a) (3 * r a)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B a) : ℝ≥0∞)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : (x : α) → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (20 * R x)) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set ι := {a : ι | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
x : α
h : x ∈ s \ ⋃ a ∈ u, B a
v : Set ι := {a : ι | a ∈ u ∧ (B a ∩ ball x (R x)).Nonempty}
vu : v ⊆ u
K : ℝ
μK : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x K) : ℝ≥0∞) (∞ : ℝ≥0∞)
hK : ∀ a ∈ u, (B a ∩ ball x (R x)).Nonempty → B a ⊆ closedBall x K
ε : ℝ≥0∞
εpos : 0 < ε
I : LT.lt (α := ℝ≥0∞) (∑' (a : (↑v : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (B (↑a : ι))) ∞
w : Finset (↑v : Type u_2)
hw :
  ∑' (a : { a : (↑v : Type u_2) // a ∉ w }), (μ : (a : Set α) → ℝ≥0∞) (B (↑(↑a : (↑v : Type u_2)) : ι)) <
    ε / (↑C : ℝ≥0∞)
M :
  (s \ ⋃ a ∈ u, B a) ∩ ball x (R x) ⊆
    ⋃ (a : { a : (↑v : Type u_2) // a ∉ w }),
      closedBall (c (↑(↑a : (↑v : Type u_2)) : ι)) (3 * r (↑(↑a : (↑v : Type u_2)) : ι))
this : Countable.{u_2 + 1} (↑v : Type u_2)
⊢ (↑C : ℝ≥0∞) * (ε / (↑C : ℝ≥0∞)) ≤ ε

Tactic:
ENNReal.mul_div_le

Premises used: ENNReal.mul_div_le