Theorem: frequently_smaller (Ray/Misc/Bounds.lean)

State before:
z : ℂ
z0 : z ≠ 0
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, Complex.abs w < Complex.abs z
Tactic:
simp only [Filter.Frequently, Metric.eventually_nhds_iff, not_exists, not_forall, not_not,
  Complex.dist_eq, not_and]
State after:
z : ℂ
z0 : z ≠ 0
⊢ ∀ x > 0, ∃ x_1, ∃ (_ : Complex.abs (x_1 - z) < x), Complex.abs x_1 < Complex.abs z

State before:
z : ℂ
z0 : z ≠ 0
⊢ ∀ x > 0, ∃ x_1, ∃ (_ : Complex.abs (x_1 - z) < x), Complex.abs x_1 < Complex.abs z
Tactic:
intro r rp
State after:
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z

State before:
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z
Tactic:
rcases slightly_smaller z0 rp with ⟨w, b, lt⟩
State after:
case intro.intro
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
w : ℂ
b : Complex.abs (w - z) < r
lt : Complex.abs w < Complex.abs z
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z

State before:
case intro.intro
z : ℂ
z0 : z ≠ 0
r : ℝ
rp : r > 0
w : ℂ
b : Complex.abs (w - z) < r
lt : Complex.abs w < Complex.abs z
⊢ ∃ x, ∃ (_ : Complex.abs (x - z) < r), Complex.abs x < Complex.abs z
Tactic:
use w, b, lt
State after:
no goals