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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
q : ℝ × α × Set α
hq : q ∈ t'
q' : ℝ × α × Set α
hq' : q' ∈ t'
hqq' : Ne.{u_1 + 1} (α := α × Set α) ((fun (p : ℝ × α × Set α) ↦ p.2) q) ((fun (p : ℝ × α × Set α) ↦ p.2) q')
⊢ Function.onFun (β := Set α) Disjoint (fun (p : α × Set α) ↦ p.2) ((fun (p : ℝ × α × Set α) ↦ p.2) q)
    ((fun (p : ℝ × α × Set α) ↦ p.2) q')

Tactic:
t'_disj hq hq' (ne_of_apply_ne _ hqq')

Premises used: ne_of_apply_ne
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
q : ℝ × α × Set α
hq : q ∈ t'
q' : ℝ × α × Set α
hq' : q' ∈ t'
hqq' : Ne.{u_1 + 1} (α := α × Set α) ((fun (p : ℝ × α × Set α) ↦ p.2) q) ((fun (p : ℝ × α × Set α) ↦ p.2) q')
⊢ Function.onFun (β := Set α) Disjoint (fun (p : α × Set α) ↦ p.2) ((fun (p : ℝ × α × Set α) ↦ p.2) q)
    ((fun (p : ℝ × α × Set α) ↦ p.2) q')

Tactic:
exact t'_disj hq hq' (ne_of_apply_ne _ hqq')

Premises used: ne_of_apply_ne
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
q : ℝ × α × Set α
hq : q ∈ t'
⊢ ((fun (p : ℝ × α × Set α) ↦ p.2) q).2 ∈ f ((fun (p : ℝ × α × Set α) ↦ p.2) q).1

Tactic:
(t't hq).2.2.2.2.1

Premises used: Set.Mem, And.right, And.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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
q : ℝ × α × Set α
hq : q ∈ t'
⊢ ((fun (p : ℝ × α × Set α) ↦ p.2) q).2 ∈ f ((fun (p : ℝ × α × Set α) ↦ p.2) q).1

Tactic:
exact (t't hq).2.2.2.2.1

Premises used: And.right, And.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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
μt'
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ :
  Eq.{u_1 + 1} (α := Set α)
    (⋃ (p : α × Set α), ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2)
    (⋃ a ∈ t', a.2.2)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (s \
          ⋃ (p : α × Set α),
            ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
convert! μt' using 3
-- 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 μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ h₂ : Eq.{u_1 + 1} (α := Set α) (⋃ y ∈ t', y.2.2) (⋃ a ∈ t', a.2.2)
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (p : α × Set α), ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2)
    (⋃ a ∈ t', a.2.2)

Tactic:
rw [biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
⊢ ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ v.setsAt p.1 ∩ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)

Tactic:
v.covering s (fun x => v.setsAt x ∩ f x) (fun _ _ => inter_subset_left) h

Premises used: Set.inter_subset_left, Inter.inter, VitaliFamily.setsAt, VitaliFamily.covering
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
⊢ ∀ p ∈ h.index (f := f) (s := s), p.1 ∈ s

Tactic:
h.exists_disjoint_covering_ae.choose_spec.1

Premises used: Exists.choose_spec, Set.Mem, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, And.left, VitaliFamily.FineSubfamilyOn.index
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
⊢ h.index (f := f) (s := s).PairwiseDisjoint (h.covering (f := f) (s := s))

Tactic:
h.exists_disjoint_covering_ae.choose_spec.2.1

Premises used: VitaliFamily.FineSubfamilyOn.covering, Exists.choose_spec, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, And.right, And.left, VitaliFamily.FineSubfamilyOn.index
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
⊢ Pairwise.{u_1} (α := (↑(h.index (f := f) (s := s)) : Type u_1))
    (Function.onFun (β := Set X) Disjoint fun (x : (↑(h.index (f := f) (s := s)) : Type u_1)) ↦
      h.covering (f := f) (s := s) (↑x : X × Set X))

Tactic:
(pairwise_subtype_iff_pairwise_set _ _).2 h.covering_disjoint

Premises used: Iff.mpr, pairwise_subtype_iff_pairwise_set, VitaliFamily.FineSubfamilyOn.covering_disjoint
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
p : X × Set X
hp : p ∈ h.index (f := f) (s := s)
⊢ h.covering (f := f) (s := s) p ∈ f p.1

Tactic:
(h.exists_disjoint_covering_ae.choose_spec.2.2.1 p hp).2

Premises used: VitaliFamily.FineSubfamilyOn.covering, Exists.choose_spec, Set.Mem, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, And.right, And.left
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
p : X × Set X
hp : p ∈ h.index (f := f) (s := s)
⊢ h.covering (f := f) (s := s) p ∈ v.setsAt p.1

Tactic:
(h.exists_disjoint_covering_ae.choose_spec.2.2.1 p hp).1

Premises used: VitaliFamily.FineSubfamilyOn.covering, Exists.choose_spec, Set.Mem, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, And.right, And.left
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
⊢ Eq (α := ENNReal)
    ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
    (0 : ENNReal)

Tactic:
h.exists_disjoint_covering_ae.choose_spec.2.2.2

Premises used: VitaliFamily.FineSubfamilyOn.covering, Exists.choose_spec, Set.Mem, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, And.right, VitaliFamily.FineSubfamilyOn.index
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
⊢ h.index (f := f) (s := s).Countable

Tactic:
h.covering_disjoint.countable_of_nonempty_interior fun _ hx =>
    v.nonempty_interior _ _ (h.covering_mem_family hx)

Premises used: VitaliFamily.nonempty_interior, VitaliFamily.FineSubfamilyOn.covering, VitaliFamily.FineSubfamilyOn.covering_mem_family, Prod.fst, VitaliFamily.FineSubfamilyOn.covering_disjoint, Set.PairwiseDisjoint.countable_of_nonempty_interior
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
p : X × Set X
hp : p ∈ h.index (f := f) (s := s)
⊢ MeasurableSet (h.covering (f := f) (s := s) p)

Tactic:
v.measurableSet p.1 _ (h.covering_mem_family hp)

Premises used: VitaliFamily.FineSubfamilyOn.covering_mem_family, Prod.fst, VitaliFamily.measurableSet
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ s ⊆
    (s \ ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) ∪
      ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p

Tactic:
simp only [subset_union_left, diff_union_self]

Premises used: Set.diff_union_self, Set.subset_union_left
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
rw :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
rw₁ :
  Eq (α := ENNReal)
    ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
    (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
        (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)) :
      ENNReal)
rw₂ rw₃ :
  Eq (α := ENNReal)
    (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)))
    (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)))
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal)
      ((ρ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))

