-- Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
theorem blimsup_thickening_mul_ae_eq (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ)
    (hr : Tendsto r atTop (𝓝 0)) :
    (blimsup (fun i => thickening (M * r i) (s i)) atTop p : Set α) =ᵐ[μ]
      (blimsup (fun i => thickening (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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p

Tactic:
have h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p =
    blimsup (fun i => thickening (r i) (s i)) atTop q := by
  refine blimsup_congr' (Eventually.of_forall fun i h => ?_)
  replace hi : 0 < r i := by contrapose! h; apply thickening_of_nonpos h
  simp only [q, hi, iff_self_and, imp_true_iff]

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
i : ℕ
h : thickening (r i) (s i) ≠ ⊥
hi : 0 < r i
⊢ p i ↔ q i

Tactic:
simp only [q, hi, iff_self_and, imp_true_iff]

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q

Tactic:
refine blimsup_congr' (Eventually.of_forall fun i h ↦ ?_)

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ p i ↔ q 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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < M * r i

Tactic:
contrapose! h

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : M * r i ≤ 0
⊢ thickening (M * r i) (s 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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : 0 < r i
⊢ p i ↔ q i

Tactic:
simp only [q, h, iff_self_and, imp_true_iff]

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < r i

Tactic:
rw [← mul_pos_iff_of_pos_left hM]

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
i : ℕ
h : thickening (M * r i) (s i) ≠ ⊥
⊢ 0 < M * 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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p

Tactic:
have h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p =
    blimsup (fun i => thickening (M * r i) (s i)) atTop q := by
  refine blimsup_congr' (Eventually.of_forall fun i h ↦ ?_)
  replace h : 0 < r i := by
    rw [← mul_pos_iff_of_pos_left hM]; contrapose! h; apply thickening_of_nonpos h
  simp only [q, h, iff_self_and, imp_true_iff]

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 : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p