-- 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₁
⊢ blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p

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

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 (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (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
i : ℕ
hi : M * R₁ i ≤ R₂ i
x✝ : p i
⊢ 0 ⊔ r₁ i ≤ 0 ⊔ r₂ i

Tactic:
exact (le_mul_of_one_le_left (hRp i) hM').trans hi

Result:
no goals

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) (closure (s i))) atTop p ≤ᶠ[ae μ]
    blimsup (fun i => cthickening (0 ⊔ r₂ i) (closure (s i))) atTop p

Tactic:
have hs : ∀ i, IsClosed (closure (s i)) := fun i => isClosed_closure

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
hs : ∀ (i : ℕ), IsClosed (closure (s i))
⊢ 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:
change _ ≤ _

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

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
hs : ∀ (i : ℕ), IsClosed (closure (s i))
⊢ 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

Tactic:
exact blimsup_cthickening_ae_le_of_eventually_mul_le_aux μ p hs
  (tendsto_nhds_max_right hr) hRp hM hM' hMr

Result:
no goals

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
⊢ 0 ⊔ M * r₁ i ≤ R₂ i

Tactic:
exact max_le_max (le_refl 0) hi

Result:
no goals

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
⊢ blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p

Tactic:
let R₁ i := max 0 (r₁ i)

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
⊢ blimsup (fun i => cthickening (r₁ i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => cthickening (r₂ i) (s i)) atTop p