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 : ℕ → ℝ
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 : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)

Tactic:
have h₁ : ∀ i, p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i) := by
    rintro i ⟨-, hi⟩; simp only [r', hi, if_true]
-- 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)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
i : ℕ
hi : r i ≤ 0
⊢ M * r i ≤ 0

Tactic:
have hi' : M * r i ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hM.le 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
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
i : ℕ
hi : r i ≤ 0
hi' : M * r i ≤ 0
rw : cthickening (M * r i) (s i) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
rw₁ rw₂ :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i) =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
⊢ cthickening (M * r i) (s i) = cthickening (r i) (s i)

Tactic:
rw [cthickening_of_nonpos hi, cthickening_of_nonpos hi']

Premises used: Metric.cthickening_of_nonpos
-- 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)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
⊢ ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)

Tactic:
have h₂ : ∀ i, p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i) := by
    rintro i ⟨-, hi⟩
    have hi' : M * r i ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hM.le hi
    rw [cthickening_of_nonpos hi, cthickening_of_nonpos 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
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
h : ∀ (i : ℕ), p i ↔ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
⊢ p = fun (i : ℕ) ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0

Tactic:
ext 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
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
i : ℕ
⊢ p i ↔ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0

Tactic:
simp [← and_or_left, lt_or_ge 0 (r i)]

Premises used: and_or_left, lt_or_ge, OfNat.ofNat
-- 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)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
⊢ p = fun (i : ℕ) ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0

