Theorem: cauchy2_hasSum_n1n0 (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 0 r
w1m : w1 ∈ ball 0 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Tactic:
have cw0m : c0 + w0 ∈ ball c0 r := by
  simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, Complex.dist_eq,
    sub_zero] using w0m
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + 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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Tactic:
have cw1m : c1 + w1 ∈ ball c1 r := by
  simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, dist_zero_right] using 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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + 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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum (fun n1 => w1 ^ n1 • h.series2CoeffN0Sum n1 w0) (f (c0 + w0, c1 + w1))
Tactic:
simp_rw [Separate.series2CoeffN0Sum]
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (f (c0 + w0, c1 + 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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (f (c0 + w0, c1 + w1))
Tactic:
rw [← cauchy2 h cw0m cw1m]
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r),
        (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        (2 * ↑π * I)⁻¹ •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    ((2 * ↑π * I)⁻¹ •
      ∮ (z0 : ℂ) in C(c0, r),
        (z0 - (c0 + w0))⁻¹ • (2 * ↑π * I)⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
generalize hs : (2 * ↑π * I)⁻¹ = s
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        s •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      w1 ^ n1 •
        s •
          ∮ (z0 : ℂ) in C(c0, r),
            (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [smul_comm _ s _]
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      s •
        w1 ^ n1 •
          ∮ (z0 : ℂ) in C(c0, r),
            s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun n1 =>
      s •
        w1 ^ n1 •
          ∮ (z0 : ℂ) in C(c0, r),
            s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n1 • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
apply HasSum.const_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 : ℝ
h : Separate f c0 c1 r b s✝
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      w1 ^ i •
        ∮ (z0 : ℂ) in C(c0, r),
          s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

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 : ℝ
h : Separate f c0 c1 r b s✝
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      w1 ^ i •
        ∮ (z0 : ℂ) in C(c0, r),
          s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [← circleIntegral.integral_smul (w1 ^ _) _ _ _]
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 : ℝ
h : Separate f c0 c1 r b s✝
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      ∮ (z : ℂ) in C(c0, r),
        w1 ^ i • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

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 : ℝ
h : Separate f c0 c1 r b s✝
w0m : w0 ∈ ball 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ HasSum
    (fun i =>
      ∮ (z : ℂ) in C(c0, r),
        w1 ^ i • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z, z1))
    (∮ (z0 : ℂ) in C(c0, r), s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
apply sum_integral_commute (fun n ↦ (r - abs w0)⁻¹ * b * (abs w1 / r) ^ n) h.rp
State after:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ContinuousOn
      (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (sphere c0 r)

case hf.fb
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ∀ z ∈ sphere c0 r,
      ‖w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
        (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

case hf.bs
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ Summable fun n => (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ z ∈ sphere c0 r,
    HasSum (fun n => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z, z1))

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 0 r
w1m : w1 ∈ ball 0 r
⊢ c0 + w0 ∈ ball c0 r
Tactic:
simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, Complex.dist_eq,
  sub_zero] using 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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
⊢ c1 + w1 ∈ ball c1 r
Tactic:
simpa only [Metric.mem_ball, dist_self_add_left, Complex.norm_eq_abs, dist_zero_right] using w1m
State after:
no goals

State before:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ContinuousOn
      (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (sphere c0 r)
Tactic:
intro n
State after:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn
    (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
    (sphere c0 r)

State before:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn
    (fun z => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
    (sphere c0 r)
Tactic:
apply ContinuousOn.smul continuousOn_const
State after:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => s • (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)

State before:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => s • (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)
Tactic:
apply ContinuousOn.smul continuousOn_const
State after:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)

State before:
case hf.fc
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1))
    (sphere c0 r)
Tactic:
apply ContinuousOn.smul
State after:
case hf.fc.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹) (sphere c0 r)

case hf.fc.hg
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1)) (sphere c0 r)

State before:
case hf.fc.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => (x - (c0 + w0))⁻¹) (sphere c0 r)

case hf.fc.hg
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1)) (sphere c0 r)
Tactic:
exact ContinuousOn.inv_sphere_ball w0m
State after:
case hf.fc.hg
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1)) (sphere c0 r)

State before:
case hf.fc.hg
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn (fun x => ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (x, z1)) (sphere c0 r)
Tactic:
apply ContinuousOn.cauchy1 h.rp
State after:
case hf.fc.hg
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)

