case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f

case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : ¬a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
⊢ limsup (fun x => a * u x) f = a * limsup u f
by_cases ha_top : a ≠ ⊤
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : ¬a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
push_neg  at ha_top
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f

case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
by_cases hu : u =ᶠ[f] 0
no goals
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
exact limsup_const_mul_of_ne_top ha_top
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
hau : (fun x => a * u x) =ᶠ[f] 0
⊢ ⊥ = a * ⊥
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
hau : (fun x => a * u x) =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
simp only [limsup_congr hu, limsup_congr hau, Pi.zero_apply, ← ENNReal.bot_eq_zero,
  limsup_const_bot]
no goals
case pos
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
hau : (fun x => a * u x) =ᶠ[f] 0
⊢ ⊥ = a * ⊥
simp
no goals
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : u =ᶠ[f] 0
x : α
hx : u x = OfNat.ofNat 0 x
⊢ (fun x => a * u x) x = OfNat.ofNat 0 x
simp [hx]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
have hu_mul : ∃ᶠ x : α in f, ⊤ ≤ ite (u x = 0) (0 : ℝ≥0∞) ⊤ := by
  rw [EventuallyEq, not_eventually] at hu
  refine' hu.mono fun x hx => _
  rw [Pi.zero_apply] at hx
  simp [hx]
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
h_top_le : limsup (fun x => if u x = 0 then 0 else ⊤) f = ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
have h_top_le : (f.limsup fun x : α => ite (u x = 0) (0 : ℝ≥0∞) ⊤) = ⊤ :=
  eq_top_iff.mpr (le_limsup_of_frequently_le hu_mul)
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
h_top_le : limsup (fun x => if u x = 0 then 0 else ⊤) f = ⊤
hfu : limsup u f ≠ 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
h_top_le : limsup (fun x => if u x = 0 then 0 else ⊤) f = ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f
have hfu : f.limsup u ≠ 0 := mt limsup_eq_zero_iff.1 hu
no goals
case neg
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
hu_mul : ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
h_top_le : limsup (fun x => if u x = 0 then 0 else ⊤) f = ⊤
hfu : limsup u f ≠ 0
⊢ limsup (fun x => a * u x) f = a * limsup u f
simp only [ha_top, top_mul', hfu, h_top_le]
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
⊢ ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ¬u =ᶠ[f] 0
⊢ ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
rw [EventuallyEq, not_eventually] at hu
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
x : α
hx : ¬u x = OfNat.ofNat 0 x
⊢ ⊤ ≤ if u x = 0 then 0 else ⊤
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
⊢ ∃ᶠ (x : α) in f, ⊤ ≤ if u x = 0 then 0 else ⊤
refine' hu.mono fun x hx => _
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
x : α
hx : ¬u x = 0
⊢ ⊤ ≤ if u x = 0 then 0 else ⊤
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
x : α
hx : ¬u x = OfNat.ofNat 0 x
⊢ ⊤ ≤ if u x = 0 then 0 else ⊤
rw [Pi.zero_apply] at hx
no goals
α : Type u_1
f : Filter α
inst✝ : CountableInterFilter f
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a = ⊤
hu : ∃ᶠ (x : α) in f, ¬u x = OfNat.ofNat 0 x
x : α
hx : ¬u x = 0
⊢ ⊤ ≤ if u x = 0 then 0 else ⊤
simp [hx]