awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
inl : ∀ (i : ℕ) (hi : M * R₁ i ≤ R₂ i), p i → max 0 (r₁ i) ≤ max 0 (r₂ i)
⊢ LE.le.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ cthickening (max 0 (r₁ i)) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (max 0 (r₂ i)) (s i)) atTop p)

Tactic:
refine mono_blimsup' (hMr.mono fun i hi _ => cthickening_mono ?_ (s i))

Premises used: Metric.cthickening_mono, Filter.Eventually.mono, Filter.mono_blimsup'
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
i : ℕ
hi : M * R₁ i ≤ R₂ i
h : p i
⊢ max 0 (r₁ i) ≤ max 0 (r₂ i)

Tactic:
(le_mul_of_one_le_left (hRp i) hM').trans hi

Premises used: le_mul_of_one_le_left, LE.le.trans
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
i : ℕ
hi : M * R₁ i ≤ R₂ i
h : p i
⊢ max 0 (r₁ i) ≤ max 0 (r₂ i)

Tactic:
exact (le_mul_of_one_le_left (hRp i) hM').trans hi

Premises used: le_mul_of_one_le_left, LE.le.trans
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
inr :
  (ae μ).EventuallyLE (β := Prop)
    (blimsup
      (fun (i : ℕ) ↦ cthickening (max 0 (r₁ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p)
    (blimsup
      (fun (i : ℕ) ↦ cthickening (max 0 (r₂ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (max 0 (r₁ i)) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (max 0 (r₂ i)) (s i)) atTop p)

Tactic:
simp only [← @cthickening_closure _ _ _ (s _)]

Premises used: Metric.cthickening_closure
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
⊢ ∀ (i : ℕ),
    IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i))

Tactic:
have hs : ∀ i, IsClosed (closure (s i)) := fun i => isClosed_closure
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
hs :
  ∀ (i : ℕ),
    IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i))
⊢ (ae μ).EventuallyLE (β := Prop)
    (blimsup
      (fun (i : ℕ) ↦ cthickening (max 0 (r₁ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p)
    (blimsup
      (fun (i : ℕ) ↦ cthickening (max 0 (r₂ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p)

Tactic:
blimsup_cthickening_ae_le_of_eventually_mul_le_aux μ p hs
      (tendsto_nhds_max_right hr) hRp hM hM' hMr

Premises used: blimsup_cthickening_ae_le_of_eventually_mul_le_aux, Filter.tendsto_nhds_max_right
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
hs :
  ∀ (i : ℕ),
    IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i))
⊢ (ae μ).EventuallyLE (β := Prop)
    (blimsup
      (fun (i : ℕ) ↦ cthickening (max 0 (r₁ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p)
    (blimsup
      (fun (i : ℕ) ↦ cthickening (max 0 (r₂ i)) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)))
      atTop p)

Tactic:
exact blimsup_cthickening_ae_le_of_eventually_mul_le_aux μ p hs
      (tendsto_nhds_max_right hr) hRp hM hM' hMr

Premises used: blimsup_cthickening_ae_le_of_eventually_mul_le_aux, Filter.tendsto_nhds_max_right
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ Tendsto (fun (a : ℕ) ↦ M * r a) atTop (𝓝[>] (M * 0))

Tactic:
TendstoNhdsWithinIoi.const_mul hM hr

Premises used: Filter.TendstoNhdsWithinIoi.const_mul
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
h h₁ : 0 = M * 0
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)

Tactic:
convert! TendstoNhdsWithinIoi.const_mul hM hr

Premises used: Filter.TendstoNhdsWithinIoi.const_mul
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ 0 = M * 0

Tactic:
simp only [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)

Tactic:
have hr' : Tendsto (fun i => M * r i) atTop (𝓝[>] 0) := by
      convert! TendstoNhdsWithinIoi.const_mul hM hr <;> simp only [mul_zero]
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)

Tactic:
eventuallyLE_antisymm_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Filter.eventuallyLE_antisymm_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)
refine_1 :
  (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
refine_2 :
  (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)

Tactic:
refine eventuallyLE_antisymm_iff.mpr ⟨?_, ?_⟩

Premises used: Iff.mpr, Filter.eventuallyLE_antisymm_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)
i : ℕ
rw rw₁ : r i ≤ r i
⊢ M⁻¹ * (M * r i) ≤ r i

Tactic:
rw [inv_mul_cancel_left₀ hM.ne' (r i)]

Premises used: inv_mul_cancel_left₀, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)

Tactic:
exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p (inv_pos.mpr hM) hr'
        (Eventually.of_forall fun i => by rw [inv_mul_cancel_left₀ hM.ne' (r i)])

Premises used: Iff.mpr, blimsup_cthickening_ae_le_of_eventually_mul_le, inv_pos, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)

Tactic:
blimsup_cthickening_ae_le_of_eventually_mul_le μ p hM hr
        (Eventually.of_forall fun i => le_refl _)

Premises used: le_refl, HMul.hMul, blimsup_cthickening_ae_le_of_eventually_mul_le, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝[>] 0)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)

Tactic:
exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p hM hr
        (Eventually.of_forall fun i => le_refl _)

Premises used: le_refl, HMul.hMul, blimsup_cthickening_ae_le_of_eventually_mul_le, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
⊢ ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)

Tactic:
have : ∀ (p : ℕ → Prop) {r : ℕ → ℝ} (_ : Tendsto r atTop (𝓝[>] 0)),
      (blimsup (fun i => cthickening (M * r i) (s i)) atTop p : Set α) =ᵐ[μ]
        (blimsup (fun i => cthickening (r i) (s i)) atTop p : Set α) := by
    clear p hr r; intro p r hr
    have hr' : Tendsto (fun i => M * r i) atTop (𝓝[>] 0) := by
      convert! TendstoNhdsWithinIoi.const_mul hM hr <;> simp only [mul_zero]
    refine eventuallyLE_antisymm_iff.mpr ⟨?_, ?_⟩
    · exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p (inv_pos.mpr hM) hr'
        (Eventually.of_forall fun i => by rw [inv_mul_cancel_left₀ hM.ne' (r i)])
    · exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p hM hr
        (Eventually.of_forall fun i => le_refl _)
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ Tendsto r' atTop (𝓝[>] 0)

Tactic:
tendsto_nhdsWithin_iff.mpr
      ⟨Tendsto.if' hr tendsto_one_div_add_atTop_nhds_zero_nat, Eventually.of_forall fun i => ?_⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, tendsto_one_div_add_atTop_nhds_zero_nat, Filter.Eventually.of_forall, Filter.Tendsto.if', And.intro
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
refine : ∀ (i : ℕ), Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
⊢ Tendsto r' atTop (𝓝[>] 0)

Tactic:
refine tendsto_nhdsWithin_iff.mpr
      ⟨Tendsto.if' hr tendsto_one_div_add_atTop_nhds_zero_nat, Eventually.of_forall fun i => ?_⟩

Premises used: Iff.mpr, tendsto_nhdsWithin_iff, tendsto_one_div_add_atTop_nhds_zero_nat, Filter.Eventually.of_forall, Filter.Tendsto.if', And.intro
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
i : ℕ
pos : ∀ (hi : 0 < r i), Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
neg : ∀ (hi : ¬0 < r i), Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)

Tactic:
by_cases hi : 0 < r i
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
i : ℕ
hi : 0 < r i
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)

Tactic:
simp [r', hi]
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
i : ℕ
hi : ¬0 < r i
neg : 0 < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)

Tactic:
simp only [r', hi, one_div, mem_Ioi, if_false, inv_pos]

Premises used: if_false, Set.mem_Ioi, inv_pos, one_div
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
i : ℕ
hi : ¬0 < r i
⊢ 0 < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
⊢ Tendsto r' atTop (𝓝[>] 0)

Tactic:
have hr' : Tendsto r' atTop (𝓝[>] 0) := by
    refine tendsto_nhdsWithin_iff.mpr
      ⟨Tendsto.if' hr tendsto_one_div_add_atTop_nhds_zero_nat, Eventually.of_forall fun i => ?_⟩
    by_cases hi : 0 < r i
    · simp [r', hi]
    · simp only [r', hi, one_div, mem_Ioi, if_false, inv_pos]; positivity
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hr' : Tendsto r' atTop (𝓝[>] 0)
⊢ ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hr' : Tendsto r' atTop (𝓝[>] 0)
⊢ ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)

Tactic:
have h₀ : ∀ i, p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i) := by
    grind
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
        (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
r' : ℕ → ℝ := fun (i : ℕ) ↦ if 0 < r i then r i else 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
i : ℕ
hi : 0 < r i
⊢ cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)

Tactic:
simp only [r', hi, if_true]

Premises used: if_true