internlm/Lean-Github huggingface dataset:
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
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
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
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
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
⊢ Complex.abs (c - d) < t
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
⊢ Complex.abs (c - d) < t
Tactic:
rw [← neg_sub, Complex.abs.map_neg]
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
⊢ Complex.abs (d - c) < t
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
⊢ Complex.abs (d - c) < t
Tactic:
exact dt.1
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
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
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
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
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
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
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
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 ⊢
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) ≤ ‖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
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) ≤ ‖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
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
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
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
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
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
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
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
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]
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
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