awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ → ℝ
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 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)
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 _)
-- 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 : ℕ → ℝ
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)
have refine : ∀ (i : ℕ), Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
Tactic: refine tendsto_nhdsWithin_iff.mpr
      ⟨Tendsto.if' hr tendsto_one_div_add_atTop_nhds_zero_nat, Eventually.of_forall fun 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 : ℕ → ℝ
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 : ℕ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
have pos : ∀ (hi : 0 < r i), Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
Tactic: by_cases hi : 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 : ℕ → ℝ
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)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
have neg : ∀ (hi : ¬0 < r i), Membership.mem (γ := Set ℝ) (Ioi 0) (r' i)
Tactic: by_cases hi : 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 : ℕ → ℝ
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)
have neg : 0 < HAdd.hAdd (α := ℝ) (↑i : ℝ) 1
Tactic: simp only [r', hi, one_div, mem_Ioi, if_false, inv_pos]
-- 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 : ℕ → ℝ
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
⊢ (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 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
-- 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 : ℕ → ℝ
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)
⊢ (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 h₀ : ∀ (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
-- 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 : ℕ → ℝ
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)
⊢ (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 h₁ : ∀ (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]
-- 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 : ℕ → ℝ
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
⊢ cthickening (M * r i) (s i) = cthickening (r i) (s i)
have hi' : M * r i ≤ 0
Tactic: have hi' : M * r i ≤ 0 := mul_nonpos_of_nonneg_of_nonpos hM.le 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 : ℕ → ℝ
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
⊢ cthickening (M * r i) (s i) = cthickening (r i) (s i)
have rw : cthickening (M * r i) (s i) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
Tactic: rw [cthickening_of_nonpos hi, cthickening_of_nonpos 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 : ℕ → ℝ
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)
⊢ cthickening (M * r i) (s i) = cthickening (r i) (s i)
have rw₁ : closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i) =
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
Tactic: rw [cthickening_of_nonpos hi, cthickening_of_nonpos hi']
-- 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 : ℕ → ℝ
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)
⊢ (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 h₂ : ∀ (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']
-- 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 : ℕ → ℝ
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
have h : ∀ (i : ℕ), p i ↔ p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0
Tactic: ext i
-- 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 : ℕ → ℝ
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)
⊢ (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 hp : 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)]
-- 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 : ℕ → ℝ
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 (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
have 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)
Tactic: rw [hp, blimsup_or_eq_sup, blimsup_or_eq_sup]
-- 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 : ℕ → ℝ
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 (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)
have 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)
Tactic: rw [blimsup_congr (Eventually.of_forall h₀), blimsup_congr (Eventually.of_forall h₁),
    blimsup_congr (Eventually.of_forall h₂)]
-- 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 α
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)
have 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)
Tactic: refine eventuallyLE_antisymm_iff.mpr ⟨?_, 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 α
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)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
have 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)
Tactic: refine eventuallyLE_antisymm_iff.mpr ⟨?_, 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ (ae μ).EventuallyLE (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
have 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)
Tactic: rw [eventuallyLE_congr (blimsup_cthickening_mul_ae_eq μ p s (one_half_pos (α := ℝ)) r hr).symm
      EventuallyEq.rfl]
-- 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 α
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
⊢ (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)
have 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)
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 α
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)
have refine_1 : ∀ (i : ℕ) (hi : p i → 0 < r i) (pi : p i), 1 / 2 * r i < r i
Tactic: refine mono_blimsup' (hr'.mono fun i hi pi => cthickening_subset_thickening' (hi pi) ?_ (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 α
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
⊢ 1 / 2 * r i < r i
have nlinarith : r i ≤ 1 / 2 * r i → 2 / 2 = 1
Tactic: nlinarith [hi pi]