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 α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
ε : ℝ≥0
εpos : ε > 0
⊢ 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
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)}
change : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
change μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)}
⊢ ∃ (o : Set α),
    MeasurableSet o ∧
      Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞) ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hρ

Premises used: MeasureTheory.Measure.MutuallySingular
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)}
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ oᶜ = 0 := hρ

Premises used: Set
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊥ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply le_antisymm _ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 ∪ s ∩ oᶜ) : ℝ≥0∞)
| ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← inter_union_compl s o]

Premises used: Set.inter_union_compl
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
conv_lhs :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ s ∩ oᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)

Tactic:
conv_lhs => rw [← inter_union_compl s o]

Premises used: Set.inter_union_compl
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
h : s ∩ oᶜ ⊆ oᶜ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ s ∩ oᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
⊢ s ∩ oᶜ ⊆ oᶜ

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 ∪ oᶜ) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞)

Tactic:
measure_union_le _ _

Premises used: MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ o)

Tactic:
rw [μo, add_zero]

Premises used: add_zero
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
simp :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
    HMul.hMul (β := ℝ≥0∞) ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) = HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)

Tactic:
simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.coe_nnreal_smul_apply, mul_assoc, mul_comm
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) =
    HMul.hMul (β := ℝ≥0∞) ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥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]

Premises used: Iff.mpr, LT.lt.ne', ENNReal.coe_pos, ENNReal.mul_inv_cancel, one_mul, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
bc : LE.le (α := ℝ≥0∞) ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)

Tactic:
gcongr _ * ?_
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)

Tactic:
v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_

Premises used: VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
bc :
  ∀ x ∈ s ∩ o,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) (((↑ε : ℝ≥0∞) • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)

Tactic:
refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_

Premises used: VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 ∈ s ∩ o
⊢ x ∈
    {x : α |
        ¬∀ᶠ (a : Set α) in v.filterAt x,
            (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)} ∩
      o

Tactic:
rw [hs] at hx
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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
⊢ (∃ᶠ (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

Premises used: Set.mem_inter_iff, Set.mem_setOf_eq, not_lt, Filter.not_eventually
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) x) ∧
    x ∈ o
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) (((↑ε : ℝ≥0∞) • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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 : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) x) ∧
    x ∈ o
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) (((↑ε : ℝ≥0∞) • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
bc : s ∩ o ⊆ o
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
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∞)
⊢ s ∩ o ⊆ o

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right