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

Tactic:
intro y h

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
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in F, y ≤ xs n
⊢ y ≤ b

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
⊢ liminf xs F ≤ b

Tactic:
apply liminf_le_of_le ⟨0, 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
⊢ ∀ (b_1 : ℝ≥0∞), (∀ᶠ (n : ι) in F, b_1 ≤ xs n) → b_1 ≤ b

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
liminf_le : liminf xs F ≤ b
⊢ liminf (fun i => (xs i).toReal) F = (liminf 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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ liminf (fun i => (xs i).toReal) F = (liminf 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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
key : b.truncateToReal (liminf xs F) = liminf (b.truncateToReal ∘ xs) F
⊢ liminf (fun a => b.truncateToReal (xs a)) F = liminf (b.truncateToReal ∘ xs) F

Tactic:
rfl

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
liminf_le : liminf xs F ≤ 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
liminf_le : liminf xs F ≤ b
i : ι
i_le_b : xs i ≤ b
⊢ (xs i).toReal = b.truncateToReal (xs i)

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
⊢ ∀ᶠ (x : ℝ≥0∞) in map xs F, (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
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in F, y ≤ xs n
⊢ y ≤ b

Tactic:
obtain ⟨i, hi⟩ := (Eventually.and h le_b).exists

Result:
case intro
ι : Type u_5
F : Filter ι
inst✝ : F.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ⊤
xs : ι → ℝ≥0∞
le_b : ∀ᶠ (i : ι) in F, xs i ≤ b
y : ℝ≥0∞
h : ∀ᶠ (n : ι) in F, y ≤ xs n
i : ι
hi : y ≤ xs i ∧ xs i ≤ b
⊢ y ≤ b

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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf 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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
⊢ (liminf xs F).toReal = b.truncateToReal (liminf xs F)

Tactic:
rw [truncateToReal_eq_toReal b_ne_top liminf_le]

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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
⊢ liminf (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (liminf xs F)

Tactic:
have key := Monotone.map_liminf_of_continuousAt (F := F) (monotone_truncateToReal b_ne_top) xs
        (continuous_truncateToReal b_ne_top).continuousAt
        (IsBoundedUnder.isCoboundedUnder_ge ⟨b, by simpa only [eventually_map] using le_b⟩)
        ⟨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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
key : b.truncateToReal (liminf xs F) = liminf (b.truncateToReal ∘ xs) F
⊢ liminf (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (liminf 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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf 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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
key : b.truncateToReal (liminf xs F) = liminf (b.truncateToReal ∘ xs) F
⊢ liminf (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (liminf 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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
key : b.truncateToReal (liminf xs F) = liminf (b.truncateToReal ∘ xs) F
⊢ liminf (fun a => b.truncateToReal (xs a)) F = liminf (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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
⊢ liminf (fun i => (xs i).toReal) F = (liminf xs F).toReal

Tactic:
simp_rw [liminf_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
liminf_le : liminf xs F ≤ b
aux : ∀ᶠ (i : ι) in F, (xs i).toReal = b.truncateToReal (xs i)
aux' : (liminf xs F).toReal = b.truncateToReal (liminf xs F)
⊢ liminf (fun a => b.truncateToReal (xs a)) F = b.truncateToReal (liminf xs F)

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
liminf_le : liminf xs F ≤ 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