-- Mathlib/Order/LiminfLimsup.lean
theorem GaloisConnection.l_limsup_le [ConditionallyCompleteLattice β]
    [ConditionallyCompleteLattice γ] {f : Filter α} {v : α → β} {l : β → γ} {u : γ → β}
    (gc : GaloisConnection l u)
    (hlv : f.IsBoundedUnder (· ≤ ·) fun x => l (v x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c

Tactic:
simp_rw [gc _ _] at hc ⊢

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c

Tactic:
exact limsSup_le_of_le hv_co hc

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
c : γ
hc : ∀ᶠ (n : γ) in map (fun x => l (v x)) f, n ≤ c
⊢ l (limsup v f) ≤ c

Tactic:
rw [Filter.eventually_map] at hc

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
⊢ l (limsup v f) ≤ limsup (fun x => l (v x)) f

Tactic:
refine le_limsSup_of_le hlv fun c hc => ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
c : γ
hc : ∀ᶠ (n : γ) in map (fun x => l (v x)) f, n ≤ c
⊢ l (limsup v f) ≤ c