awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx :
  Tendsto
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 (v.limRatio ρ x))
h'x : v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ 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))
have h : ∀
  (hx :
    Tendsto
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 (AEMeasurable.mk (v.limRatio ρ) sorry x)))
  (h'x : v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) sorry 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))
Tactic: rwa [h'x] at hx
Cleared hypotheses: hx, h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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 : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have A : μ tᶜ = 0 := v.ae_tendsto_limRatioMeas hρ
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [inter_union_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₂ : s ∩ tᶜ ⊆ tᶜ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have bc : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have ρ₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
Tactic: calc
    ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
    _ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
    _ ≤ p * μ s := by gcongr; apply inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
ρ₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have ρ₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
Tactic: calc
    ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
    _ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
    _ ≤ p * μ s := by gcongr; apply inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
ρ₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
ρ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have ρ₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: calc
    ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
    _ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
    _ ≤ p * μ s := by gcongr; apply inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
H : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
ρ₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
ρ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
ρ₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have ρ₄ : HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ≤
  HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: calc
    ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
    _ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
    _ ≤ p * μ s := by gcongr; apply inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have suffices : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: suffices H : ρ (s ∩ t) ≤ (p • μ) (s ∩ t) by calc
    ρ s = ρ (s ∩ t ∪ s ∩ tᶜ) := by rw [inter_union_compl]
    _ ≤ ρ (s ∩ t) + ρ (s ∩ tᶜ) := measure_union_le _ _
    _ ≤ (p • μ) (s ∩ t) + ρ tᶜ := by gcongr; apply inter_subset_right
    _ ≤ p * μ (s ∩ t) := by simp [(hρ A)]
    _ ≤ p * μ s := by gcongr; apply inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
have 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∞)
Tactic: refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have I : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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 α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have 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∞)
Tactic: apply I.frequently.mono fun a ha => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((p • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have rw : (ρ : (a : Set α) → ℝ≥0∞) a ≤ HMul.hMul (β := ℝ≥0∞) (↑p : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: rw [coe_nnreal_smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞)
have refine : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ∨ (↑p : ℝ≥0∞) ≠ ∞
Tactic: refine (ENNReal.div_le_iff_le_mul ?_ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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))}
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have A : μ tᶜ = 0 := v.ae_tendsto_limRatioMeas hρ
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
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∞)
⊢ Eq (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [inter_union_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
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∞) ((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∞)
have h₂ : s ∩ tᶜ ⊆ tᶜ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
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∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : s ∩ t ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Differentiation (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
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∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have s₁ : Eq (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
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