awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
s : Set α := {x : α | ¬∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs : s = {x : α | ∃ᶠ (x : Set α) in v.filterAt x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)}
f : α → Set (Set α) := fun (x : α) ↦ {a : Set α | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)}
h : v.FineSubfamilyOn f s
μ₁ :
  Eq (α := ℝ≥0∞)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (μ : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)))
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)), 0)
μ₂ : Eq (α := ℝ≥0∞) (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)), 0) 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
calc
    μ s ≤ ∑' x : h.index, μ (h.covering x) := h.measure_le_tsum
    _ = ∑' x : h.index, 0 := by congr; ext1 x; exact h.covering_mem x.2
    _ = 0 := by simp only [tsum_zero]

Premises used: VitaliFamily.FineSubfamilyOn.measure_le_tsum, VitaliFamily.FineSubfamilyOn.index, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : IsLocallyFiniteMeasure μ
x : α
⊢ ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(μ.finiteAt_nhds x).eventually.filter_mono inf_le_left

Premises used: MeasureTheory.Measure.finiteAt_nhds, Filter.Eventually.filter_mono, MeasureTheory.Measure.FiniteAtFilter.eventually, inf_le_left, VitaliFamily.filterAt
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
apply :
  ∀ (ε : ℝ≥0) (εpos : 0 < ε),
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      (ρ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply ENNReal.le_of_forall_pos_le_add fun ε εpos _ => ?_

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (U : Set α),
    s ⊆ U ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U ∧
        (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
exists_isOpen_le_add s ν (ENNReal.coe_pos.2 εpos).ne'

Premises used: Iff.mpr, LT.lt.ne', ENNReal.coe_pos, Set.exists_isOpen_le_add
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
obtain :
  ∀ (U : Set α) (sU : s ⊆ U) (U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)
    (νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)),
    (ρ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨U, sU, U_open, νU⟩ : ∃ (U : Set α), s ⊆ U ∧ IsOpen U ∧ ν U ≤ ν s + ε :=
    exists_isOpen_le_add s ν (ENNReal.coe_pos.2 εpos).ne'

Premises used: Iff.mpr, LT.lt.ne', ENNReal.coe_pos, Set.exists_isOpen_le_add, DFunLike.coe, Set
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
apply : ∀ (x : α) (hx : x ∈ s), ∃ᶠ (t : Set α) in v.filterAt x, t ∈ f x
⊢ v.FineSubfamilyOn f s

Tactic:
apply v.fineSubfamilyOn_of_frequently f s fun x hx => ?_

Premises used: VitaliFamily.fineSubfamilyOn_of_frequently
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
x : α
hx : x ∈ s
⊢ ∃ᶠ (x_1 : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ∧
      x_1 ∈ v.setsAt x ∧ x_1 ⊆ U

Tactic:
have :=
      (hs x hx).and_eventually
        ((v.eventually_filterAt_mem_setsAt x).and
          (v.eventually_filterAt_subset_of_nhds (U_open.mem_nhds (sU hx))))
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
x : α
hx : x ∈ s
this :
  ∃ᶠ (x_1 : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ∧
      x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
apply :
  ∀ (x_1 : Set α),
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ∧
        x_1 ∈ v.setsAt x ∧ x_1 ⊆ U →
      x_1 ∈ f x
⊢ ∃ᶠ (t : Set α) in v.filterAt x, t ∈ f x

Tactic:
apply Frequently.mono this

Premises used: Filter.Frequently.mono
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
x : α
hx : x ∈ s
this :
  ∃ᶠ (x_1 : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ∧
      x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
a : Set α
ρa : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
left : a ∈ v.setsAt x
aU : a ⊆ U
⊢ a ∈ f x

Tactic:
⟨ρa, aU⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
x : α
hx : x ∈ s
this :
  ∃ᶠ (x_1 : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) x_1 : ℝ≥0∞) ∧
      x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
a : Set α
ρa : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
left : a ∈ v.setsAt x
aU : a ⊆ U
⊢ a ∈ f x

Tactic:
exact ⟨ρa, aU⟩
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
⊢ v.FineSubfamilyOn f s

Tactic:
have h : v.FineSubfamilyOn f s := by
    apply v.fineSubfamilyOn_of_frequently f s fun x hx => ?_
    have :=
      (hs x hx).and_eventually
        ((v.eventually_filterAt_mem_setsAt x).and
          (v.eventually_filterAt_subset_of_nhds (U_open.mem_nhds (sU hx))))
    apply Frequently.mono this
    rintro a ⟨ρa, _, aU⟩
    exact ⟨ρa, aU⟩
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
haveI :
  ∀ (this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)),
    (ρ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
haveI : Encodable h.index := h.index_countable.toEncodable
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
        (ρ : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)) :
      ℝ≥0∞)

Tactic:
h.measure_le_tsum_of_absolutelyContinuous hρ

Premises used: VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)
⊢ LE.le (α := ℝ≥0∞)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)))
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ν : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)))