State before:
case hf.fc.hg
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
n : ℕ
⊢ ContinuousOn f (sphere c0 r ×ˢ sphere c1 r)
Tactic:
apply ContinuousOn.mono h.fc h.rs'
State after:
no goals

State before:
case hf.fb
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ∀ z ∈ sphere c0 r,
      ‖w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
        (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
rw [← hs]
State after:
case hf.fb
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ∀ z ∈ sphere c0 r,
      ‖w1 ^ n •
            (2 * ↑π * I)⁻¹ • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
        (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n

State before:
case hf.fb
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ (n : ℕ),
    ∀ z ∈ sphere c0 r,
      ‖w1 ^ n •
            (2 * ↑π * I)⁻¹ • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1)‖ ≤
        (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
exact fun n z0 z0s ↦ cauchy2_hasSum_n1n0_bound h w0m n z0s
State after:
no goals

State before:
case hf.bs
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ Summable fun n => (r - Complex.abs w0)⁻¹ * b * (Complex.abs w1 / r) ^ n
Tactic:
apply Summable.mul_left
State after:
case hf.bs.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ Summable fun i => (Complex.abs w1 / r) ^ i

State before:
case hf.bs.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ Summable fun i => (Complex.abs w1 / r) ^ i
Tactic:
apply summable_geometric_of_abs_lt_one
State after:
case hf.bs.hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ |Complex.abs w1 / r| < 1

State before:
case hf.bs.hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ |Complex.abs w1 / r| < 1
Tactic:
rw [abs_div, abs_of_pos h.rp]
State after:
case hf.bs.hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ |Complex.abs w1| / r < 1

State before:
case hf.bs.hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ |Complex.abs w1| / r < 1
Tactic:
simp at w1m ⊢
State after:
case hf.bs.hf.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 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
w1m : Complex.abs w1 < r
⊢ Complex.abs w1 / r < 1

State before:
case hf.bs.hf.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 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
w1m : Complex.abs w1 < r
⊢ Complex.abs w1 / r < 1
Tactic:
exact (div_lt_one h.rp).mpr w1m
State after:
no goals

State before:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
⊢ ∀ z ∈ sphere c0 r,
    HasSum (fun n => w1 ^ n • s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z, z1))
      (s • (z - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z, z1))
Tactic:
intro z0 z0s
State after:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    (s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    (s • (z0 - (c0 + w0))⁻¹ • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [smul_comm s _]
State after:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => w1 ^ n • (z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [smul_comm (w1 ^ _) _]
State after:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => (z0 - (c0 + w0))⁻¹ • s • w1 ^ n • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun n => (z0 - (c0 + w0))⁻¹ • s • w1 ^ n • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ n • (z1 - c1)⁻¹ • f (z0, z1))
    ((z0 - (c0 + w0))⁻¹ • s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
apply HasSum.const_smul
State after:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
have fcs : ContinuousOn (fun z1 ↦ f (z0, z1)) (sphere c1 r) :=
  ContinuousOn.mono (h.fc1 (Metric.sphere_subset_closedBall z0s))
    Metric.sphere_subset_closedBall
State after:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
have hs1 := cauchy1_hasSum h.rp fcs w1m
State after:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => w1 ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => w1 ^ n • (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
simp_rw [hs, smul_comm _ s] at hs1
State after:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => s • w1 ^ n • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    (s • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))

State before:
case hf.h.hf
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 0 r
w1m : w1 ∈ ball 0 r
cw0m : c0 + w0 ∈ ball c0 r
cw1m : c1 + w1 ∈ ball c1 r
s : ℂ
hs : (2 * ↑π * I)⁻¹ = s
z0 : ℂ
z0s : z0 ∈ sphere c0 r
fcs : ContinuousOn (fun z1 => f (z0, z1)) (sphere c1 r)
hs1 :
  HasSum (fun n => s • w1 ^ n • ∮ (z : ℂ) in C(c1, r), (z - c1)⁻¹ ^ n • (z - c1)⁻¹ • f (z0, z))
    (s • ∮ (z : ℂ) in C(c1, r), (z - (c1 + w1))⁻¹ • f (z0, z))
⊢ HasSum (fun i => s • w1 ^ i • ∮ (z1 : ℂ) in C(c1, r), (z1 - c1)⁻¹ ^ i • (z1 - c1)⁻¹ • f (z0, z1))
    (s • ∮ (z1 : ℂ) in C(c1, r), (z1 - (c1 + w1))⁻¹ • f (z0, z1))
Tactic:
assumption
State after:
no goals