Theorem: IsPreconnected.ball_diff_center (Ray/AnalyticManifold/Nonseparating.lean)

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
⊢ IsPreconnected (ball a r \ {a})
Tactic:
by_cases rp : r ≤ 0
State after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

State before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Tactic:
simp only [Metric.ball_eq_empty.mpr rp, empty_diff]
State after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected ∅

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

State before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : r ≤ 0
⊢ IsPreconnected ∅

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Tactic:
exact isPreconnected_empty
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : ¬r ≤ 0
⊢ IsPreconnected (ball a r \ {a})
Tactic:
simp only [not_le] at rp
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ IsPreconnected (ball a r \ {a})

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected (ball a r \ {a})
Tactic:
rw [e]
State after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected ((fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ)

State before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected ((fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ)
Tactic:
apply IsPreconnected.image
State after:
case neg.H
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected (Ioo 0 r ×ˢ univ)

case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)

State before:
case neg.H
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ IsPreconnected (Ioo 0 r ×ˢ univ)

case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)
Tactic:
exact isPreconnected_Ioo.prod isPreconnected_univ
State after:
case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)

State before:
case neg.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ ContinuousOn (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) (Ioo 0 r ×ˢ univ)
Tactic:
apply Continuous.continuousOn
State after:
case neg.hf.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ Continuous fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp

State before:
case neg.hf.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
e : ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
⊢ Continuous fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp
Tactic:
continuity
State after:
no goals

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ ball a r \ {a} = (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Tactic:
apply Set.ext
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ ∀ (x : ℂ), x ∈ ball a r \ {a} ↔ x ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
⊢ ∀ (x : ℂ), x ∈ ball a r \ {a} ↔ x ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Tactic:
intro z
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ z ∈ ball a r \ {a} ↔ z ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ z ∈ ball a r \ {a} ↔ z ∈ (fun p => a + ↑p.1 * (↑p.2 * Complex.I).exp) '' Ioo 0 r ×ˢ univ
Tactic:
simp only [mem_diff, mem_ball, Complex.dist_eq, mem_singleton_iff, mem_image, Prod.exists,
  mem_prod_eq, mem_Ioo, mem_univ, and_true_iff]
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a ↔ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a ↔ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z
Tactic:
constructor
State after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a → ∃ a_2 b, (0 < a_2 ∧ a_2 < r) ∧ a + ↑a_2 * (↑b * Complex.I).exp = z

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ (∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z) → Complex.abs (z - a) < r ∧ ¬z = a

State before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ Complex.abs (z - a) < r ∧ ¬z = a → ∃ a_2 b, (0 < a_2 ∧ a_2 < r) ∧ a + ↑a_2 * (↑b * Complex.I).exp = z
Tactic:
intro ⟨zr, za⟩
State after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z

State before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ ∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z
Tactic:
use abs (z - a), Complex.arg (z - a)
State after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ (0 < Complex.abs (z - a) ∧ Complex.abs (z - a) < r) ∧ a + ↑(Complex.abs (z - a)) * (↑(z - a).arg * Complex.I).exp = z

State before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
zr : Complex.abs (z - a) < r
za : ¬z = a
⊢ (0 < Complex.abs (z - a) ∧ Complex.abs (z - a) < r) ∧ a + ↑(Complex.abs (z - a)) * (↑(z - a).arg * Complex.I).exp = z
Tactic:
simp only [AbsoluteValue.pos_iff, Ne, Complex.abs_mul_exp_arg_mul_I,
  add_sub_cancel, eq_self_iff_true, sub_eq_zero, za, zr, not_false_iff, and_true_iff]
State after:
no goals

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
⊢ (∃ a_1 b, (0 < a_1 ∧ a_1 < r) ∧ a + ↑a_1 * (↑b * Complex.I).exp = z) → Complex.abs (z - a) < r ∧ ¬z = a
Tactic:
intro ⟨s, t, ⟨s0, sr⟩, e⟩
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ Complex.abs (z - a) < r ∧ ¬z = a

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ Complex.abs (z - a) < r ∧ ¬z = a
Tactic:
simp only [← e, add_sub_cancel_left, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos s0,
  Complex.abs_exp_ofReal_mul_I, mul_one, sr, true_and_iff, add_right_eq_self, mul_eq_zero,
  Complex.exp_ne_zero, or_false_iff, Complex.ofReal_eq_zero]
State after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ ¬s = 0

State before:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
S : Type
inst✝² : TopologicalSpace S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
a : ℂ
r : ℝ
rp : 0 < r
z : ℂ
s t : ℝ
s0 : 0 < s
sr : s < r
e : a + ↑s * (↑t * Complex.I).exp = z
⊢ ¬s = 0
Tactic:
exact s0.ne'
State after:
no goals