-- Mathlib/Order/LiminfLimsup.lean
theorem Monotone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
    {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atTop atTop) :
    IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Tactic:
obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) ((g ∘ f) a) c
b : β
hb : ∀ a ≥ b, c < g a
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Tactic:
refine ⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (g ∘ f) → IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) ((g ∘ f) a) c
b : β
hb : ∀ a ≥ b, c < g a
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Tactic:
exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x1 x2 => x1 ≤ x2) x c
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Tactic:
rw [eventually_map] at hc

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (g ∘ f) → IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Tactic:
rintro ⟨c, hc⟩

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x1 x2 => x1 ≤ x2) x c
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f