Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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)