Tactic:
have hp : p = fun i => p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0 := by
    ext i; simp [← and_or_left, lt_or_ge 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
hr' : Tendsto r' atTop (𝓝[>] 0)
h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
hp : p = fun (i : ℕ) ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
rw :
  (ae μ).EventuallyEq (β := Prop)
    ((blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ 0 < r i) ⊔
      blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 0)
    ((blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ 0 < r i) ⊔
      blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 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:
rw [hp, blimsup_or_eq_sup, blimsup_or_eq_sup]

Premises used: Filter.blimsup_or_eq_sup
-- 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)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
hp : p = fun (i : ℕ) ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
rw :
  (ae μ).EventuallyEq (β := Prop)
    ((blimsup (fun (x : ℕ) ↦ cthickening (M * r' x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ 0 < r x) ∪
      blimsup (fun (x : ℕ) ↦ cthickening (r x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ r x ≤ 0)
    ((blimsup (fun (x : ℕ) ↦ cthickening (r' x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ 0 < r x) ∪
      blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 0)
⊢ (ae μ).EventuallyEq (β := Prop)
    ((blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ 0 < r i) ∪
      blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 0)
    ((blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ 0 < r i) ∪
      blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 0)

Tactic:
rw [blimsup_congr (Eventually.of_forall h₀), blimsup_congr (Eventually.of_forall h₁),
    blimsup_congr (Eventually.of_forall h₂)]

Premises used: Filter.Eventually.of_forall, Filter.blimsup_congr
-- 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)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
hp : p = fun (i : ℕ) ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
⊢ (ae μ).EventuallyEq (β := Prop)
    ((blimsup (fun (x : ℕ) ↦ cthickening (M * r' x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ 0 < r x) ∪
      blimsup (fun (x : ℕ) ↦ cthickening (r x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ r x ≤ 0)
    ((blimsup (fun (x : ℕ) ↦ cthickening (r' x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ 0 < r x) ∪
      blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 0)

Tactic:
ae_eq_set_union (this (fun i => p i ∧ 0 < r i) hr') (ae_eq_refl _)

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl, And, LT.lt, OfNat.ofNat
-- 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)
h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)
h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)
hp : p = fun (i : ℕ) ↦ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
⊢ (ae μ).EventuallyEq (β := Prop)
    ((blimsup (fun (x : ℕ) ↦ cthickening (M * r' x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ 0 < r x) ∪
      blimsup (fun (x : ℕ) ↦ cthickening (r x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ r x ≤ 0)
    ((blimsup (fun (x : ℕ) ↦ cthickening (r' x) (s x)) atTop fun (x : ℕ) ↦ p x ∧ 0 < r x) ∪
      blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop fun (i : ℕ) ↦ p i ∧ r i ≤ 0)

Tactic:
exact ae_eq_set_union (this (fun i => p i ∧ 0 < r i) hr') (ae_eq_refl _)

Premises used: MeasureTheory.ae_eq_set_union, MeasureTheory.ae_eq_refl, And, LT.lt, OfNat.ofNat
-- 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
eventuallyLE_antisymm_iff.mpr ⟨?_, HasSubset.Subset.eventuallyLE (?_ : _ ≤ _)⟩

Premises used: Iff.mpr, Filter.eventuallyLE_antisymm_iff, HasSubset.Subset.eventuallyLE, 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
refine_1 :
  (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
refine_2 :
  LE.le.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
refine eventuallyLE_antisymm_iff.mpr ⟨?_, HasSubset.Subset.eventuallyLE (?_ : _ ≤ _)⟩

Premises used: Iff.mpr, Filter.eventuallyLE_antisymm_iff, HasSubset.Subset.eventuallyLE, 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
refine_1 :
  (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (1 / 2 * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
rw [eventuallyLE_congr (blimsup_cthickening_mul_ae_eq μ p s (one_half_pos (α := ℝ)) r hr).symm
      EventuallyEq.rfl]

Premises used: Filter.eventuallyLE_congr, one_half_pos, blimsup_cthickening_mul_ae_eq, Filter.EventuallyEq.rfl, Filter.EventuallyEq.symm
-- 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
refine_1 :
  Subset.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ cthickening (1 / 2 * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (1 / 2 * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
apply HasSubset.Subset.eventuallyLE

Premises used: HasSubset.Subset.eventuallyLE
-- 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ LE.le.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ cthickening (1 / 2 * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
mono_blimsup' (hr'.mono fun i hi pi => cthickening_subset_thickening' (hi pi) ?_ (s i))

Premises used: Filter.Eventually.mono, Metric.cthickening_subset_thickening', 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
refine_1 : ∀ (i : ℕ) (hi : p i → 0 < r i) (pi : p i), 1 / 2 * r i < r i
⊢ LE.le.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ cthickening (1 / 2 * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
refine mono_blimsup' (hr'.mono fun i hi pi => cthickening_subset_thickening' (hi pi) ?_ (s i))

Premises used: Filter.Eventually.mono, Metric.cthickening_subset_thickening', 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
i : ℕ
hi : p i → 0 < r i
pi : p i
nlinarith : r i ≤ 1 / 2 * r i → 2 / 2 = 1
nlinarith₁ : r i ≤ 1 / 2 * r i → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : r i ≤ 1 / 2 * r i → HMul.hMul (α := ℝ) 2 1 = 2
nlinarith₃ : r i ≤ 1 / 2 * r i → GT.gt (α := ℝ) 2 0
nlinarith₄ : r i ≤ 1 / 2 * r i → 2 * r i - HMul.hMul (α := ℝ) 1 1 * (1 * r i) + (0 - r i) = 0
⊢ 1 / 2 * r i < r i

Tactic:
nlinarith [hi pi]
-- 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ LE.le.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)

Tactic:
mono_blimsup fun i _ => thickening_subset_cthickening _ _

Premises used: Metric.thickening_subset_cthickening, 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ LE.le.{u_1} (α := Set α) (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)

Tactic:
exact mono_blimsup fun i _ => thickening_subset_cthickening _ _

Premises used: Metric.thickening_subset_cthickening, 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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
have h₁ := blimsup_cthickening_ae_eq_blimsup_thickening (s := s) μ hr hr'
-- 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)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (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:
have h₂ := blimsup_cthickening_mul_ae_eq μ p s hM r hr
-- 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)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
⊢ Tendsto (fun (x : ℕ) ↦ M * r x) atTop (𝓝 (M * 0))

Tactic:
hr.const_mul M

Premises used: Filter.Tendsto.const_mul