Theorem: ContinuousOn.inv_sphere_ball (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
⊢ ContinuousOn (fun z => (z - (c + w))⁻¹) (sphere c r)
Tactic:
refine ContinuousOn.inv₀ (ContinuousOn.sub continuousOn_id continuousOn_const) fun z zs ↦ ?_
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ z - (c + w) ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ z - (c + w) ≠ 0
Tactic:
rw [←Complex.abs.ne_zero_iff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ Complex.abs (z - (c + w)) ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
wr : w ∈ ball 0 r
z : ℂ
zs : z ∈ sphere c r
⊢ Complex.abs (z - (c + w)) ≠ 0
Tactic:
simp only [mem_ball_zero_iff, Complex.norm_eq_abs, mem_sphere_iff_norm] at zs wr
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - (c + w)) ≠ 0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - (c + w)) ≠ 0
Tactic:
apply ne_of_gt
State after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ 0 < Complex.abs (z - (c + w))

State before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ 0 < Complex.abs (z - (c + w))
Tactic:
calc abs (z - (c + w))
  _ = abs (z - c + -w) := by ring_nf
  _ ≥ abs (z - c) - abs (-w) := by bound
  _ = r - abs (-w) := by rw [zs]
  _ = r - abs w := by rw [Complex.abs.map_neg]
  _ > r - r := (sub_lt_sub_left wr _)
  _ = 0 := by ring
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - (c + w)) = Complex.abs (z - c + -w)
Tactic:
ring_nf
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - c + -w) ≥ Complex.abs (z - c) - Complex.abs (-w)
Tactic:
bound
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ Complex.abs (z - c) - Complex.abs (-w) = r - Complex.abs (-w)
Tactic:
rw [zs]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ r - Complex.abs (-w) = r - Complex.abs w
Tactic:
rw [Complex.abs.map_neg]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r✝ b : ℝ
c w : ℂ
r : ℝ
z : ℂ
zs : Complex.abs (z - c) = r
wr : Complex.abs w < r
⊢ r - r = 0
Tactic:
ring
State after:
no goals