awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) (B j)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j ∪ W ∩ B j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
Tactic: rw [← measure_union' hj₁ measurableSet_closedBall]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j ∪ W ∩ B j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
have grw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
Tactic: grw [union_subset (h₁ j) (h₂ j)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
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)
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have 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)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
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)
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have hj₄ : 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))
Cleared hypotheses: hj₃
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
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)
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r₁ i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p)
have hRp : 0 ≤ R₁
Tactic: have hRp : 0 ≤ R₁ := fun i => le_max_left 0 (r₁ i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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
have refine : ∀ (i : ℕ) (hi : M * r₁ i ≤ r₂ i), M * R₁ i ≤ R₂ i
Tactic: refine hMr.mono fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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
⊢ M * R₁ i ≤ R₂ i
have rw : max 0 (M * r₁ i) ≤ R₂ i
Tactic: rw [mul_max_of_nonneg _ _ hM.le, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
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₁
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r₁ i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p)
have hMr₁ : ∀ᶠ (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
Cleared hypotheses: hMr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r₁ i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r₂ i) (s i)) atTop p)
have 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)
Tactic: simp_rw [← cthickening_max_zero (r₁ _), ← cthickening_max_zero (r₂ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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
⊢ (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)
have 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)
Tactic: rcases le_or_gt 1 M with hM' | hM'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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)
⊢ (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)
have 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)
Tactic: rcases le_or_gt 1 M with hM' | hM'
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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
⊢ (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)
have 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)
Tactic: apply HasSubset.Subset.eventuallyLE
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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)
have inl : ∀ (i : ℕ) (hi : M * R₁ i ≤ R₂ i), p i → max 0 (r₁ i) ≤ max 0 (r₂ i)
Tactic: refine mono_blimsup' (hMr.mono fun i hi _ => cthickening_mono ?_ (s i))
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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
⊢ (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)
have 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)
Tactic: simp only [← @cthickening_closure _ _ _ (s _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
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
⊢ (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)
have hs : ∀ (i : ℕ),
  IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i))
Tactic: have hs : ∀ i, IsClosed (closure (s i)) := fun i => isClosed_closure
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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)
have h : 0 = M * 0
Tactic: convert! TendstoNhdsWithinIoi.const_mul hM hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (hypothesis)
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)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
have hr' : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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)
have 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)
Tactic: refine eventuallyLE_antisymm_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
have 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)
Tactic: refine eventuallyLE_antisymm_iff.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
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 : ℕ
⊢ M⁻¹ * (M * r i) ≤ r i
have rw : r i ≤ r i
Tactic: rw [inv_mul_cancel_left₀ hM.ne' (r i)]