rcases h with ⟨a, ha⟩
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε