-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
/-- If `xs : ι → ℝ≥0∞` is bounded, then we have `liminf (toReal ∘ xs) = toReal (liminf xs)`. -/
lemma limsup_toReal_eq {ι : Type*} {F : Filter ι} [NeBot F] {b : ℝ≥0∞} (b_ne_top : b ≠ ∞)
    {xs : ι → ℝ≥0∞} (le_b : ∀ᶠ i in F, xs i ≤ b) :
    F.limsup (fun i ↦ (xs i).toReal) = (F.limsup xs).toReal

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
key : b.truncateToReal (limsup xs F) = limsup (b.truncateToReal ∘ xs) F
⊢ limsup (fun a => b.truncateToReal (xs a)) F = limsup (b.truncateToReal ∘ xs) F

Tactic:
rfl

Result:
no goals

Proof state:
case h
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
i : ι
i_le_b : xs i ≤ b
⊢ (xs i).toReal = b.truncateToReal (xs i)

Tactic:
simp only [truncateToReal_eq_toReal b_ne_top i_le_b, implies_true]

Result:
no goals

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
⊢ limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal

Tactic:
simp_rw [limsup_congr aux, aux']

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
⊢ limsup (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (limsup xs F)

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal

Tactic:
have aux' : (F.limsup xs).toReal = ENNReal.truncateToReal b (F.limsup xs) := by
  rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
⊢ limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
⊢ limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal

Tactic:
have aux : ∀ᶠ i in F, (xs i).toReal = ENNReal.truncateToReal b (xs i) := by
  filter_upwards [le_b] with i i_le_b
  simp only [truncateToReal_eq_toReal b_ne_top i_le_b, implies_true]

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ limsup (fun i => (xs i).toReal) F = (limsup xs F).toReal

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
⊢ ∀ (x : ℝ≥0∞), (fun x1 x2 => x1 ≥ x2) x 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
key : b.truncateToReal (limsup xs F) = limsup (b.truncateToReal ∘ xs) F
⊢ limsup (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (limsup xs F)

Tactic:
rw [key]

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
key : b.truncateToReal (limsup xs F) = limsup (b.truncateToReal ∘ xs) F
⊢ limsup (fun a => b.truncateToReal (xs a)) F = limsup (b.truncateToReal ∘ xs) F

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ ∀ (a : ℝ≥0∞), (∀ᶠ (x : ℝ≥0∞) in map xs F, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) 0 a

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
⊢ ∀ᶠ (x : ℝ≥0∞) in map xs F, (fun x1 x2 => x1 ≤ x2) x b

Tactic:
simpa only [eventually_map] using le_b

Result:
no goals

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ (limsup xs F).toReal = b.truncateToReal (limsup xs F)

Tactic:
rw [truncateToReal_eq_toReal b_ne_top (limsup_le_of_le ⟨0, by simp⟩ le_b)]

Result:
no goals

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
⊢ limsup (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (limsup xs F)

Tactic:
have key := Monotone.map_limsup_of_continuousAt (F := F) (monotone_truncateToReal b_ne_top) xs
        (continuous_truncateToReal b_ne_top).continuousAt
        ⟨b, by simpa only [eventually_map] using le_b⟩
        (IsBoundedUnder.isCoboundedUnder_le ⟨0, Eventually.of_forall (by simp)⟩)

Result:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (limsup xs F).toReal = b.truncateToReal (limsup xs F)
key : b.truncateToReal (limsup xs F) = limsup (b.truncateToReal ∘ xs) F
⊢ limsup (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (limsup xs F)

Proof state:
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
⊢ ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)

Tactic:
filter_upwards [le_b] with i i_le_b

Result:
case h
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
i : ι
i_le_b : xs i ≤ b
⊢ (xs i).toReal = b.truncateToReal (xs i)