exact ht _ <| (diff_subset_diff (square_subset_square hε'0 hε'.le) subset_rfl).trans hε
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
ε' : ℝ
hε'0 : 0 < ε'
hε' : ε' < ε
⊢ BddAbove (f '' (Square x ε' \ {x}))
no goals