Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param' (Ray/AnalyticManifold/OpenMapping.lean)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
⊢ 𝓝 (c, f c z) ≤ Filter.map (fun p => (p.1, f p.1 p.2)) (𝓝 (c, z))
Tactic:
rw [Filter.le_map_iff]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
⊢ ∀ s ∈ 𝓝 (c, z), (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
⊢ ∀ s ∈ 𝓝 (c, z), (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
intro s' sn
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
generalize hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
have ss : s ⊆ s' := by rw [← hs]; apply inter_subset_left
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
replace sn : s ∈ 𝓝 (c, z) := by rw [← hs]; exact Filter.inter_mem sn fa.eventually_analyticAt
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
replace fa : AnalyticOn ℂ (uncurry f) s := by rw [← hs]; apply inter_subset_right
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s' ∈ 𝓝 (c, f c z)
Tactic:
refine Filter.mem_of_superset ?_ (image_subset _ ss)
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
clear ss hs s'
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
rcases Metric.mem_nhds_iff.mp sn with ⟨e, ep, es⟩
State after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
er : ∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
rcases er with ⟨r, rp, rs, fr⟩
State after:
case intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
have fc : ContinuousOn (fun w ↦ ‖f c w - f c z‖) (sphere z r) := by
  apply ContinuousOn.norm; refine ContinuousOn.sub ?_ continuousOn_const
  apply fa.along_snd.continuousOn.mono; intro x xs; apply rs
  simp only [← closedBall_prod_same, mem_prod_eq]
  use Metric.mem_closedBall_self rp.le, Metric.sphere_subset_closedBall xs
State after:
case intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
rcases (isCompact_sphere _ _).exists_isMinOn (NormedSpace.sphere_nonempty.mpr rp.le) fc with
  ⟨x, xs, xm⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
generalize he : ‖f c x - f c z‖ = e
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
have ep : 0 < e := by
  contrapose fr
  simp only [norm_pos_iff, sub_ne_zero, not_not, mem_image, ← he] at fr ⊢
  use x, xs, fr
State after:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
rcases Metric.uniformContinuousOn_iff.mp
    ((isCompact_closedBall _ _).uniformContinuousOn_of_continuous (fa.continuousOn.mono rs))
    (e / 4) (by linarith) with
  ⟨t, tp, ft⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
have ef : ∀ d, d ∈ ball c (min t r) → ∀ w, w ∈ sphere z r → e / 2 ≤ ‖f d w - f d z‖ := by
  intro d dt w wr; simp only [Complex.norm_eq_abs]
  simp only [Complex.dist_eq, Prod.forall, mem_closedBall, Prod.dist_eq, max_le_iff, max_lt_iff,
    Function.uncurry, and_imp] at ft
  simp only [mem_ball, Complex.dist_eq, lt_min_iff] at dt
  have a1 : abs (f d w - f c w) ≤ e / 4 :=
    (ft d w dt.2.le (le_of_eq wr) c w (abs_sub_self_lt rp).le (le_of_eq wr) dt.1
      (abs_sub_self_lt tp)).le
  have a2 : abs (f c z - f d z) ≤ e / 4 := by
    refine (ft c z (abs_sub_self_lt rp).le (abs_sub_self_lt rp).le d z
        dt.2.le (abs_sub_self_lt rp).le ?_ (abs_sub_self_lt tp)).le
    rw [← neg_sub, Complex.abs.map_neg]; exact dt.1
  calc abs (f d w - f d z)
    _ = abs (f c w - f c z + (f d w - f c w) + (f c z - f d z)) := by ring_nf
    _ ≥ abs (f c w - f c z + (f d w - f c w)) - abs (f c z - f d z) := by bound
    _ ≥ abs (f c w - f c z) - abs (f d w - f c w) - abs (f c z - f d z) := by bound
    _ ≥ e - e / 4 - e / 4 := by rw [← he] at a1 a2 ⊢; exact sub_le_sub (sub_le_sub (xm wr) a1) a2
    _ = e / 2 := by ring
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
have ss : ball c (min t r) ×ˢ closedBall z r ⊆ s := by
  refine _root_.trans ?_ rs; rw [← closedBall_prod_same]; apply prod_mono_left
  exact _root_.trans (Metric.ball_subset_ball (min_le_right _ _)) Metric.ball_subset_closedBall
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
ss : ball c (min t r) ×ˢ closedBall z r ⊆ s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
ss : ball c (min t r) ×ˢ closedBall z r ⊆ s
⊢ (fun p => (p.1, f p.1 p.2)) '' s ∈ 𝓝 (c, f c z)
Tactic:
exact Filter.mem_of_superset ((fa.mono ss).ball_subset_image_closedBall_param rp (half_pos ep)
  (Metric.ball_mem_nhds _ (by bound)) ef) (image_subset _ ss)
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ s ⊆ s'
Tactic:
rw [← hs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ s' ∩ {p | AnalyticAt ℂ (uncurry f) p} ⊆ s'

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
⊢ s' ∩ {p | AnalyticAt ℂ (uncurry f) p} ⊆ s'
Tactic:
apply inter_subset_left
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ s ∈ 𝓝 (c, z)
Tactic:
rw [← hs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ s' ∩ {p | AnalyticAt ℂ (uncurry f) p} ∈ 𝓝 (c, z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' : Set (ℂ × ℂ)
sn : s' ∈ 𝓝 (c, z)
s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
⊢ s' ∩ {p | AnalyticAt ℂ (uncurry f) p} ∈ 𝓝 (c, z)
Tactic:
exact Filter.inter_mem sn fa.eventually_analyticAt
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ AnalyticOn ℂ (uncurry f) s
Tactic:
rw [← hs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ AnalyticOn ℂ (uncurry f) (s' ∩ {p | AnalyticAt ℂ (uncurry f) p})

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
fa : AnalyticAt ℂ (uncurry f) (c, z)
s' s : Set (ℂ × ℂ)
hs : s' ∩ {p | AnalyticAt ℂ (uncurry f) p} = s
ss : s ⊆ s'
sn : s ∈ 𝓝 (c, z)
⊢ AnalyticOn ℂ (uncurry f) (s' ∩ {p | AnalyticAt ℂ (uncurry f) p})
Tactic:
apply inter_subset_right
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
⊢ ∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r
Tactic:
have h := n.eventually_ne
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z
⊢ ∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z
⊢ ∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r
Tactic:
contrapose h
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ¬∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r
⊢ ¬∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ¬∃ r, 0 < r ∧ closedBall (c, z) r ⊆ s ∧ f c z ∉ f c '' sphere z r
⊢ ¬∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z
Tactic:
simp only [not_exists, Filter.not_frequently, not_not, not_and, not_exists] at h
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ¬∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ¬∀ᶠ (w : ℂ) in 𝓝 z, w ≠ z → f c w ≠ f c z
Tactic:
simp only [Filter.not_eventually, _root_.not_imp, not_not, Filter.eventually_iff,
  Metric.mem_nhds_iff, not_exists, not_subset, mem_setOf, not_and]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ∀ x > 0, ∃ a ∈ ball z x, a ≠ z ∧ f c a = f c z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
⊢ ∀ x > 0, ∃ a ∈ ball z x, a ≠ z ∧ f c a = f c z
Tactic:
intro r rp
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Tactic:
specialize h (min (e/2) (r/2)) ?_ ?_
State after:
case specialize_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ 0 < min (e / 2) (r / 2)

case specialize_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ closedBall (c, z) (min (e / 2) (r / 2)) ⊆ s

X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z

State before:
case specialize_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ 0 < min (e / 2) (r / 2)
Tactic:
bound
State after:
no goals

State before:
case specialize_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
h : ∀ (x : ℝ), 0 < x → closedBall (c, z) x ⊆ s → f c z ∈ f c '' sphere z x
r : ℝ
rp : r > 0
⊢ closedBall (c, z) (min (e / 2) (r / 2)) ⊆ s
Tactic:
exact _root_.trans (Metric.closedBall_subset_ball (lt_of_le_of_lt (min_le_left _ _)
  (half_lt_self ep))) es
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Tactic:
rcases (mem_image _ _ _).mp h with ⟨w, ws, wz⟩
State after:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z

State before:
case intro.intro
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ ∃ a ∈ ball z r, a ≠ z ∧ f c a = f c z
Tactic:
use w
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r ∧ w ≠ z ∧ f c w = f c z

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r ∧ w ≠ z ∧ f c w = f c z
Tactic:
refine ⟨?_, ?_, wz⟩
State after:
case h.refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r

case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ≠ z

State before:
case h.refine_1
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ∈ ball z r
Tactic:
exact Metric.closedBall_subset_ball (lt_of_le_of_lt (min_le_right _ _) (half_lt_self rp))
  (Metric.sphere_subset_closedBall ws)
State after:
no goals

State before:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
ws : w ∈ sphere z (min (e / 2) (r / 2))
wz : f c w = f c z
⊢ w ≠ z
Tactic:
contrapose ws
State after:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : ¬w ≠ z
⊢ w ∉ sphere z (min (e / 2) (r / 2))

State before:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : ¬w ≠ z
⊢ w ∉ sphere z (min (e / 2) (r / 2))
Tactic:
simp only [not_not] at ws
State after:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ w ∉ sphere z (min (e / 2) (r / 2))

State before:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ w ∉ sphere z (min (e / 2) (r / 2))
Tactic:
simp only [ws, Metric.mem_sphere, dist_self]
State after:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ ¬0 = min (e / 2) (r / 2)

State before:
case h.refine_2
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ ¬0 = min (e / 2) (r / 2)
Tactic:
exact ne_of_lt (by bound)
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : r > 0
h : f c z ∈ f c '' sphere z (min (e / 2) (r / 2))
w : ℂ
wz : f c w = f c z
ws : w = z
⊢ 0 < min (e / 2) (r / 2)
Tactic:
bound
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
Tactic:
apply ContinuousOn.norm
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ ContinuousOn (fun x => f c x - f c z) (sphere z r)

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ ContinuousOn (fun x => f c x - f c z) (sphere z r)
Tactic:
refine ContinuousOn.sub ?_ continuousOn_const
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ ContinuousOn (fun x => f c x) (sphere z r)

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ ContinuousOn (fun x => f c x) (sphere z r)
Tactic:
apply fa.along_snd.continuousOn.mono
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ sphere z r ⊆ {y | (c, y) ∈ s}

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
⊢ sphere z r ⊆ {y | (c, y) ∈ s}
Tactic:
intro x xs
State after:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
x : ℂ
xs : x ∈ sphere z r
⊢ x ∈ {y | (c, y) ∈ s}

State before:
case h
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
x : ℂ
xs : x ∈ sphere z r
⊢ x ∈ {y | (c, y) ∈ s}
Tactic:
apply rs
State after:
case h.a
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
x : ℂ
xs : x ∈ sphere z r
⊢ (c, x) ∈ closedBall (c, z) r

State before:
case h.a
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
x : ℂ
xs : x ∈ sphere z r
⊢ (c, x) ∈ closedBall (c, z) r
Tactic:
simp only [← closedBall_prod_same, mem_prod_eq]
State after:
case h.a
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
x : ℂ
xs : x ∈ sphere z r
⊢ c ∈ closedBall c r ∧ x ∈ closedBall z r

State before:
case h.a
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e : ℝ
ep : e > 0
es : ball (c, z) e ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
x : ℂ
xs : x ∈ sphere z r
⊢ c ∈ closedBall c r ∧ x ∈ closedBall z r
Tactic:
use Metric.mem_closedBall_self rp.le, Metric.sphere_subset_closedBall xs
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
⊢ 0 < e
Tactic:
contrapose fr
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
fr : ¬0 < e
⊢ ¬f c z ∉ f c '' sphere z r

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
fr : ¬0 < e
⊢ ¬f c z ∉ f c '' sphere z r
Tactic:
simp only [norm_pos_iff, sub_ne_zero, not_not, mem_image, ← he] at fr ⊢
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
fr : f c x = f c z
⊢ ∃ x ∈ sphere z r, f c x = f c z

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
fr : f c x = f c z
⊢ ∃ x ∈ sphere z r, f c x = f c z
Tactic:
use x, xs, fr
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
⊢ e / 4 > 0
Tactic:
linarith
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
⊢ ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
Tactic:
intro d dt w wr
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
d : ℂ
dt : d ∈ ball c (min t r)
w : ℂ
wr : w ∈ sphere z r
⊢ e / 2 ≤ ‖f d w - f d z‖

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
d : ℂ
dt : d ∈ ball c (min t r)
w : ℂ
wr : w ∈ sphere z r
⊢ e / 2 ≤ ‖f d w - f d z‖
Tactic:
simp only [Complex.norm_eq_abs]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
d : ℂ
dt : d ∈ ball c (min t r)
w : ℂ
wr : w ∈ sphere z r
⊢ e / 2 ≤ Complex.abs (f d w - f d z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
d : ℂ
dt : d ∈ ball c (min t r)
w : ℂ
wr : w ∈ sphere z r
⊢ e / 2 ≤ Complex.abs (f d w - f d z)
Tactic:
simp only [Complex.dist_eq, Prod.forall, mem_closedBall, Prod.dist_eq, max_le_iff, max_lt_iff,
  Function.uncurry, and_imp] at ft
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d : ℂ
dt : d ∈ ball c (min t r)
w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
⊢ e / 2 ≤ Complex.abs (f d w - f d z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d : ℂ
dt : d ∈ ball c (min t r)
w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
⊢ e / 2 ≤ Complex.abs (f d w - f d z)
Tactic:
simp only [mem_ball, Complex.dist_eq, lt_min_iff] at dt
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
⊢ e / 2 ≤ Complex.abs (f d w - f d z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
⊢ e / 2 ≤ Complex.abs (f d w - f d z)
Tactic:
have a1 : abs (f d w - f c w) ≤ e / 4 :=
  (ft d w dt.2.le (le_of_eq wr) c w (abs_sub_self_lt rp).le (le_of_eq wr) dt.1
    (abs_sub_self_lt tp)).le
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ e / 2 ≤ Complex.abs (f d w - f d z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ e / 2 ≤ Complex.abs (f d w - f d z)
Tactic:
have a2 : abs (f c z - f d z) ≤ e / 4 := by
  refine (ft c z (abs_sub_self_lt rp).le (abs_sub_self_lt rp).le d z
      dt.2.le (abs_sub_self_lt rp).le ?_ (abs_sub_self_lt tp)).le
  rw [← neg_sub, Complex.abs.map_neg]; exact dt.1
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ e / 2 ≤ Complex.abs (f d w - f d z)

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ e / 2 ≤ Complex.abs (f d w - f d z)
Tactic:
calc abs (f d w - f d z)
  _ = abs (f c w - f c z + (f d w - f c w) + (f c z - f d z)) := by ring_nf
  _ ≥ abs (f c w - f c z + (f d w - f c w)) - abs (f c z - f d z) := by bound
  _ ≥ abs (f c w - f c z) - abs (f d w - f c w) - abs (f c z - f d z) := by bound
  _ ≥ e - e / 4 - e / 4 := by rw [← he] at a1 a2 ⊢; exact sub_le_sub (sub_le_sub (xm wr) a1) a2
  _ = e / 2 := by ring
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ Complex.abs (f c z - f d z) ≤ e / 4
Tactic:
refine (ft c z (abs_sub_self_lt rp).le (abs_sub_self_lt rp).le d z
    dt.2.le (abs_sub_self_lt rp).le ?_ (abs_sub_self_lt tp)).le
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ Complex.abs (c - d) < t

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ Complex.abs (c - d) < t
Tactic:
rw [← neg_sub, Complex.abs.map_neg]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ Complex.abs (d - c) < t

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
⊢ Complex.abs (d - c) < t
Tactic:
exact dt.1
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ Complex.abs (f d w - f d z) = Complex.abs (f c w - f c z + (f d w - f c w) + (f c z - f d z))
Tactic:
ring_nf
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ Complex.abs (f c w - f c z + (f d w - f c w) + (f c z - f d z)) ≥
    Complex.abs (f c w - f c z + (f d w - f c w)) - Complex.abs (f c z - f d z)
Tactic:
bound
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ Complex.abs (f c w - f c z + (f d w - f c w)) - Complex.abs (f c z - f d z) ≥
    Complex.abs (f c w - f c z) - Complex.abs (f d w - f c w) - Complex.abs (f c z - f d z)
Tactic:
bound
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ Complex.abs (f c w - f c z) - Complex.abs (f d w - f c w) - Complex.abs (f c z - f d z) ≥ e - e / 4 - e / 4
Tactic:
rw [← he] at a1 a2 ⊢
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ ‖f c x - f c z‖ / 4
a2 : Complex.abs (f c z - f d z) ≤ ‖f c x - f c z‖ / 4
⊢ Complex.abs (f c w - f c z) - Complex.abs (f d w - f c w) - Complex.abs (f c z - f d z) ≥
    ‖f c x - f c z‖ - ‖f c x - f c z‖ / 4 - ‖f c x - f c z‖ / 4

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ ‖f c x - f c z‖ / 4
a2 : Complex.abs (f c z - f d z) ≤ ‖f c x - f c z‖ / 4
⊢ Complex.abs (f c w - f c z) - Complex.abs (f d w - f c w) - Complex.abs (f c z - f d z) ≥
    ‖f c x - f c z‖ - ‖f c x - f c z‖ / 4 - ‖f c x - f c z‖ / 4
Tactic:
exact sub_le_sub (sub_le_sub (xm wr) a1) a2
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
d w : ℂ
wr : w ∈ sphere z r
ft :
  ∀ (a b : ℂ),
    Complex.abs (a - c) ≤ r →
      Complex.abs (b - z) ≤ r →
        ∀ (a_3 b_1 : ℂ),
          Complex.abs (a_3 - c) ≤ r →
            Complex.abs (b_1 - z) ≤ r →
              Complex.abs (a - a_3) < t → Complex.abs (b - b_1) < t → Complex.abs (f a b - f a_3 b_1) < e / 4
dt : Complex.abs (d - c) < t ∧ Complex.abs (d - c) < r
a1 : Complex.abs (f d w - f c w) ≤ e / 4
a2 : Complex.abs (f c z - f d z) ≤ e / 4
⊢ e - e / 4 - e / 4 = e / 2
Tactic:
ring
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ×ˢ closedBall z r ⊆ s
Tactic:
refine _root_.trans ?_ rs
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ×ˢ closedBall z r ⊆ closedBall (c, z) r

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ×ˢ closedBall z r ⊆ closedBall (c, z) r
Tactic:
rw [← closedBall_prod_same]
State after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ×ˢ closedBall z r ⊆ closedBall c r ×ˢ closedBall z r

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ×ˢ closedBall z r ⊆ closedBall c r ×ˢ closedBall z r
Tactic:
apply prod_mono_left
State after:
case hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ⊆ closedBall c r

State before:
case hs
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
⊢ ball c (min t r) ⊆ closedBall c r
Tactic:
exact _root_.trans (Metric.ball_subset_ball (min_le_right _ _)) Metric.ball_subset_closedBall
State after:
no goals

State before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ → ℂ
c z : ℂ
n : NontrivialHolomorphicAt (f c) z
s : Set (ℂ × ℂ)
sn : s ∈ 𝓝 (c, z)
fa : AnalyticOn ℂ (uncurry f) s
e✝ : ℝ
ep✝ : e✝ > 0
es : ball (c, z) e✝ ⊆ s
r : ℝ
rp : 0 < r
rs : closedBall (c, z) r ⊆ s
fr : f c z ∉ f c '' sphere z r
fc : ContinuousOn (fun w => ‖f c w - f c z‖) (sphere z r)
x : ℂ
xs : x ∈ sphere z r
xm : IsMinOn (fun w => ‖f c w - f c z‖) (sphere z r) x
e : ℝ
he : ‖f c x - f c z‖ = e
ep : 0 < e
t : ℝ
tp : t > 0
ft : ∀ x ∈ closedBall (c, z) r, ∀ y ∈ closedBall (c, z) r, dist x y < t → dist (uncurry f x) (uncurry f y) < e / 4
ef : ∀ d ∈ ball c (min t r), ∀ w ∈ sphere z r, e / 2 ≤ ‖f d w - f d z‖
ss : ball c (min t r) ×ˢ closedBall z r ⊆ s
⊢ 0 < min t r
Tactic:
bound
State after:
no goals