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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_

Premises used: VitaliFamily.measure_le_of_frequently_le, 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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  ∀ (x : α) (hx : x ∈ s ∩ t),
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_

Premises used: VitaliFamily.measure_le_of_frequently_le, 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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
⊢ ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) <
      (↑p : ℝ≥0∞)

Tactic:
have I : ∀ᶠ b : Set α in v.filterAt x, ρ b / μ b < p := (tendsto_order.1 hx.2).2 _ (h hx.1)
-- 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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) <
      (↑p : ℝ≥0∞)
apply :
  ∀ (a : Set α)
    (ha :
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
        (↑p : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

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

Premises used: Filter.Frequently.mono, Filter.Eventually.frequently
-- 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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) <
      (↑p : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑p : ℝ≥0∞)
rw : (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
rw [coe_nnreal_smul_apply]

Premises used: MeasureTheory.Measure.coe_nnreal_smul_apply
-- 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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) <
      (↑p : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑p : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) <
      (↑p : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑p : ℝ≥0∞)
refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ∨ (↑p : ℝ≥0∞) ≠ ∞
⊢ (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥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ρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x : α | v.limRatioMeas hρ x < (↑p : ℝ≥0∞)}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
I :
  ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) <
      (↑p : ℝ≥0∞)
a : Set α
ha :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    (↑p : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ∨ (↑p : ℝ≥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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have A : μ tᶜ = 0 := v.ae_tendsto_limRatioMeas 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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw rw₁ : Eq (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)

Tactic:
rw [inter_union_compl]

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 ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ (q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥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 ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
h₂ : s ∩ tᶜ ⊆ tᶜ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ s ∩ tᶜ ⊆ tᶜ

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 ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) =
    (ρ : (a : Set α) → ℝ≥0∞) (s ∩ t)

Tactic:
simp [A]
-- 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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
h₁ : s ∩ t ⊆ s
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ s ∩ t ⊆ s

Tactic:
apply inter_subset_left

Premises used: Set.inter_subset_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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
H : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
s₁ : Eq (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
s₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
s₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) =
    (ρ : (a : Set α) → ℝ≥0∞) (s ∩ t)
s₄ : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s

Tactic:
calc
    (q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ (q • μ) (s ∩ t) + (q • μ) (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ ρ (s ∩ t) + (q • μ) tᶜ := by gcongr; apply inter_subset_right
    _ = ρ (s ∩ t) := by simp [A]
    _ ≤ ρ s := by gcongr; apply inter_subset_left

Premises used: Compl.compl, Inter.inter, HSMul.hSMul, Union.union, DFunLike.coe, 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 ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
suffices : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s

Tactic:
suffices H : (q • μ) (s ∩ t) ≤ ρ (s ∩ t) by calc
    (q • μ) s = (q • μ) (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ (q • μ) (s ∩ t) + (q • μ) (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ ρ (s ∩ t) + (q • μ) tᶜ := by gcongr; apply inter_subset_right
    _ = ρ (s ∩ t) := by simp [A]
    _ ≤ ρ s := by gcongr; apply inter_subset_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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- 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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  ∀ x ∈ s ∩ t,
    ∃ᶠ (a : Set α) in v.filterAt x,
      LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)

Tactic:
refine v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, VitaliFamily.measure_le_of_frequently_le, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- 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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
t : Set α :=
  {x : α |
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
⊢ ∀ᶠ (a : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
have I : ∀ᶠ a in v.filterAt x, (q : ℝ≥0∞) < ρ a / μ a := (tendsto_order.1 hx.2).1 _ (h hx.1)