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ρ : ρ ≪ μ
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∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have 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∞)
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
-- 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∞)
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∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have s₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) =
  (ρ : (a : Set α) → ℝ≥0∞) (s ∩ t)
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
-- 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∞)
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)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have s₄ : LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥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
-- 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∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have suffices : LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
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
-- 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∞)
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
have refine : ∀ x ∈ s ∩ t,
  ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: refine v.measure_le_of_frequently_le _ (.smul_left .rfl _) _ ?_
-- 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))}
A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s ∩ t
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have I : ∀ᶠ (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)
-- 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∞)
x : α
hx : x ∈ s ∩ t
I :
  ∀ᶠ (a : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ ∃ᶠ (a : Set α) in v.filterAt x,
    LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have apply : ∀ (a : Set α)
  (ha :
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (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ρ : ρ ≪ μ
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
I :
  ∀ᶠ (a : Set α) in v.filterAt x,
    (↑q : ℝ≥0∞) <
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
a : Set α
ha :
  (↑q : ℝ≥0∞) <
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((q • μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) a
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ρ : ρ ≪ μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | v.limRatioMeas hρ x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : ∀ (x : α),
  Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x →
    ∃ u ∈ 𝓝[{x : α | v.limRatioMeas hρ x = ∞}] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine measure_null_of_locally_null _ fun x _ => ?_
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
⊢ ∃ u ∈ 𝓝[{x : α | v.limRatioMeas hρ x = ∞}] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
have obtain : ∀ (o : Set α) (xo : x ∈ o) (o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o)
  (μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∃ u ∈ 𝓝[{x : α | v.limRatioMeas hρ x = ∞}] 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
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
⊢ ∃ u ∈ 𝓝[{x : α | v.limRatioMeas hρ x = ∞}] x, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨s, inter_mem_nhdsWithin _ (o_open.mem_nhds xo), le_antisymm ?_ bot_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ρ : ρ ≪ μ
x : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have ρs : ρ s ≠ ∞ := measure_ne_top_of_subset inter_subset_right μo.ne
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 1 ≤ q
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
Tactic: rw [mul_comm, ← div_eq_mul_inv, ENNReal.le_div_iff_mul_le _ (Or.inr ρs), mul_comm]
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 1 ≤ q
rw : HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : (↑q : ℝ≥0∞) ≠ 0 ∨ Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mul_comm, ← div_eq_mul_inv, ENNReal.le_div_iff_mul_le _ (Or.inr ρs), mul_comm]
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 1 ≤ q
⊢ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ (ρ : (a : Set α) → ℝ≥0∞) s
have apply : s ⊆ {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x}
Tactic: apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
-- 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ρ : ρ ≪ μ
x : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
q : ℝ≥0
hq : 1 ≤ q
y : α
hy : y ∈ s
⊢ Membership.mem (γ := Set α) {x : α | (↑q : ℝ≥0∞) < v.limRatioMeas hρ x} y
have this : v.limRatioMeas hρ y = ∞
Tactic: have : v.limRatioMeas hρ y = ∞ := hy.1
-- 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ρ : ρ ≪ μ
x : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have A : ∀ (q : ℝ≥0),
  1 ≤ q → (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: have A : ∀ q : ℝ≥0, 1 ≤ q → μ s ≤ (q : ℝ≥0∞)⁻¹ * ρ s := by
    intro q hq
    rw [mul_comm, ← div_eq_mul_inv, ENNReal.le_div_iff_mul_le _ (Or.inr ρs), mul_comm]
    · apply v.mul_measure_le_of_subset_lt_limRatioMeas hρ
      intro y hy
      have : v.limRatioMeas hρ y = ∞ := hy.1
      simp only [this, ENNReal.coe_lt_top, mem_setOf_eq]
    · simp only [(zero_lt_one.trans_le hq).ne', true_or, ENNReal.coe_eq_zero, Ne,
        not_false_iff]
-- 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 : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    1 ≤ q → (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Tendsto (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞⁻¹ : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have apply : Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)⁻¹) atTop (𝓝 ∞⁻¹)
Tactic: apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)
-- 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ρ : ρ ≪ μ
x : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    1 ≤ q → (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have B : Tendsto (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
  (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞⁻¹ : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
Tactic: have B : Tendsto (fun q : ℝ≥0 => (q : ℝ≥0∞)⁻¹ * ρ s) atTop (𝓝 (∞⁻¹ * ρ s)) := by
    apply ENNReal.Tendsto.mul_const _ (Or.inr ρs)
    exact tendsto_inv_iff.2 (ENNReal.tendsto_coe_nhds_top.2 tendsto_id)
-- 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ρ : ρ ≪ μ
x : α
h : Membership.mem (γ := Set α) {x : α | v.limRatioMeas hρ x = ∞} x
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : LT.lt (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α := {x : α | v.limRatioMeas hρ x = ∞} ∩ o
ρs : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  ∀ (q : ℝ≥0),
    1 ≤ q → (μ : (a : Set α) → ℝ≥0∞) s ≤ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
B :
  Tendsto (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞⁻¹ : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have B₁ : Tendsto (β := ℝ≥0∞) (fun (q : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (↑q : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
  (𝓝 0)
Tactic: simp only [zero_mul, ENNReal.inv_top] at B
Cleared hypotheses: B