internlm/Lean-Github huggingface dataset:
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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]
Proof 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
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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 ⊢
Proof 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
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof state after:
no goals
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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‖
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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]
Proof 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)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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)
Theorem: NontrivialHolomorphicAt.nhds_le_map_nhds_param'
Proof 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
Proof 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)