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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
C :
  ∀ (n : ℤ),
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
      ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1)))

Tactic:
(add_le_add (add_le_add A B) (ENNReal.tsum_le_tsum C))

Premises used: ENNReal.tsum_le_tsum, add_le_add
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
C :
  ∀ (n : ℤ),
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
      ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
        ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞) +
      ∑' (n : ℤ), (t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) =
    (t • ν : (a : Set α) → ℝ≥0∞) s

Tactic:
(measure_eq_measure_preimage_add_measure_tsum_Ico_zpow (t • ν) f_meas hs ht).symm

Premises used: measure_eq_measure_preimage_add_measure_tsum_Ico_zpow, HSMul.hSMul, Eq.symm
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : (↑t : ℝ≥0∞) ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {0}) : ℝ≥0∞)
B :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
    ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' {∞}) : ℝ≥0∞)
C :
  ∀ (n : ℤ),
    LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
      ((t • ν : (a : Set α) → ℝ≥0∞) (s ∩ f ⁻¹' Ico ((↑t : ℝ≥0∞) ^ n) ((↑t : ℝ≥0∞) ^ (n + 1))) : ℝ≥0∞)
⊢ (ρ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    ρ s =
      ρ (s ∩ f ⁻¹' {0}) + ρ (s ∩ f ⁻¹' {∞}) +
        ∑' n : ℤ, ρ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
      measure_eq_measure_preimage_add_measure_tsum_Ico_zpow ρ f_meas hs ht
    _ ≤
        (t • ν) (s ∩ f ⁻¹' {0}) + (t • ν) (s ∩ f ⁻¹' {∞}) +
          ∑' n : ℤ, (t • ν) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
      (add_le_add (add_le_add A B) (ENNReal.tsum_le_tsum C))
    _ = (t • ν) s :=
      (measure_eq_measure_preimage_add_measure_tsum_Ico_zpow (t • ν) f_meas hs ht).symm

Premises used: ENNReal.tsum_le_tsum, add_le_add, Inter.inter, Set.preimage, measure_eq_measure_preimage_add_measure_tsum_Ico_zpow, HSMul.hSMul, Top.top, Singleton.singleton, OfNat.ofNat, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Covering.Differentiation
Goal:
α : Type u_1
inst : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst_1 : SecondCountableTopology α
inst_2 : BorelSpace α
inst_3 : IsLocallyFiniteMeasure μ
ρ : Measure α
inst_4 : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.withDensity (v.limRatioMeas hρ) = ρ

Tactic:
ext1 s hs
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
h :
  LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_

Premises used: ENNReal.Tendsto.mul, tendsto_const_nhds
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
refine_1 : Tendsto (fun (t : ℝ≥0) ↦ HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) (𝓝[>] 1) (𝓝 (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2))
refine_2 : HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ 0 ∨ Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 : Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ ∞
⊢ Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_

Premises used: ENNReal.Tendsto.mul, tendsto_const_nhds
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun (t : ℝ≥0) ↦ HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) (𝓝[>] 1) (𝓝 (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2))

Tactic:
ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)

Premises used: Iff.mpr, ENNReal.Tendsto.pow, ENNReal.tendsto_coe, nhdsWithin_le_nhds
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun (t : ℝ≥0) ↦ HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) (𝓝[>] 1) (𝓝 (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2))

Tactic:
exact ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ 0 ∨ Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Ne (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨ HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2 ≠ ∞

Tactic:
simp only [one_pow, Ne, or_true, ENNReal.one_ne_top, not_false_iff]

Premises used: one_pow, Ne, not_false_iff, or_true, ENNReal.one_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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
have : Tendsto (fun t : ℝ≥0 =>
        ((t : ℝ≥0∞) ^ 2 * ρ s : ℝ≥0∞)) (𝓝[>] 1) (𝓝 ((1 : ℝ≥0∞) ^ 2 * ρ s)) := by
      refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_
      · exact ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)
      · simp
      · simp only [one_pow, Ne, or_true, ENNReal.one_ne_top, not_false_iff]
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 (HMul.hMul (β := ℝ≥0∞) (HPow.hPow (α := ℝ≥0∞) (β := ℕ) 1 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
simp only [one_pow, one_mul] at this

Premises used: one_pow, one_mul
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
ge_of_tendsto this ?_

Premises used: ge_of_tendsto
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
h :
  ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
    (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine ge_of_tendsto this ?_

Premises used: ge_of_tendsto
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
h :
  ∀ (a : ℝ≥0) (ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a),
    (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑a : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
    (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin] with _ ht

Premises used: self_mem_nhdsWithin
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : ℝ≥0
ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a
⊢ (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑a : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
v.withDensity_le_mul hρ hs ht

Premises used: VitaliFamily.withDensity_le_mul
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦ HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑t : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((ρ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
a : ℝ≥0
ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a
⊢ (μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) (HPow.hPow (β := ℕ) (↑a : ℝ≥0∞) 2) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact v.withDensity_le_mul hρ hs ht

Premises used: VitaliFamily.withDensity_le_mul
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1)
    (𝓝
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_

Premises used: Iff.mpr, ENNReal.Tendsto.mul_const, ENNReal.tendsto_coe, nhdsWithin_le_nhds
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
refine :
  Ne (α := ℝ≥0∞) 1 0 ∨ Ne (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1)
    (𝓝
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
refine ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Ne (α := ℝ≥0∞) 1 0 ∨ Ne (α := ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [true_or, Ne, not_false_iff, one_ne_zero]

Premises used: true_or, Ne, not_false_iff, one_ne_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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1)
    (𝓝
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
have :
      Tendsto (fun t : ℝ≥0 => (t : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s) (𝓝[>] 1)
        (𝓝 ((1 : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s)) := by
      refine ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_
      simp only [true_or, Ne, not_false_iff, one_ne_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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1)
    (𝓝
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
        ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
simp only [one_mul] at this

Premises used: one_mul
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
ge_of_tendsto this ?_

Premises used: ge_of_tendsto
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
h :
  ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
    (ρ : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine ge_of_tendsto this ?_

Premises used: ge_of_tendsto
-- 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (β := ℝ≥0∞)
    (fun (t : ℝ≥0) ↦
      HMul.hMul (β := ℝ≥0∞) (↑t : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (𝓝[>] 1) (𝓝 ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
h :
  ∀ (a : ℝ≥0) (ht : Membership.mem (γ := Set ℝ≥0) (Ioi 1) a),
    (ρ : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (↑a : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[>] 1,
    (ρ : (a : Set α) → ℝ≥0∞) s ≤
      HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ.withDensity (v.limRatioMeas hρ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
filter_upwards [self_mem_nhdsWithin] with _ ht

Premises used: self_mem_nhdsWithin