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ρ : ρ ⟂ₘ μ
A :
  ∀ ε > 0,
    ∀ᵐ (x : α) ∂μ,
      ∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
x : α
hx :
  ∀ (n : ℕ),
    ∀ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < (↑w : ℝ≥0∞)
w_lt : (↑w : ℝ≥0∞) < z
n : ℕ
hn : u n < w
a : Set α
ha : (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
μa_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
μa_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
μa_lt_top.ne

Premises used: LT.lt.ne
-- 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ρ : ρ ⟂ₘ μ
A :
  ∀ ε > 0,
    ∀ᵐ (x : α) ∂μ,
      ∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
x : α
hx :
  ∀ (n : ℕ),
    ∀ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h'x : ∀ᶠ (a : Set α) in v.filterAt x, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
z : ℝ≥0∞
hz : z > 0
w : ℝ≥0
w_pos : 0 < (↑w : ℝ≥0∞)
w_lt : (↑w : ℝ≥0∞) < z
n : ℕ
hn : u n < w
a : Set α
ha : (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
μa_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
μa_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact μa_lt_top.ne

Premises used: LT.lt.ne
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
apply : ∀ x ∈ s, ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_null_of_locally_null s fun x _ => ?_

Premises used: MeasureTheory.measure_null_of_locally_null
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h : x ∈ s
⊢ ∃ (o : Set α),
    x ∈ o ∧
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Measure.exists_isOpen_measure_lt_top μ x

Premises used: MeasureTheory.Measure.exists_isOpen_measure_lt_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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h : x ∈ s
obtain :
  ∀ (o : Set α) (xo : x ∈ o) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o)
    (μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨o, xo, o_open, μo⟩ : ∃ o : Set α, x ∈ o ∧ IsOpen o ∧ μ o < ∞ :=
    Measure.exists_isOpen_measure_lt_top μ x

Premises used: MeasureTheory.Measure.exists_isOpen_measure_lt_top, 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 ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨s ∩ o, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), ?_⟩

Premises used: inter_mem_nhdsWithin, Inter.inter, And.intro, IsOpen.mem_nhds, Exists.intro
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ u ∈ 𝓝[s] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨s ∩ o, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), ?_⟩
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
by_contra : ∀ (h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_contra h
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
apply : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
⊢ False

Tactic:
apply lt_irrefl (ρ s')

Premises used: lt_irrefl, 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s' ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)

Tactic:
v.measure_le_of_frequently_le (c • μ) hρ s' fun x hx => hc x hx.1

Premises used: VitaliFamily.measure_le_of_frequently_le, And.left, HSMul.hSMul
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
hinf : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥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 ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top_of_subset inter_subset_right μo.ne

Premises used: MeasureTheory.measure_ne_top_of_subset, Set.inter_subset_right, LT.lt.ne
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top_of_subset inter_subset_right μo.ne

Premises used: MeasureTheory.measure_ne_top_of_subset, Set.inter_subset_right, LT.lt.ne
-- 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ρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s'

Tactic:
v.measure_le_of_frequently_le ρ smul_absolutelyContinuous s' fun x hx ↦ hd x hx.1

Premises used: VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.smul_absolutelyContinuous, 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 ρ
hρ : ρ ≪ μ
c d : ℝ≥0
hcd : c < d
s : Set α
hc :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
hd :
  ∀ x ∈ s,
    ∃ᶠ (a : Set α) in v.filterAt x,
      HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
x : α
h_1 : x ∈ s
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s' : Set α := s ∩ o
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) (0 : ℝ≥0∞)
ρ₁ :
  HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) (↑d : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)

Tactic:
calc
    ρ s' ≤ c * μ s' := v.measure_le_of_frequently_le (c • μ) hρ s' fun x hx => hc x hx.1
    _ < d * μ s' := by gcongr; exact measure_ne_top_of_subset inter_subset_right μo.ne
    _ ≤ ρ s' := v.measure_le_of_frequently_le ρ smul_absolutelyContinuous s' fun x hx ↦ hd x hx.1

Premises used: VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.smul_absolutelyContinuous, And.left, HSMul.hSMul, 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ρ : ρ ≪ μ
⊢ ∃ (w : Set ℝ≥0∞), w.Countable ∧ Dense w ∧ 0 ∉ w ∧ ∞ ∉ w

Tactic:
ENNReal.exists_countable_dense_no_zero_top

Premises used: ENNReal.exists_countable_dense_no_zero_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ρ : ρ ≪ μ
obtain :
  ∀ (w : Set ℝ≥0∞) (w_count : w.Countable) (w_dense : Dense w),
    0 ∉ w →
      ∀ (w_top : ∞ ∉ w),
        ∀ᵐ (x : α) ∂μ,
          ∃ (c : ℝ≥0∞),
            Tendsto
              (fun (a : Set α) ↦
                HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
                  ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
              (v.filterAt x) (𝓝 c)
⊢ ∀ᵐ (x : α) ∂μ,
    ∃ (c : ℝ≥0∞),
      Tendsto
        (fun (a : Set α) ↦
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
        (v.filterAt x) (𝓝 c)

Tactic:
obtain ⟨w, w_count, w_dense, _, w_top⟩ :
    ∃ w : Set ℝ≥0∞, w.Countable ∧ Dense w ∧ 0 ∉ w ∧ ∞ ∉ w :=
    ENNReal.exists_countable_dense_no_zero_top

Premises used: ENNReal, ENNReal.exists_countable_dense_no_zero_top, 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 ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left : 0 ∉ w
w_top : ∞ ∉ w
⊢ ∀ x ∈ w, x ≠ ∞

Tactic:
have I : ∀ x ∈ w, x ≠ ∞ := fun x xs hx => w_top (hx ▸ xs)
-- 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 ∈ w
d : ℝ≥0∞
hd : d ∈ w
hcd : c < d
⊢ c ≠ ∞

Tactic:
I c hc
-- 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 ∈ w
d : ℝ≥0∞
hd : d ∈ w
hcd : c < d
lift :
  ∀ (c : ℝ≥0) (hc : (↑c : ℝ≥0∞) ∈ w) (hcd : (↑c : ℝ≥0∞) < d),
    ∀ᵐ (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 <
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
⊢ ∀ᵐ (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:
lift c to ℝ≥0 using I c hc
-- 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 ≠ ∞
d : ℝ≥0∞
hd : d ∈ w
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < d
⊢ d ≠ ∞

Tactic:
I d hd
-- 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 ≠ ∞
d : ℝ≥0∞
hd : d ∈ w
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ∈ w
hcd : (↑c : ℝ≥0∞) < d
lift :
  ∀ (d : ℝ≥0) (hd : (↑d : ℝ≥0∞) ∈ w) (hcd : (↑c : ℝ≥0∞) < (↑d : ℝ≥0∞)),
    ∀ᵐ (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 : α) ∂μ,
    ¬((∃ᶠ (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 < HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))

Tactic:
lift d to ℝ≥0 using I d hd