Theorem: cauchy2 (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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have h1 := fun z0 (z0m : z0 ∈ closedBall c0 r) ↦
  cauchy1 w1m (h.fc1 z0m) fun z1 z1m ↦ h.fd1 z0m (mem_open_closed z1m)
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have ic1 : ContinuousOn (fun z0 ↦ (2 * π * I : ℂ)⁻¹ • ∮ z1 in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1))
    (closedBall c0 r) :=
  (h.fc0 w1m).congr h1
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have id1 : DifferentiableOn ℂ (fun z0 ↦ (2 * π * I : ℂ)⁻¹ • ∮ z1 in C(c1, r), (z1 - w1)⁻¹
    • f (z0, z1)) (ball c0 r) := by
  rw [differentiableOn_congr fun z zs ↦ h1 z (mem_open_closed zs)]
  intro z0 z0m; apply DifferentiableAt.differentiableWithinAt
  exact h.fd0 (mem_open_closed z0m) (mem_open_closed w1m)
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
have h01 :=
  cauchy1 w0m ic1 fun z0 z0m ↦
    DifferentiableOn.differentiableAt id1 (IsOpen.mem_nhds isOpen_ball z0m)
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
h01 :
  ((2 * ↑π * I)⁻¹ •
      ∮ (z : ℂ) in C(c0, r), (z - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z, z1)) =
    (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (w0, z1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
id1 : DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
h01 :
  ((2 * ↑π * I)⁻¹ •
      ∮ (z : ℂ) in C(c0, r), (z - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z, z1)) =
    (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (w0, z1)
⊢ ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r), (z0 - w0)⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) =
    f (w0, w1)
Tactic:
exact _root_.trans h01 (h1 w0 (mem_open_closed w0m))
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ DifferentiableOn ℂ (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (ball c0 r)
Tactic:
rw [differentiableOn_congr fun z zs ↦ h1 z (mem_open_closed zs)]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ DifferentiableOn ℂ (fun z => f (z, w1)) (ball c0 r)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
⊢ DifferentiableOn ℂ (fun z => f (z, w1)) (ball c0 r)
Tactic:
intro z0 z0m
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableWithinAt ℂ (fun z => f (z, w1)) (ball c0 r) z0

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableWithinAt ℂ (fun z => f (z, w1)) (ball c0 r) z0
Tactic:
apply DifferentiableAt.differentiableWithinAt
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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableAt ℂ (fun z => f (z, w1)) z0

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 : ℝ
h : Separate f c0 c1 r b s
w0m : w0 ∈ ball c0 r
w1m : w1 ∈ ball c1 r
h1 : ∀ z0 ∈ closedBall c0 r, ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - w1)⁻¹ • f (z0, z)) = f (z0, w1)
ic1 : ContinuousOn (fun z0 => (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - w1)⁻¹ • f (z0, z1)) (closedBall c0 r)
z0 : ℂ
z0m : z0 ∈ ball c0 r
⊢ DifferentiableAt ℂ (fun z => f (z, w1)) z0
Tactic:
exact h.fd0 (mem_open_closed z0m) (mem_open_closed w1m)
State after:
no goals