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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
hc₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {x : α |
            (fun (x : α) ↦
                ¬((∃ᶠ (a : Set α) in v.filterAt x,
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                        (↑c : ℝ≥0∞)) ∧
                    ∃ᶠ (a : Set α) in v.filterAt x,
                      (↑d : ℝ≥0∞) <
                        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)))
              x}ᶜ
        x →
      ∃ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        {x : α |
            (fun (x : α) ↦
                ¬((∃ᶠ (a : Set α) in v.filterAt x,
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                        (↑c : ℝ≥0∞)) ∧
                    ∃ᶠ (a : Set α) in v.filterAt x,
                      (↑d : ℝ≥0∞) <
                        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)))
              x}ᶜ
        x →
      ∃ᶠ (a : Set α) in v.filterAt x,
        HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
⊢ ∀ᵐ (x : α) ∂μ,
    ¬((∃ᶠ (a : Set α) in v.filterAt x,
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
            (↑c : ℝ≥0∞)) ∧
        ∃ᶠ (a : Set α) in v.filterAt x,
          (↑d : ℝ≥0∞) <
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))

Tactic:
apply v.null_of_frequently_le_of_frequently_ge hρ (ENNReal.coe_lt_coe.1 hcd)

Premises used: ENNReal.coe_lt_coe, VitaliFamily.null_of_frequently_le_of_frequently_ge, Iff.mp
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
hc₁ :
  ∀ (x : α),
    (∃ᶠ (a : Set α) in v.filterAt x,
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
          (↑c : ℝ≥0∞)) →
      (∃ᶠ (x : Set α) in v.filterAt x,
          (↑d : ℝ≥0∞) <
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)) →
        ∃ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ∀ (x : α),
    Membership.mem (γ := Set α)
        {x : α |
            (fun (x : α) ↦
                ¬((∃ᶠ (a : Set α) in v.filterAt x,
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                        (↑c : ℝ≥0∞)) ∧
                    ∃ᶠ (a : Set α) in v.filterAt x,
                      (↑d : ℝ≥0∞) <
                        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)))
              x}ᶜ
        x →
      ∃ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
simp only [and_imp, exists_prop, not_frequently, not_and, not_lt, not_le, not_eventually,
        mem_setOf_eq, mem_compl_iff, not_forall]

Premises used: not_le, and_imp, Set.mem_setOf_eq, exists_prop, not_lt, Filter.not_frequently, Filter.not_eventually, not_and, Classical.not_forall, Set.mem_compl_iff
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h1x :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
hc₁ :
  (∃ᶠ (x : Set α) in v.filterAt x,
      (↑d : ℝ≥0∞) <
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)) →
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ (∃ᶠ (x : Set α) in v.filterAt x,
      (↑d : ℝ≥0∞) <
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)) →
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
_
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h1x :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
apply :
  ∀ (a : Set α)
    (ha :
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
        (↑c : ℝ≥0∞)),
    (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
apply h1x.mono fun a ha => ?_

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 α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h1x :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑c : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
(ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le

Premises used: ENNReal.div_le_iff_le_mul, LT.lt.le, LT.lt.ne', Iff.mp, LE.le.trans_lt, bot_le, Or.inr
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h1x :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑c : ℝ≥0∞)
refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ∨ (↑c : ℝ≥0∞) ≠ ∞
⊢ (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le

Premises used: ENNReal.div_le_iff_le_mul, LT.lt.le, LT.lt.ne', Iff.mp, LE.le.trans_lt, bot_le, Or.inr
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h1x :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑c : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ∨ (↑c : ℝ≥0∞) ≠ ∞

Tactic:
simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]

Premises used: Ne, not_false_iff, or_true, 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 ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
hd₁ :
  ∀ (x : α),
    (∃ᶠ (a : Set α) in v.filterAt x,
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
          (↑c : ℝ≥0∞)) →
      (∃ᶠ (x : Set α) in v.filterAt x,
          (↑d : ℝ≥0∞) <
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)) →
        ∃ᶠ (a : Set α) in v.filterAt x,
          HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
