-- Mathlib/Order/Filter/ENNReal.lean
theorem limsup_const_mul_of_ne_top {u : α → ℝ≥0∞} {a : ℝ≥0∞} (ha_top : a ≠ ⊤) :
    (f.limsup fun x : α => a * u x) = a * f.limsup u

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
x : ℝ≥0∞
⊢ (fun x => a⁻¹ * x) (g x) = x

Tactic:
simp [g, ← mul_assoc, ENNReal.inv_mul_cancel ha_zero ha_top]

Result:
no goals

Proof state:
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : a = 0
⊢ limsup (fun x => ⊥) f = ⊥

Tactic:
exact limsup_const_bot

Result:
no goals

Proof state:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
⊢ limsup (fun x => a * u x) f = a * limsup u f

Tactic:
have hg_mono : StrictMono g :=
  Monotone.strictMono_of_injective (fun _ _ _ => by rwa [mul_le_mul_left ha_zero ha_top]) hg_bij.1

Result:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
hg_mono : StrictMono g
⊢ limsup (fun x => a * u x) f = a * limsup u f

Proof state:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
⊢ limsup (fun x => a * u x) f = a * limsup u f

Tactic:
let g := fun x : ℝ≥0∞ => a * x

Result:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
⊢ limsup (fun x => a * u x) f = a * limsup u f

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

Tactic:
simp_rw [ha_zero, zero_mul, ← ENNReal.bot_eq_zero]

Result:
case pos
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : a = 0
⊢ limsup (fun x => ⊥) f = ⊥

Proof state:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
hg_mono : StrictMono g
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective g hg_mono ⋯
⊢ limsup (fun x => a * u x) f = a * limsup u f

Tactic:
exact (OrderIso.limsup_apply g_iso).symm

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
x✝² x✝¹ : ℝ≥0∞
x✝ : x✝² ≤ x✝¹
⊢ g x✝² ≤ g x✝¹

Tactic:
rwa [mul_le_mul_left ha_zero ha_top]

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
⊢ limsup (fun x => a * u x) f = a * limsup u f

Tactic:
by_cases ha_zero : a = 0

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

case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
⊢ limsup (fun x => a * u x) f = a * limsup u f

Proof state:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
hg_mono : StrictMono g
⊢ limsup (fun x => a * u x) f = a * limsup u f

Tactic:
let g_iso := StrictMono.orderIsoOfSurjective g hg_mono hg_bij.2

Result:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
hg_mono : StrictMono g
g_iso : ℝ≥0∞ ≃o ℝ≥0∞ := StrictMono.orderIsoOfSurjective g hg_mono ⋯
⊢ limsup (fun x => a * u x) f = a * limsup u f

Proof state:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
⊢ limsup (fun x => a * u x) f = a * limsup u f

Tactic:
have hg_bij : Function.Bijective g :=
  Function.bijective_iff_has_inverse.mpr
    ⟨fun x => a⁻¹ * x,
      ⟨fun x => by simp [g, ← mul_assoc, ENNReal.inv_mul_cancel ha_zero ha_top], fun x => by
        simp [g, ← mul_assoc, ENNReal.mul_inv_cancel ha_zero ha_top]⟩⟩

Result:
case neg
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
hg_bij : Function.Bijective g
⊢ limsup (fun x => a * u x) f = a * limsup u f

Proof state:
α : Type u_1
f : Filter α
u : α → ℝ≥0∞
a : ℝ≥0∞
ha_top : a ≠ ⊤
ha_zero : ¬a = 0
g : ℝ≥0∞ → ℝ≥0∞ := fun x => a * x
x : ℝ≥0∞
⊢ g ((fun x => a⁻¹ * x) x) = x

Tactic:
simp [g, ← mul_assoc, ENNReal.mul_inv_cancel ha_zero ha_top]

Result:
no goals