exact subset_trans (square_subset_square hε'0 hε'.le) hε
case h
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
a✝ : ℝ
hε'0 : 0 < a✝
hε' : a✝ < ε
⊢ Square p a✝ ⊆ Rectangle z w
no goals