-- Mathlib/Order/LiminfLimsup.lean
theorem isCoboundedUnder_le_max [LinearOrder β] {f : Filter α} {u v : α → β}
    (h : f.IsCoboundedUnder (· ≤ ·) u ∨ f.IsCoboundedUnder (· ≤ ·) v) :
    f.IsCoboundedUnder (· ≤ ·) (fun a ↦ max (u a) (v a))

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a

Tactic:
rcases h' with ⟨b, hb⟩

Result:
case inr.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a => u a ⊔ v a) f, (fun x1 x2 => x1 ≤ x2) x c
⊢ b ≤ c

Tactic:
apply hb c

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a => u a ⊔ v a) f, (fun x1 x2 => x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x c

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
⊢ ∀ (a : β), (∀ᶠ (x : β) in map (fun a => u a ⊔ v a) f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a

Tactic:
intro c hc

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a => u a ⊔ v a) f, (fun x1 x2 => x1 ≤ x2) x c
⊢ b ≤ c

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun a => u a ⊔ v a) f, (fun x1 x2 => x1 ≤ x2) x c
⊢ ∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x c

Tactic:
rw [eventually_map] at hc ⊢

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (u a ⊔ v a) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (v a) c

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a

Tactic:
use b

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
⊢ ∀ (a : β), (∀ᶠ (x : β) in map (fun a => u a ⊔ v a) f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (u a ⊔ v a) c
x✝ : α
⊢ (fun x1 x2 => x1 ≤ x2) (u x✝ ⊔ v x✝) c → (fun x1 x2 => x1 ≤ x2) (v x✝) c

Tactic:
simp +contextual only [implies_true, max_le_iff, and_imp]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (u a ⊔ v a) c
⊢ ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (v a) c

Tactic:
refine hc.mono (fun _ ↦ ?_)

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (u a ⊔ v a) c
x✝ : α
⊢ (fun x1 x2 => x1 ≤ x2) (u x✝ ⊔ v x✝) c → (fun x1 x2 => x1 ≤ x2) (v x✝) c