Theorem: cindex_eq_order_aux (RMT4/cindex.lean)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
⊢ cindex z₀ r f = c
Tactic:
have e2 : sphere z₀ r ⊆ U := sphere_subset_closedBall.trans h0
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
⊢ cindex z₀ r f = c

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
⊢ cindex z₀ r f = c
Tactic:
have e4 : (∮ z in C(z₀,r), deriv f z / f z) = ∮ z in C(z₀,r), c / (z - z₀) + deriv g z / g z :=
  circleIntegral.integral_congr hr.le (λ z hz => h3 hz)
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ cindex z₀ r f = c

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
⊢ cindex z₀ r f = c
Tactic:
have e6 : (∮ z in C(z₀, r), deriv g z / g z) = 0 := by
  have := cindex_eq_zero hU hr h0 h1 h2
  simpa [cindex, Real.pi_ne_zero, I_ne_zero] using this
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
⊢ cindex z₀ r f = c

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
⊢ cindex z₀ r f = c
Tactic:
have e7 : (∮ z in C(z₀, r), c / (z - z₀)) = 2 * π * I * c := by
  simpa [div_eq_mul_inv, mul_comm _ _⁻¹] using circle_integral_sub_center_inv_smul hr
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
e7 : (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
⊢ cindex z₀ r f = c

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
e7 : (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
⊢ cindex z₀ r f = c
Tactic:
field_simp [cindex, e4, e5, e6, e7, Real.pi_ne_zero, I_ne_zero, two_ne_zero]
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
e7 : (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
⊢ 2 * ↑π * I * c = c * (2 * ↑π * I)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
e7 : (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
⊢ 2 * ↑π * I * c = c * (2 * ↑π * I)
Tactic:
ring
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
Tactic:
apply circleIntegral.integral_add
State after:
case hf
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ CircleIntegrable (fun z => c / (z - z₀)) z₀ r

case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ CircleIntegrable (fun z => deriv g z / g z) z₀ r

State before:
case hf
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ CircleIntegrable (fun z => c / (z - z₀)) z₀ r
Tactic:
apply ContinuousOn.circleIntegrable hr.le
State after:
case hf
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => c / (z - z₀)) (sphere z₀ r)

State before:
case hf
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => c / (z - z₀)) (sphere z₀ r)
Tactic:
apply ContinuousOn.div continuousOn_const (continuousOn_id.sub continuousOn_const)
State after:
case hf
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ∀ x ∈ sphere z₀ r, id x - z₀ ≠ 0

State before:
case hf
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ∀ x ∈ sphere z₀ r, id x - z₀ ≠ 0
Tactic:
exact λ z hz => sub_ne_zero.mpr (ne_of_mem_sphere hz hr.ne.symm)
State after:
no goals

State before:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ CircleIntegrable (fun z => deriv g z / g z) z₀ r
Tactic:
apply ContinuousOn.circleIntegrable hr.le
State after:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z / g z) (sphere z₀ r)

State before:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z / g z) (sphere z₀ r)
Tactic:
refine ContinuousOn.div ?_ (h1.continuousOn.mono e2) (λ z hz => h2 _ (sphere_subset_closedBall hz))
State after:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) (sphere z₀ r)

State before:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) (sphere z₀ r)
Tactic:
refine ContinuousOn.mono ?_ e2
State after:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) U

State before:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) U
Tactic:
apply ContDiffOn.continuousOn_deriv_of_isOpen ?_ hU le_rfl
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContDiffOn ℂ 1 g U

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContDiffOn ℂ 1 g U
Tactic:
exact h1.contDiffOn hU
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
⊢ (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
Tactic:
have := cindex_eq_zero hU hr h0 h1 h2
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
this : cindex z₀ r g = 0
⊢ (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
this : cindex z₀ r g = 0
⊢ (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
Tactic:
simpa [cindex, Real.pi_ne_zero, I_ne_zero] using this
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
⊢ (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
Tactic:
simpa [div_eq_mul_inv, mul_comm _ _⁻¹] using circle_integral_sub_center_inv_smul hr
State after:
no goals