⊢ ∀ (x : α),
    Membership.mem (γ := Set α)
        {x : α |
            (fun (x : α) ↦
                ¬((∃ᶠ (a : Set α) in v.filterAt x,
                      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                        (↑c : ℝ≥0∞)) ∧
                    ∃ᶠ (a : Set α) in v.filterAt x,
                      (↑d : ℝ≥0∞) <
                        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)))
              x}ᶜ
        x →
      ∃ᶠ (a : Set α) in v.filterAt x,
        HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
simp only [and_imp, exists_prop, not_frequently, not_and, not_lt, not_le, not_eventually,
        mem_setOf_eq, mem_compl_iff, not_forall]

Premises used: not_le, and_imp, Set.mem_setOf_eq, exists_prop, not_lt, Filter.not_frequently, Filter.not_eventually, not_and, Classical.not_forall, Set.mem_compl_iff
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
hd₁ :
  (∃ᶠ (a : Set α) in v.filterAt x,
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
        (↑c : ℝ≥0∞)) →
    (∃ᶠ (x : Set α) in v.filterAt x,
        (↑d : ℝ≥0∞) <
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)) →
      ∃ᶠ (a : Set α) in v.filterAt x,
        HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
⊢ (∃ᶠ (a : Set α) in v.filterAt x,
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
        (↑c : ℝ≥0∞)) →
    (∃ᶠ (x : Set α) in v.filterAt x,
        (↑d : ℝ≥0∞) <
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)) →
      ∃ᶠ (a : Set α) in v.filterAt x,
        HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
_
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h2x :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
apply :
  ∀ (a : Set α)
    (ha :
      (↑d : ℝ≥0∞) <
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)),
    HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
apply h2x.mono fun a ha => ?_

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 α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h2x :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
a : Set α
ha :
  (↑d : ℝ≥0∞) <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
ENNReal.mul_le_of_le_div ha.le

Premises used: LT.lt.le, ENNReal.mul_le_of_le_div
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
d : ℝ≥0
hd : (↑d : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)
x : α
h :
  ∃ᶠ (a : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
      (↑c : ℝ≥0∞)
h2x :
  ∃ᶠ (x : Set α) in v.filterAt x,
    (↑d : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
a : Set α
ha :
  (↑d : ℝ≥0∞) <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a

Tactic:
exact ENNReal.mul_le_of_le_div ha.le

Premises used: LT.lt.le, ENNReal.mul_le_of_le_div
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
⊢ ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))

Tactic:
have A : ∀ c ∈ w, ∀ d ∈ w, c < d → ∀ᵐ x ∂μ,
      ¬((∃ᶠ a in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ a in v.filterAt x, d < ρ a / μ a) := by
    intro c hc d hd hcd
    lift c to ℝ≥0 using I c hc
    lift d to ℝ≥0 using I d hd
    apply v.null_of_frequently_le_of_frequently_ge hρ (ENNReal.coe_lt_coe.1 hcd)
    · simp only [and_imp, exists_prop, not_frequently, not_and, not_lt, not_le, not_eventually,
        mem_setOf_eq, mem_compl_iff, not_forall]
      intro x h1x _
      apply h1x.mono fun a ha => ?_
      refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
      simp only [ENNReal.coe_ne_top, Ne, or_true, not_false_iff]
    · simp only [and_imp, exists_prop, not_frequently, not_and, not_lt, not_le, not_eventually,
        mem_setOf_eq, mem_compl_iff, not_forall]
      intro x _ h2x
      apply h2x.mono fun a ha => ?_
      exact ENNReal.mul_le_of_le_div ha.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 ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d →
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))

Tactic:
simpa only [ae_ball_iff w_count, ae_all_iff]

Premises used: MeasureTheory.ae_ball_iff, MeasureTheory.ae_all_iff
-- 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d →
          ¬((∃ᶠ (a : Set α) in v.filterAt x,
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
                  c) ∧
              ∃ᶠ (a : Set α) in v.filterAt x,
                d <
                  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))

Tactic:
have B : ∀ᵐ x ∂μ, ∀ c ∈ w, ∀ d ∈ w, c < d →
      ¬((∃ᶠ a in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ a in v.filterAt x, d < ρ a / μ a) := by
    simpa only [ae_ball_iff w_count, ae_all_iff]