awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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 ∪ ⋃ (i : Fin N), Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have A : ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
Tactic: have A : (∑' x : t0, μ (closedBall x (r x))) ≤ μ s + ε / 2 :=
      calc
        (∑' x : t0, μ (closedBall x (r x))) = ∑' x : t0, μ (closedBall x (r0 x)) := by
          congr 1; ext x; rw [r_t0 x x.2]
        _ = μ (⋃ x : t0, closedBall x (r0 x)) := by
          haveI : Encodable t0 := t0_count.toEncodable
          rw [measure_iUnion]
          · exact (pairwise_subtype_iff_pairwise_set _ _).2 t0_disj
          · exact fun i => measurableSet_closedBall
        _ ≤ μ u := by
          apply measure_mono
          simp only [SetCoe.forall, iUnion_subset_iff]
          intro x hx
          apply Subset.trans (closedBall_subset_ball (hr0 x hx).2.2) (hR x (t0s hx)).2
        _ ≤ μ s + ε / 2 := μu
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (hypothesis)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
i : Fin N
⊢ Eq (α := ℝ≥0∞)
    (∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))))
    (∑' (x : (↑(S i) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r (↑(↑x : (↑s' : Type u_1)) : α))))
have this : InjOn (Subtype.val (p := fun (x : α) ↦ x ∈ s')) (S i)
Tactic: have : InjOn ((↑) : s' → α) (S i) := Subtype.val_injective.injOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
i : Fin N
⊢ Eq (α := ℝ≥0∞)
    (∑' (x : (↑(S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
have haveI : ∀ (this : Encodable (↑(S i) : Type u_1)),
  Eq (α := ℝ≥0∞)
    (∑' (x : (↑(S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
Tactic: haveI : Encodable (S i) := (S_count i).toEncodable
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
i : Fin N
this : Encodable (↑(S i) : Type u_1)
⊢ Eq (α := ℝ≥0∞)
    (∑' (x : (↑(S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
have hn : Pairwise.{u_1} (α := (↑(S i) : Type u_1))
  (Function.onFun (β := Set α) Disjoint fun (x : (↑(S i) : Type u_1)) ↦
    closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α)))
Tactic: rw [measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
i : Fin N
this : Encodable (↑(S i) : Type u_1)
hn :
  Pairwise.{u_1} (α := (↑(S i) : Type u_1))
    (Function.onFun (β := Set α) Disjoint fun (x : (↑(S i) : Type u_1)) ↦
      closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α)))
⊢ Eq (α := ℝ≥0∞)
    (∑' (x : (↑(S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
have h : ∀ (i_1 : (↑(S i) : Type u_1)),
  MeasurableSet (closedBall (↑(↑i_1 : (↑s' : Type u_1)) : α) (r1 (↑(↑i_1 : (↑s' : Type u_1)) : α)))
Tactic: rw [measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
i : Fin N
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)
have h : ⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α)) ⊆ v
Tactic: apply measure_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
i : Fin N
⊢ ⋃ (x : (↑(S i) : Type u_1)), closedBall (↑(↑x : (↑s' : Type u_1)) : α) (r1 (↑(↑x : (↑s' : Type u_1)) : α)) ⊆ v
have h : ∀ (x : α) (h : x ∈ s') (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s') x h ∈ S i), closedBall x (r1 x) ⊆ v
Tactic: simp only [SetCoe.forall, iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
B :
  ∀ (i : Fin N),
    ∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
      ε / 2 / (↑N : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))))
      (∑ i : Fin N,
        ∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
          (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α)))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2) + ∑ i : Fin N, ε / 2 / (↑N : ℝ≥0∞)
have h₂ : ∀ (i : Fin N),
  Membership.mem (γ := Finset (Fin N)) Finset.univ i →
    ∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
      ε / 2 / (↑N : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
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
A :
  ∑' (x : (↑t0 : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2)
B :
  ∀ (i : Fin N),
    ∑' (x : (↑(Subtype.val (p := fun (x : α) ↦ x ∈ s') '' S i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (closedBall (↑x : α) (r (↑x : α))) ≤
      ε / 2 / (↑N : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2) + ∑ i : Fin N, ε / 2 / (↑N : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (ε / 2) + ε / 2
have bc : ∑ i : Fin N, ε / 2 / (↑N : ℝ≥0∞) ≤ ε / 2
Tactic: gcongr