Theorem: crucial (RMT4/deriv_inj.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
⊢ cindex c r f = 1
Tactic:
have hr : 0 < r := dist_nonneg.trans_lt hz₀
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
⊢ cindex c r f = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
⊢ cindex c r f = 1
Tactic:
set g := dslope f z₀
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
⊢ cindex c r f = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
⊢ cindex c r f = 1
Tactic:
have h1 : DifferentiableOn ℂ g U :=
  (differentiableOn_dslope (hU.mem_nhds (hcr (ball_subset_closedBall hz₀)))).2 hf
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
⊢ cindex c r f = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
⊢ cindex c r f = 1
Tactic:
have h2 : ∀ z ∈ closedBall c r, g z ≠ 0 := by
  rintro z hz
  by_cases h : z = z₀
  case pos => simp [g, dslope, h, Function.update, hf'z₀]
  case neg => simp [g, dslope, h, Function.update, slope, sub_ne_zero.2 h, hfz₀, hfz z hz h]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
⊢ cindex c r f = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
⊢ cindex c r f = 1
Tactic:
have h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0 :=
  λ z hz => sub_ne_zero.2 (sphere_disjoint_ball.ne_of_mem hz hz₀)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
⊢ cindex c r f = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
⊢ cindex c r f = 1
Tactic:
suffices this : cindex c r f = ((2 * Real.pi * I)⁻¹ * ∮ z in C(c, r), (z - z₀)⁻¹) + cindex c r g
  by rw [this, integral_sub_inv_of_mem_ball hz₀, cindex_eq_zero hU hr hcr h1 h2]
     field_simp [two_ne_zero, Real.pi_ne_zero, I_ne_zero]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
⊢ cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
⊢ cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g
Tactic:
have h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z := by
  rintro z hz
  have h3 : ∀ z ∈ U, f z = (z - z₀) * g z :=
    λ z _ => by simpa only [smul_eq_mul, hfz₀, sub_zero] using (sub_smul_dslope f z₀ z).symm
  have hz' : z ∈ U := hcr (sphere_subset_closedBall hz)
  have e0 : U ∈ 𝓝 z := hU.mem_nhds hz'
  have h4 : deriv f z = deriv (λ w => (w - z₀) * g w) z :=
    EventuallyEq.deriv_eq (eventually_of_mem e0 h3)
  have e1 : DifferentiableAt ℂ (λ y => y - z₀) z := differentiableAt_id.sub_const z₀
  have e2 : DifferentiableAt ℂ g z := h1.differentiableAt e0
  have h5 : deriv f z = g z + (z - z₀) * deriv g z := by
    have : deriv (fun y => y - z₀) z = 1 := by
      change deriv (fun y => id y - z₀) z = 1
      simp [deriv_sub_const]
    simp [h4, deriv_mul e1 e2, this]
  have e3 : g z ≠ 0 := h2 z (sphere_subset_closedBall hz)
  field_simp [h3 z hz', h5, mul_comm, h10 z hz]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g
Tactic:
simp only [cindex, integral_congr hr.le h6, ← mul_add]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹ + deriv g z / g z) =
    (2 * ↑Real.pi * I)⁻¹ * ((∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + ∮ (z : ℂ) in C(c, r), deriv g z / g z)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹ + deriv g z / g z) =
    (2 * ↑Real.pi * I)⁻¹ * ((∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + ∮ (z : ℂ) in C(c, r), deriv g z / g z)
Tactic:
congr
State after:
case e_a
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ (∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹ + deriv g z / g z) =
    (∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + ∮ (z : ℂ) in C(c, r), deriv g z / g z

State before:
case e_a
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ (∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹ + deriv g z / g z) =
    (∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + ∮ (z : ℂ) in C(c, r), deriv g z / g z
Tactic:
apply circleIntegral.integral_add
State after:
case e_a.hf
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ CircleIntegrable (fun z => (z - z₀)⁻¹) c r

case e_a.hg
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ CircleIntegrable (fun z => deriv g z / g z) c r

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
⊢ ∀ z ∈ closedBall c r, g z ≠ 0
Tactic:
rintro z hz
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
⊢ g z ≠ 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
⊢ g z ≠ 0
Tactic:
by_cases h : z = z₀
State after:
case pos
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
h : z = z₀
⊢ g z ≠ 0

case neg
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
h : ¬z = z₀
⊢ g z ≠ 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
h : z = z₀
⊢ g z ≠ 0
Tactic:
case pos => simp [g, dslope, h, Function.update, hf'z₀]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
h : ¬z = z₀
⊢ g z ≠ 0
Tactic:
case neg => simp [g, dslope, h, Function.update, slope, sub_ne_zero.2 h, hfz₀, hfz z hz h]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
h : z = z₀
⊢ g z ≠ 0
Tactic:
simp [g, dslope, h, Function.update, hf'z₀]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
z : ℂ
hz : z ∈ closedBall c r
h : ¬z = z₀
⊢ g z ≠ 0
Tactic:
simp [g, dslope, h, Function.update, slope, sub_ne_zero.2 h, hfz₀, hfz z hz h]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
this : cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g
⊢ cindex c r f = 1
Tactic:
rw [this, integral_sub_inv_of_mem_ball hz₀, cindex_eq_zero hU hr hcr h1 h2]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
this : cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g
⊢ (2 * ↑Real.pi * I)⁻¹ * (2 * ↑Real.pi * I) + 0 = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
this : cindex c r f = ((2 * ↑Real.pi * I)⁻¹ * ∮ (z : ℂ) in C(c, r), (z - z₀)⁻¹) + cindex c r g
⊢ (2 * ↑Real.pi * I)⁻¹ * (2 * ↑Real.pi * I) + 0 = 1
Tactic:
field_simp [two_ne_zero, Real.pi_ne_zero, I_ne_zero]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
⊢ ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
rintro z hz
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have h3 : ∀ z ∈ U, f z = (z - z₀) * g z :=
  λ z _ => by simpa only [smul_eq_mul, hfz₀, sub_zero] using (sub_smul_dslope f z₀ z).symm
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have hz' : z ∈ U := hcr (sphere_subset_closedBall hz)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have e0 : U ∈ 𝓝 z := hU.mem_nhds hz'
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have h4 : deriv f z = deriv (λ w => (w - z₀) * g w) z :=
  EventuallyEq.deriv_eq (eventually_of_mem e0 h3)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have e1 : DifferentiableAt ℂ (λ y => y - z₀) z := differentiableAt_id.sub_const z₀
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have e2 : DifferentiableAt ℂ g z := h1.differentiableAt e0
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have h5 : deriv f z = g z + (z - z₀) * deriv g z := by
  have : deriv (fun y => y - z₀) z = 1 := by
    change deriv (fun y => id y - z₀) z = 1
    simp [deriv_sub_const]
  simp [h4, deriv_mul e1 e2, this]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
h5 : deriv f z = g z + (z - z₀) * deriv g z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
h5 : deriv f z = g z + (z - z₀) * deriv g z
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
have e3 : g z ≠ 0 := h2 z (sphere_subset_closedBall hz)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
h5 : deriv f z = g z + (z - z₀) * deriv g z
e3 : g z ≠ 0
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
h5 : deriv f z = g z + (z - z₀) * deriv g z
e3 : g z ≠ 0
⊢ deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
Tactic:
field_simp [h3 z hz', h5, mul_comm, h10 z hz]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z✝ : ℂ
hz : z✝ ∈ sphere c r
z : ℂ
x✝ : z ∈ U
⊢ f z = (z - z₀) * g z
Tactic:
simpa only [smul_eq_mul, hfz₀, sub_zero] using (sub_smul_dslope f z₀ z).symm
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv f z = g z + (z - z₀) * deriv g z
Tactic:
have : deriv (fun y => y - z₀) z = 1 := by
  change deriv (fun y => id y - z₀) z = 1
  simp [deriv_sub_const]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
this : deriv (fun y => y - z₀) z = 1
⊢ deriv f z = g z + (z - z₀) * deriv g z

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
this : deriv (fun y => y - z₀) z = 1
⊢ deriv f z = g z + (z - z₀) * deriv g z
Tactic:
simp [h4, deriv_mul e1 e2, this]
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv (fun y => y - z₀) z = 1
Tactic:
change deriv (fun y => id y - z₀) z = 1
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv (fun y => id y - z₀) z = 1

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
z : ℂ
hz : z ∈ sphere c r
h3 : ∀ z ∈ U, f z = (z - z₀) * g z
hz' : z ∈ U
e0 : U ∈ 𝓝 z
h4 : deriv f z = deriv (fun w => (w - z₀) * g w) z
e1 : DifferentiableAt ℂ (fun y => y - z₀) z
e2 : DifferentiableAt ℂ g z
⊢ deriv (fun y => id y - z₀) z = 1
Tactic:
simp [deriv_sub_const]
State after:
no goals

State before:
case e_a.hf
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ CircleIntegrable (fun z => (z - z₀)⁻¹) c r
Tactic:
rw [circleIntegrable_sub_inv_iff, abs_eq_self.2 hr.le]
State after:
case e_a.hf
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ r = 0 ∨ z₀ ∉ sphere c r

State before:
case e_a.hf
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ r = 0 ∨ z₀ ∉ sphere c r
Tactic:
exact Or.inr (disjoint_right.1 sphere_disjoint_ball hz₀)
State after:
no goals

State before:
case e_a.hg
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ CircleIntegrable (fun z => deriv g z / g z) c r
Tactic:
refine (ContinuousOn.div ?_ ?_ ?_).circleIntegrable hr.le
State after:
case e_a.hg.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) (sphere c r)

case e_a.hg.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ContinuousOn (fun z => g z) (sphere c r)

case e_a.hg.refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ∀ x ∈ sphere c r, g x ≠ 0

State before:
case e_a.hg.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) (sphere c r)
Tactic:
exact (h1.deriv hU).continuousOn.mono (sphere_subset_closedBall.trans hcr)
State after:
no goals

State before:
case e_a.hg.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ContinuousOn (fun z => g z) (sphere c r)
Tactic:
exact h1.continuousOn.mono (sphere_subset_closedBall.trans hcr)
State after:
no goals

State before:
case e_a.hg.refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g✝ : ℂ → ℂ
hU : IsOpen U
hcr : closedBall c r ⊆ U
hz₀ : z₀ ∈ ball c r
hf : DifferentiableOn ℂ f U
hfz₀ : f z₀ = 0
hf'z₀ : deriv f z₀ ≠ 0
hfz : ∀ z ∈ closedBall c r, z ≠ z₀ → f z ≠ 0
hr : 0 < r
g : ℂ → ℂ := dslope f z₀
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall c r, g z ≠ 0
h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0
h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z
⊢ ∀ x ∈ sphere c r, g x ≠ 0
Tactic:
exact λ z hz => h2 z (sphere_subset_closedBall hz)
State after:
no goals