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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)

Tactic:
replace hj₂ : ↑C⁻¹ * μ (B j) ≤ μ (b j) := by
    rw [ENNReal.coe_inv hC, ← ENNReal.div_eq_inv_mul]
    exact ENNReal.div_le_of_le_mul' hj₂
-- 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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
grw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)
⊢ HAdd.hAdd (β := ℝ≥0∞) (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)

Tactic:
grw [hj₂]
-- 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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j ∪ W ∩ B j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)

Tactic:
rw [← measure_union' hj₁ measurableSet_closedBall]

Premises used: measurableSet_closedBall, MeasureTheory.measure_union'
-- 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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
grw grw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j ∪ W ∩ B j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)

Tactic:
grw [union_subset (h₁ j) (h₂ j)]

Premises used: Set.union_subset
-- 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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
⊢ HAdd.hAdd (β := ℝ≥0∞) (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)

Tactic:
have hj₃ : ↑C⁻¹ * μ (B j) + μ (W ∩ B j) ≤ μ (B j) := by
    grw [hj₂]
    rw [← measure_union' hj₁ measurableSet_closedBall]
    grw [union_subset (h₁ j) (h₂ j)]
-- 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 α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
hj₃ :
  HAdd.hAdd (β := ℝ≥0∞) (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)
⊢ HAdd.hAdd (β := ℝ≥0∞) (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
        ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) -
      HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))

Tactic:
replace hj₃ := tsub_le_tsub_right hj₃ (↑C⁻¹ * μ (B j))
-- 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)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
⊢ 0 ≤ R₁

Tactic:
have hRp : 0 ≤ R₁ := fun i => le_max_left 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₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
⊢ ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i

Tactic:
hMr.mono fun i hi ↦ ?_

Premises used: Filter.Eventually.mono
-- 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)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
refine : ∀ (i : ℕ) (hi : M * r₁ i ≤ r₂ i), M * R₁ i ≤ R₂ i
⊢ ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i

Tactic:
refine hMr.mono fun i hi ↦ ?_

Premises used: Filter.Eventually.mono
-- 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)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
i : ℕ
hi : M * r₁ i ≤ r₂ i
rw : max 0 (M * r₁ i) ≤ R₂ i
⊢ M * R₁ i ≤ R₂ i

Tactic:
rw [mul_max_of_nonneg _ _ hM.le, mul_zero]

Premises used: LT.lt.le, mul_max_of_nonneg, 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 μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
i : ℕ
hi : M * r₁ i ≤ r₂ i
⊢ max 0 (M * r₁ i) ≤ R₂ i

Tactic:
max_le_max (le_refl 0) hi

Premises used: le_refl, max_le_max, 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₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
i : ℕ
hi : M * r₁ i ≤ r₂ i
⊢ max 0 (M * r₁ i) ≤ R₂ i

Tactic:
exact max_le_max (le_refl 0) hi

Premises used: le_refl, max_le_max, 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₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
hMr : ∀ᶠ (i : ℕ) in atTop, M * r₁ i ≤ r₂ i
R₁ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₁ i)
R₂ : (i : ℕ) → ℝ := fun (i : ℕ) ↦ max 0 (r₂ i)
hRp : 0 ≤ R₁
⊢ ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i

Tactic:
replace hMr : ∀ᶠ i in atTop, M * R₁ i ≤ R₂ i := by
    refine hMr.mono fun i hi ↦ ?_
    rw [mul_max_of_nonneg _ _ hM.le, mul_zero]
    exact max_le_max (le_refl 0) 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₁ 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
simp_rw :
  (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)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r₁ i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p)

Tactic:
simp_rw [← cthickening_max_zero (r₁ _), ← cthickening_max_zero (r₂ _)]

Premises used: Metric.cthickening_max_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 μ
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
inl :
  ∀ (hM' : 1 ≤ M),
    (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)
inr :
  ∀ (hM' : M < 1),
    (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)
⊢ (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:
rcases le_or_gt 1 M with hM' | hM'

Premises used: le_or_gt, 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₁ 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 :
  Subset.{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)
⊢ (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:
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 α
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
⊢ 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:
mono_blimsup' (hMr.mono fun i hi _ => cthickening_mono ?_ (s i))

Premises used: Metric.cthickening_mono, Filter.Eventually.mono, Filter.mono_blimsup'