Theorem: ContinuousOn.cauchy1 (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 : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun z0 => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)) (sphere c0 r)
Tactic:
apply ContinuousOn.circleIntegral rp (isCompact_sphere _ _)
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (uncurry fun z0 z1 => (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)) (sphere c0 r ×ˢ sphere c1 r)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (uncurry fun z0 z1 => (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.smul
State after:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ ^ n1) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ ^ n1) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.pow
State after:
case hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.inv₀
State after:
case hf.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply Continuous.continuousOn
State after:
case hf.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact Continuous.sub (Continuous.snd continuous_id) continuous_const
State after:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
intro x xp
State after:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact center_not_in_sphere rp (Set.mem_prod.mp xp).right
State after:
case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹ • f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.smul
State after:
case hg.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => (x.2 - c1)⁻¹) (sphere c0 r ×ˢ sphere c1 r)

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.inv₀
State after:
case hg.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hf.hf
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => x.2 - c1) (sphere c0 r ×ˢ sphere c1 r)

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply Continuous.continuousOn
State after:
case hg.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hf.hf.h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ Continuous fun x => x.2 - c1

case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact Continuous.sub (Continuous.snd continuous_id) continuous_const
State after:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ∀ x ∈ sphere c0 r ×ˢ sphere c1 r, x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
intro x xp
State after:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hf.h0
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
x : ℂ × ℂ
xp : x ∈ sphere c0 r ×ˢ sphere c1 r
⊢ x.2 - c1 ≠ 0

case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact center_not_in_sphere rp (Set.mem_prod.mp xp).right
State after:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f (x.1, x.2)) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
simp
State after:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f x) (sphere c0 r ×ˢ sphere c1 r)

State before:
case hg.hg
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
n1 : ℕ
rp : r > 0
fc : ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
⊢ ContinuousOn (fun x => f x) (sphere c0 r ×ˢ sphere c1 r)
Tactic:
exact fc
State after:
no goals