Tactic:
rw [hρ h.measure_diff_biUnion, zero_add,
        measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]

Premises used: VitaliFamily.FineSubfamilyOn.measure_diff_biUnion, MeasureTheory.measure_biUnion, zero_add, VitaliFamily.FineSubfamilyOn.index_countable, VitaliFamily.FineSubfamilyOn.measurableSet_u, VitaliFamily.FineSubfamilyOn.covering_disjoint
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
⊢ LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) s : ENNReal)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
        (μ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑x : X × Set X)) :
      ENNReal)

Tactic:
h.measure_le_tsum_of_absolutelyContinuous Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
s : Set X
hs : s ∈ v.setsAt x
⊢ MeasurableSet s

Tactic:
v.measurableSet _ _ hs

Premises used: VitaliFamily.measurableSet
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} s
⊢ MeasurableSet s

Tactic:
hs.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
s : Set X
hs : s ∈ v.setsAt x
⊢ MeasurableSet s

Tactic:
exacts [v.measurableSet _ _ hs, hs.1]

Premises used: VitaliFamily.measurableSet
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
s : Set X
hs : s ∈ v.setsAt x
⊢ (interior s).Nonempty

Tactic:
v.nonempty_interior _ _ hs

Premises used: VitaliFamily.nonempty_interior
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} s
⊢ (interior s).Nonempty

Tactic:
hs.2.1

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
s : Set X
hs : s ∈ v.setsAt x
⊢ (interior s).Nonempty

Tactic:
exacts [v.nonempty_interior _ _ hs, hs.2.1]

Premises used: VitaliFamily.nonempty_interior
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
ε : ℝ
εpos : ε > 0
rcases :
  ∀ (s : Set X) (hs : s ∈ v.setsAt x) (h's : s ⊆ closedBall x ε),
    ∃ s ∈ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε
⊢ ∃ s ∈ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε

Tactic:
rcases v.nontrivial x ε εpos with ⟨s, hs, h's⟩

Premises used: VitaliFamily.nontrivial
-- Module: Mathlib.MeasureTheory.Covering.VitaliFamily
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
ε : ℝ
εpos : ε > 0
s : Set X
hs : s ∈ v.setsAt x
h's : s ⊆ closedBall x ε
⊢ ∃ s ∈ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε

Tactic:
⟨s, mem_union_left _ hs, h's⟩

Premises used: And.intro, Exists.intro, Set.mem_union_left