Theorem: AnalyticOn.ball_subset_image_closedBall_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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
have fn : ∀ d, d ∈ u → ∃ᶠ w in 𝓝 z, f d w ≠ f d z := by
  refine fun d m ↦ (nontrivial_local_of_global (fa.along_snd.mono ?_) rp ep (ef d m)).nonconst
  simp only [← closedBall_prod_same, mem_prod_eq, setOf_mem_eq, iff_true_iff.mpr m,
    true_and_iff, subset_refl]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
have op : ∀ d, d ∈ u → ball (f d z) (e / 2) ⊆ f d '' closedBall z r := by
  intro d du; refine DiffContOnCl.ball_subset_image_closedBall ?_ rp (ef d du) (fn d du)
  have e : f d = uncurry f ∘ fun w ↦ (d, w) := rfl
  rw [e]; apply DifferentiableOn.diffContOnCl; apply AnalyticOn.differentiableOn
  refine fa.comp (analyticOn_const.prod (analyticOn_id _)) ?_
  intro w wr; simp only [closure_ball _ rp.ne'] at wr
  simp only [← closedBall_prod_same, mem_prod_eq, du, wr, true_and_iff, du]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
rcases Metric.continuousAt_iff.mp
    (fa (c, z) (mk_mem_prod (mem_of_mem_nhds un) (mem_closedBall_self rp.le))).continuousAt
    (e / 4) (by linarith) with
  ⟨s, sp, sh⟩
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r ∈ 𝓝 (c, f c z)
Tactic:
rw [mem_nhds_prod_iff]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ u_1 ∈ 𝓝 c, ∃ v ∈ 𝓝 (f c z), u_1 ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ u_1 ∈ 𝓝 c, ∃ v ∈ 𝓝 (f c z), u_1 ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
refine ⟨u ∩ ball c s, Filter.inter_mem un (Metric.ball_mem_nhds c (by linarith)), ?_⟩
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ v ∈ 𝓝 (f c z), (u ∩ ball c s) ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ ∃ v ∈ 𝓝 (f c z), (u ∩ ball c s) ×ˢ v ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
use ball (f c z) (e / 4), Metric.ball_mem_nhds _ (by linarith)
State after:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4) ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r

State before:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4) ⊆ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
intro ⟨d, w⟩ m
State after:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d, w) ∈ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4)
⊢ (d, w) ∈ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r

State before:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d, w) ∈ (u ∩ ball c s) ×ˢ ball (f c z) (e / 4)
⊢ (d, w) ∈ (fun p => (p.1, f p.1 p.2)) '' u ×ˢ closedBall z r
Tactic:
simp only [mem_inter_iff, mem_prod_eq, mem_image, @mem_ball _ _ c, lt_min_iff] at m op ⊢
State after:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)

State before:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
have wm : w ∈ ball (f d z) (e / 2) := by
  simp only [mem_ball] at m ⊢
  specialize @sh ⟨d, z⟩; simp only [Prod.dist_eq, dist_self, Function.uncurry] at sh
  specialize sh (max_lt m.1.2 sp); rw [dist_comm] at sh
  calc dist w (f d z)
    _ ≤ dist w (f c z) + dist (f c z) (f d z) := by bound
    _ < e / 4 + dist (f c z) (f d z) := by linarith [m.2]
    _ ≤ e / 4 + e / 4 := by linarith [sh]
    _ = e / 2 := by ring
State after:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)

State before:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
specialize op d m.1.1 wm
State after:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)

State before:
case right
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
rcases (mem_image _ _ _).mp op with ⟨y, yr, yw⟩
State after:
case right.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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
y : ℂ
yr : y ∈ closedBall z r
yw : f d y = w
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)