Tactic:
ENNReal.tsum_le_tsum fun x => (h.covering_mem x.2).1

Premises used: ENNReal.tsum_le_tsum, VitaliFamily.FineSubfamilyOn.covering_mem, And.left, Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)
rw rw₁ :
  Eq (α := ℝ≥0∞)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ν : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)))
    (∑' (i : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ν : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑i : α × Set α)))
⊢ Eq (α := ℝ≥0∞)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
        (ν : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(h.index (f := f) (s := s)) : Type u_1)), h.covering (f := f) (s := s) (↑x : α × Set α)) :
      ℝ≥0∞)

Tactic:
rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]

Premises used: MeasureTheory.measure_iUnion, VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype, VitaliFamily.FineSubfamilyOn.measurableSet_u, Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)
⊢ LE.le (α := ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(h.index (f := f) (s := s)) : Type u_1)), h.covering (f := f) (s := s) (↑x : α × Set α)) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
(measure_mono (iUnion_subset fun i => (h.covering_mem i.2).2))

Premises used: Set.iUnion_subset, VitaliFamily.FineSubfamilyOn.covering_mem, And.right, MeasureTheory.measure_mono, Subtype.property
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)
⊢ (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
νU
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
ρ ν : Measure α
inst_3 : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
ε : ℝ≥0
εpos : 0 < ε
h_1 : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
U : Set α
sU : s ⊆ U
U_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
νU : (ν : (a : Set α) → ℝ≥0∞) U ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
f : α → Set (Set α) :=
  fun (x : α) ↦
    {a : Set α | LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable (↑(h.index (f := f) (s := s)) : Type u_1)
ρ₁ :
  Eq (α := ℝ≥0∞)
    (∑' (x : (↑(h.index (f := f) (s := s)) : Type u_1)),
        (ν : (a : Set α) → ℝ≥0∞) (h.covering (f := f) (s := s) (↑x : α × Set α)) :
      ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞)
        (⋃ (x : (↑(h.index (f := f) (s := s)) : Type u_1)), h.covering (f := f) (s := s) (↑x : α × Set α)) :
      ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)

Tactic:
calc
    ρ s ≤ ∑' x : h.index, ρ (h.covering x) := h.measure_le_tsum_of_absolutelyContinuous hρ
    _ ≤ ∑' x : h.index, ν (h.covering x) := ENNReal.tsum_le_tsum fun x => (h.covering_mem x.2).1
    _ = ν (⋃ x : h.index, h.covering x) := by
      rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]
    _ ≤ ν U := (measure_mono (iUnion_subset fun i => (h.covering_mem i.2).2))
    _ ≤ ν s + ε := νU

Premises used: VitaliFamily.FineSubfamilyOn.covering, ENNReal.tsum_le_tsum, Set.iUnion_subset, VitaliFamily.FineSubfamilyOn.covering_mem, And.right, And.left, MeasureTheory.measure_mono, VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous, Subtype.val, VitaliFamily.FineSubfamilyOn.index, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
rcases : ∀ (w : Set α) (w_nhds : w ∈ 𝓝 x) (hw : IntegrableOn f w μ), ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ

Tactic:
rcases hf x with ⟨w, w_nhds, hw⟩
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
h : ∀ (a : Set α) (ha : a ⊆ w), IntegrableOn f a μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ

Tactic:
filter_upwards [v.eventually_filterAt_subset_of_nhds w_nhds] with a ha

Premises used: VitaliFamily.eventually_filterAt_subset_of_nhds
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
a : Set α
ha : a ⊆ w
⊢ IntegrableOn f a μ

Tactic:
hw.mono_set ha

Premises used: MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst_1 : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
a : Set α
ha : a ⊆ w
⊢ IntegrableOn f a μ

Tactic:
exact hw.mono_set ha

Premises used: MeasureTheory.IntegrableOn.mono_set