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 ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (↑ε : ℝ≥0∞)⁻¹ * 0 = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) = 0

Tactic:
rw [ρo, mul_zero]

Premises used: MulZeroClass.mul_zero
-- 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 ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α :=
  {x : α |
    ¬∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
hs :
  s =
    {x : α |
      ¬∀ᶠ (a : Set α) in v.filterAt x,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
o : Set α
left : MeasurableSet o
ρo : Eq (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) (0 : ℝ≥0∞)
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o ∪ oᶜ) : ℝ≥0∞)
μ₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) oᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ o)
μ₃ :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ o) = HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
μ₄ :
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ε • μ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞)
μ₅ :
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ o) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞)
μ₆ : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞)⁻¹ ((ρ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) = 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⊥ : ℝ≥0∞)

Tactic:
calc
      μ s ≤ μ (s ∩ o ∪ oᶜ) := by
        conv_lhs => rw [← inter_union_compl s o]
        gcongr
        apply inter_subset_right
      _ ≤ μ (s ∩ o) + μ oᶜ := measure_union_le _ _
      _ = μ (s ∩ o) := by rw [μo, add_zero]
      _ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) := by
        simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
        rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
        gcongr _ * ?_
        refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_
        intro x hx
        rw [hs] at hx
        simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
        exact hx.1
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := by gcongr; apply inter_subset_right
      _ = 0 := by rw [ρo, mul_zero]

Premises used: ENNReal.ofNNReal, 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ρ : ρ ⟂ₘ μ
⊢ ∀ ε > 0,
    ∀ᵐ (x : α) ∂μ,
      ∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
have A : ∀ ε > (0 : ℝ≥0), ∀ᵐ x ∂μ, ∀ᶠ a in v.filterAt x, ρ a < ε * μ a := by
    intro ε εpos
    set s := {x | ¬∀ᶠ a in v.filterAt x, ρ a < ε * μ a} with hs
    change μ s = 0
    obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ oᶜ = 0 := hρ
    apply le_antisymm _ bot_le
    calc
      μ s ≤ μ (s ∩ o ∪ oᶜ) := by
        conv_lhs => rw [← inter_union_compl s o]
        gcongr
        apply inter_subset_right
      _ ≤ μ (s ∩ o) + μ oᶜ := measure_union_le _ _
      _ = μ (s ∩ o) := by rw [μo, add_zero]
      _ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) := by
        simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
        rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
        gcongr _ * ?_
        refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_
        intro x hx
        rw [hs] at hx
        simp only [mem_inter_iff, not_lt, not_eventually, mem_setOf_eq] at hx
        exact hx.1
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := by gcongr; apply inter_subset_right
      _ = 0 := by rw [ρo, mul_zero]
-- 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), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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∞)
obtain :
  ∀ (u : ℕ → ℝ≥0),
    StrictAnti u →
      ∀ (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)),
        ∀ᵐ (x : α) ∂μ,
          Tendsto (β := ℝ≥0∞)
            (fun (a : Set α) ↦
              HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
            (v.filterAt x) (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)

Tactic:
obtain ⟨u, _, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ≥0, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ≥0)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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)
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ (n : ℕ),
      ∀ᶠ (a : Set α) in v.filterAt x,
        (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
have B : ∀ᵐ x ∂μ, ∀ n, ∀ᶠ a in v.filterAt x, ρ a < u n * μ a :=
    ae_all_iff.2 fun n => A (u n) (u_pos n)
-- 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∞)
h :
  ∀ (a : α),
    (∀ (n : ℕ),
        ∀ᶠ (a : Set α) in v.filterAt a,
          (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)) →
      (∀ᶠ (a : Set α) in v.filterAt a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)) →
        Tendsto (β := ℝ≥0∞)
          (fun (a : Set α) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
          (v.filterAt a) (𝓝 0)
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (β := ℝ≥0∞)
      (fun (a : Set α) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
      (v.filterAt x) (𝓝 0)

Tactic:
filter_upwards [B, v.ae_eventually_measure_pos]

Premises used: VitaliFamily.ae_eventually_measure_pos
-- 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∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)

Tactic:
tendsto_order.2 ⟨fun z hz => (ENNReal.not_lt_zero hz).elim, fun z hz => ?_⟩

Premises used: Iff.mpr, False.elim, tendsto_order, ENNReal.not_lt_zero, And.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ρ : ρ ⟂ₘ μ
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∞)
h :
  ∀ (z : ℝ≥0∞) (hz : z > 0),
    ∀ᶠ (b : Set α) in v.filterAt x,
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) < z
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : Set α) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞))
    (v.filterAt x) (𝓝 0)

Tactic:
refine tendsto_order.2 ⟨fun z hz => (ENNReal.not_lt_zero hz).elim, fun z hz => ?_⟩

Premises used: Iff.mpr, False.elim, tendsto_order, ENNReal.not_lt_zero, And.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ρ : ρ ⟂ₘ μ
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), 0 < (↑w : ℝ≥0∞) ∧ (↑w : ℝ≥0∞) < z

Tactic:
ENNReal.lt_iff_exists_nnreal_btwn.1 hz

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
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
h :
  ∀ (w : ℝ≥0) (w_pos : 0 < (↑w : ℝ≥0∞)) (w_lt : (↑w : ℝ≥0∞) < z),
    ∀ᶠ (b : Set α) in v.filterAt x,
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) < z
⊢ ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) < z

Tactic:
obtain ⟨w, w_pos, w_lt⟩ : ∃ w : ℝ≥0, (0 : ℝ≥0∞) < w ∧ (w : ℝ≥0∞) < z :=
    ENNReal.lt_iff_exists_nnreal_btwn.1 hz

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp, OfNat.ofNat
-- 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 : ℕ), u n < w

Tactic:
((tendsto_order.1 u_lim).2 w (ENNReal.coe_pos.1 w_pos)).exists

Premises used: tendsto_order, Filter.Eventually.exists, ENNReal.coe_pos, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
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
h :
  ∀ (n : ℕ) (hn : u n < w),
    ∀ᶠ (b : Set α) in v.filterAt x,
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) < z
⊢ ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) < z

Tactic:
obtain ⟨n, hn⟩ : ∃ n, u n < w := ((tendsto_order.1 u_lim).2 w (ENNReal.coe_pos.1 w_pos)).exists

Premises used: tendsto_order, Filter.Eventually.exists, ENNReal.coe_pos, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
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
h :
  ∀ (a : Set α),
    (ρ : (a : Set α) → ℝ≥0∞) a < HMul.hMul (β := ℝ≥0∞) (↑(u n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) →
      LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞) →
          HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) < z
⊢ ∀ᶠ (b : Set α) in v.filterAt x,
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) b : ℝ≥0∞) < z

Tactic:
filter_upwards [hx n, h'x, v.eventually_measure_lt_top x]

Premises used: VitaliFamily.eventually_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ρ : ρ ⟂ₘ μ
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∞)
h :
  HMul.hMul (β := ℝ≥0∞) (↑w : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) z ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) < z

Tactic:
grw [ENNReal.div_lt_iff (.inl μa_pos.ne') (.inl μa_lt_top.ne), ha, hn]

Premises used: LT.lt.ne', Or.inl, ENNReal.div_lt_iff, 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∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑w : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) z ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
gcongr