-- Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
theorem blimsup_cthickening_ae_le_of_eventually_mul_le (p : ℕ → Prop) {s : ℕ → Set α} {M : ℝ}
    (hM : 0 < M) {r₁ r₂ : ℕ → ℝ} (hr : Tendsto r₁ atTop (𝓝[>] 0))
    (hMr : ∀ᶠ i in atTop, M * r₁ i ≤ r₂ i) :
    (blimsup (fun i => cthickening (r₁ i) (s i)) atTop p : Set α) ≤ᵐ[μ]
      (blimsup (fun i => cthickening (r₂ i) (s i)) atTop p : Set α)

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : 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₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
⊢ ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i

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

Result:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : 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₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
i : ℕ
hi : M * r₁ i ≤ r₂ i
⊢ M * R₁ i ≤ R₂ i

Proof state:
case inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
⊢ blimsup (fun i => cthickening (0 ⊔ r₁ i) (s i)) atTop p ≤ᶠ[ae μ]
    blimsup (fun i => cthickening (0 ⊔ r₂ i) (s i)) atTop p

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

Result:
case inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : M < 1
⊢ blimsup (fun i => cthickening (0 ⊔ r₁ i) (closure (s i))) atTop p ≤ᶠ[ae μ]
    blimsup (fun i => cthickening (0 ⊔ r₂ i) (closure (s i))) atTop p

Proof state:
case inl.h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
⊢ blimsup (fun i => cthickening (0 ⊔ r₁ i) (s i)) atTop p ≤ blimsup (fun i => cthickening (0 ⊔ r₂ i) (s i)) atTop p

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

Result:
case inl.h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
i : ℕ
hi : M * R₁ i ≤ R₂ i
x✝ : p i
⊢ 0 ⊔ r₁ i ≤ 0 ⊔ r₂ i

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : 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₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
i : ℕ
hi : M * r₁ i ≤ r₂ i
⊢ M * R₁ i ≤ R₂ i

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

Result:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : 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₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
i : ℕ
hi : M * r₁ i ≤ r₂ i
⊢ 0 ⊔ M * r₁ i ≤ R₂ i

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
⊢ blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p

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

Result:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
⊢ blimsup (fun i => cthickening (0 ⊔ r₁ i) (s i)) atTop p ≤ᶠ[ae μ]
    blimsup (fun i => cthickening (0 ⊔ r₂ i) (s i)) atTop p

Proof state:
case inl
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
⊢ blimsup (fun i => cthickening (0 ⊔ r₁ i) (s i)) atTop p ≤ᶠ[ae μ]
    blimsup (fun i => cthickening (0 ⊔ r₂ i) (s i)) atTop p

Tactic:
apply HasSubset.Subset.eventuallyLE

Result:
case inl.h
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r₁ r₂ : ℕ → ℝ
hr : Tendsto r₁ atTop (𝓝[>] 0)
R₁ : ℕ → ℝ := fun i => 0 ⊔ r₁ i
R₂ : ℕ → ℝ := fun i => 0 ⊔ r₂ i
hRp : 0 ≤ R₁
hMr : ∀ᶠ (i : ℕ) in atTop, M * R₁ i ≤ R₂ i
hM' : 1 ≤ M
⊢ blimsup (fun i => cthickening (0 ⊔ r₁ i) (s i)) atTop p ⊆ blimsup (fun i => cthickening (0 ⊔ r₂ i) (s i)) atTop p