Theorem: SmallSquareInRectangle (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w
Tactic:
obtain ⟨ε, hε0, hε⟩ := ((Complex.nhds_hasBasis_square p).1 _).mp pInRectInterior
State after:
case intro.intro
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w

State before:
case intro.intro
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pInRectInterior : Rectangle z w ∈ 𝓝 p
ε : ℝ
hε0 : 0 < ε
hε : Square p ε ⊆ Rectangle z w
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, Square p c ⊆ Rectangle z w
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' (hε0)] with _ ⟨hε'0, hε'⟩
State after:
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

State before:
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
Tactic:
exact subset_trans (square_subset_square hε'0 hε'.le) hε
State after:
no goals