Theorem: Metric.continuous_near (Ray/Misc/Bounds.lean)

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
⊢ ∀ (e : ℝ), 0 < e → ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
intro e ep
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
rcases Metric.continuousAt_iff.mp fc e ep with ⟨s,sp,sc⟩
State after:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, dist x z < s → dist (f x) (f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

State before:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, dist x z < s → dist (f x) (f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
simp_rw [ Complex.dist_eq ] at sc
State after:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

State before:
case intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
by_cases sr : s ≤ r
State after:
case pos
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

State before:
case pos
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
exists s
State after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : ¬s ≤ r
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
simp only [not_le] at sr
State after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∃ s, 0 < s ∧ s ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
Tactic:
exists r
State after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ 0 < r ∧ r ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ 0 < r ∧ r ≤ r ∧ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e
Tactic:
refine ⟨rp, by bound, ?_⟩
State after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ ∀ {w : ℂ}, Complex.abs (w - z) < r → Complex.abs (f w - f z) < e
Tactic:
intro w wr
State after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (f w - f z) < e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (f w - f z) < e
Tactic:
refine @sc w ?_
State after:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < s

State before:
case neg
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < s
Tactic:
trans r
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < r

f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ Complex.abs (w - z) < r

f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s
Tactic:
assumption
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
w : ℂ
wr : Complex.abs (w - z) < r
⊢ r < s
Tactic:
assumption
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ
fc : ContinuousAt f z
rp : 0 < r
e : ℝ
ep : 0 < e
s : ℝ
sp : s > 0
sc : ∀ {x : ℂ}, Complex.abs (x - z) < s → Complex.abs (f x - f z) < e
sr : r < s
⊢ r ≤ r
Tactic:
bound
State after:
no goals