Theorem: analyticOn_small_cball (Ray/Analytic/Uniform.lean)

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
⊢ AnalyticOn ℂ f (closedBall z ↑s)
Tactic:
intro x hx
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ closedBall z ↑s
⊢ AnalyticAt ℂ f x

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ closedBall z ↑s
⊢ AnalyticAt ℂ f x
Tactic:
rw [closedBall] at hx
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ {y | dist y z ≤ ↑s}
⊢ AnalyticAt ℂ f x

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : x ∈ {y | dist y z ≤ ↑s}
⊢ AnalyticAt ℂ f x
Tactic:
simp at hx
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ AnalyticAt ℂ f x

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ AnalyticAt ℂ f x
Tactic:
have hb : x ∈ ball z r := by
  rw [ball]; simp only [dist_lt_coe, Set.mem_setOf_eq]; exact lt_of_le_of_lt hx sr
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
hb : x ∈ ball z ↑r
⊢ AnalyticAt ℂ f x

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
hb : x ∈ ball z ↑r
⊢ AnalyticAt ℂ f x
Tactic:
exact h x hb
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ x ∈ ball z ↑r
Tactic:
rw [ball]
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ x ∈ {y | dist y z < ↑r}

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ x ∈ {y | dist y z < ↑r}
Tactic:
simp only [dist_lt_coe, Set.mem_setOf_eq]
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ nndist x z < r

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
h : AnalyticOn ℂ f (ball z ↑r)
s : ℝ≥0
sr : s < r
x : ℂ
hx : nndist x z ≤ s
⊢ nndist x z < r
Tactic:
exact lt_of_le_of_lt hx sr
State after:
no goals