awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
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∞)
have 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 α)))
Tactic: rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
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∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (↑ε : ℝ≥0∞)
have ρ₁ : 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: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
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 μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ
have rcases : ∀ (w : Set α) (w_nhds : w ∈ 𝓝 x) (hw : IntegrableOn f w μ), ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ
Tactic: rcases hf x with ⟨w, w_nhds, hw⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
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 α) in v.filterAt x, IntegrableOn f a μ
have h : ∀ (a : Set α) (ha : a ⊆ w), IntegrableOn f a μ
Tactic: filter_upwards [v.eventually_filterAt_subset_of_nhds w_nhds] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have hs : let s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)};
s =
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
Tactic: set s := {x | ¬∀ᶠ a in v.filterAt x, ρ a < ε * μ a} with hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have change : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: change μ s = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (o : Set α),
  MeasurableSet o →
    ∀ (ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞))
      (μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ oᶜ = 0 := hρ
Cleared hypotheses: hρ
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊥ : ℝ≥0∞)
Tactic: apply le_antisymm _ bot_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
| ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ s ∩ oᶜ) : ℝ≥0∞)
Tactic: rw [← inter_union_compl s o]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)
have conv_lhs : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ s ∩ oᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)
Tactic: conv_lhs => rw [← inter_union_compl s o]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ s ∩ oᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)
have h : s ∩ oᶜ ⊆ oᶜ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ o)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞) =
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ o)
Tactic: rw [μo, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ o)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ o)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
Tactic: rw [μo, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) = HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
have simp : (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
  HMul.hMul (β := ℝ≥0∞) ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
Tactic: simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
    HMul.hMul (β := ℝ≥0∞) ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
have rw : (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
Tactic: rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
    HMul.hMul (β := ℝ≥0∞) ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
Tactic: rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
have bc : LE.le (α := ℝ≥0∞) ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
Tactic: gcongr _ * ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
have bc : ∀ x ∈ s ∩ o,
  ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) (((↑ε : ℝ≥0∞) • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx :
  x ∈
    {x : α |
        ¬∀ᶠ (a : Set α) in v.filterAt x,
            (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)} ∩
      o
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) (((↑ε : ℝ≥0∞) • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have hx₁ : (∃ᶠ (x : Set α) in v.filterAt x,
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) x) ∧
  x ∈ o
Tactic: simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞)
have bc : s ∩ o ⊆ o
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) = 0
have rw : (↑ε : ℝ≥0∞)⁻¹ * 0 = 0
Tactic: rw [ρo, mul_zero]