State before:
case right.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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
y : ℂ
yr : y ∈ closedBall z r
yw : f d y = w
⊢ ∃ x, (x.1 ∈ u ∧ x.2 ∈ closedBall z r) ∧ (x.1, f x.1 x.2) = (d, w)
Tactic:
use⟨d, y⟩
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
y : ℂ
yr : y ∈ closedBall z r
yw : f d y = w
⊢ ((d, y).1 ∈ u ∧ (d, y).2 ∈ closedBall z r) ∧ ((d, y).1, f (d, y).1 (d, y).2) = (d, w)

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
wm : w ∈ ball (f d z) (e / 2)
op : w ∈ f d '' closedBall z r
y : ℂ
yr : y ∈ closedBall z r
yw : f d y = w
⊢ ((d, y).1 ∈ u ∧ (d, y).2 ∈ closedBall z r) ∧ ((d, y).1, f (d, y).1 (d, y).2) = (d, w)
Tactic:
simp only [mem_prod_eq, Prod.ext_iff, yw, and_true_iff, eq_self_iff_true, true_and_iff, yr, m.1.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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
⊢ ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
Tactic:
refine fun d m ↦ (nontrivial_local_of_global (fa.along_snd.mono ?_) rp ep (ef d m)).nonconst
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
d : ℂ
m : d ∈ u
⊢ closedBall z r ⊆ {y | (d, y) ∈ u ×ˢ 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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
d : ℂ
m : d ∈ u
⊢ closedBall z r ⊆ {y | (d, y) ∈ u ×ˢ closedBall z r}
Tactic:
simp only [← closedBall_prod_same, mem_prod_eq, setOf_mem_eq, iff_true_iff.mpr m,
  true_and_iff, subset_refl]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
⊢ ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
Tactic:
intro d du
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
⊢ ball (f d z) (e / 2) ⊆ f d '' 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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
⊢ ball (f d z) (e / 2) ⊆ f d '' closedBall z r
Tactic:
refine DiffContOnCl.ball_subset_image_closedBall ?_ rp (ef d du) (fn d du)
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
⊢ DiffContOnCl ℂ (f d) (ball 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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
⊢ DiffContOnCl ℂ (f d) (ball z r)
Tactic:
have e : f d = uncurry f ∘ fun w ↦ (d, w) := rfl
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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (f d) (ball 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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (f d) (ball z r)
Tactic:
rw [e]
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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (uncurry f ∘ fun w => (d, w)) (ball 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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DiffContOnCl ℂ (uncurry f ∘ fun w => (d, w)) (ball z r)
Tactic:
apply DifferentiableOn.diffContOnCl
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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DifferentiableOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball 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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ DifferentiableOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))
Tactic:
apply AnalyticOn.differentiableOn
State after:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ AnalyticOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))

State before:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ AnalyticOn ℂ (uncurry f ∘ fun w => (d, w)) (closure (ball z r))
Tactic:
refine fa.comp (analyticOn_const.prod (analyticOn_id _)) ?_
State after:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ MapsTo (fun w => (d, w)) (closure (ball z r)) (u ×ˢ closedBall z r)

State before:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
⊢ MapsTo (fun w => (d, w)) (closure (ball z r)) (u ×ˢ closedBall z r)
Tactic:
intro w wr
State after:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closure (ball z r)
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r

State before:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closure (ball z r)
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r
Tactic:
simp only [closure_ball _ rp.ne'] at wr
State after:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closedBall z r
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r

State before:
case h.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 : ℂ
e✝ r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e✝
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e✝ ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
d : ℂ
du : d ∈ u
e : f d = uncurry f ∘ fun w => (d, w)
w : ℂ
wr : w ∈ closedBall z r
⊢ (fun w => (d, w)) w ∈ u ×ˢ closedBall z r
Tactic:
simp only [← closedBall_prod_same, mem_prod_eq, du, wr, true_and_iff, du]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
⊢ 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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ 0 < s
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
⊢ 0 < e / 4
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ w ∈ ball (f c z) (e / 4)
⊢ w ∈ ball (f d z) (e / 2)
Tactic:
simp only [mem_ball] at m ⊢
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
⊢ dist w (f d z) < e / 2

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
sh : ∀ {x : ℂ × ℂ}, dist x (c, z) < s → dist (uncurry f x) (uncurry f (c, z)) < e / 4
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
specialize @sh ⟨d, z⟩
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (d, z) (c, z) < s → dist (uncurry f (d, z)) (uncurry f (c, z)) < e / 4
⊢ dist w (f d z) < e / 2

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (d, z) (c, z) < s → dist (uncurry f (d, z)) (uncurry f (c, z)) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
simp only [Prod.dist_eq, dist_self, Function.uncurry] at sh
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : max (dist d c) 0 < s → dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : max (dist d c) 0 < s → dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
specialize sh (max_lt m.1.2 sp)
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f d z) (f c z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
rw [dist_comm] at sh
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f d z) < e / 2

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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f d z) < e / 2
Tactic:
calc dist w (f d z)
  _ ≤ dist w (f c z) + dist (f c z) (f d z) := by bound
  _ < e / 4 + dist (f c z) (f d z) := by linarith [m.2]
  _ ≤ e / 4 + e / 4 := by linarith [sh]
  _ = 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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f d z) ≤ dist w (f c z) + dist (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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ dist w (f c z) + dist (f c z) (f d z) < e / 4 + dist (f c z) (f d z)
Tactic:
linarith [m.2]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ e / 4 + dist (f c z) (f d z) ≤ e / 4 + e / 4
Tactic:
linarith [sh]
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 : ℂ
e r : ℝ
u : Set ℂ
fa : AnalyticOn ℂ (uncurry f) (u ×ˢ closedBall z r)
rp : 0 < r
ep : 0 < e
un : u ∈ 𝓝 c
ef : ∀ d ∈ u, ∀ w ∈ sphere z r, e ≤ ‖f d w - f d z‖
fn : ∀ d ∈ u, ∃ᶠ (w : ℂ) in 𝓝 z, f d w ≠ f d z
op : ∀ d ∈ u, ball (f d z) (e / 2) ⊆ f d '' closedBall z r
s : ℝ
sp : s > 0
d w : ℂ
m : (d ∈ u ∧ dist d c < s) ∧ dist w (f c z) < e / 4
sh : dist (f c z) (f d z) < e / 4
⊢ e / 4 + e / 4 = e / 2
Tactic:
ring
State after:
no goals