Theorem: cindex_eq_zero (RMT4/cindex.lean)

State before:
case intro.intro.intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
V : Set ℂ
h1 : V ⊆ U
h2 : IsOpen V
h3 : closedBall c r ⊆ V
h4 : ∀ z ∈ V, f z ≠ 0
⊢ cindex c r f = 0
Tactic:
simp [cindex, circle_integral_eq_zero h2 hr h3 (((f_hol.mono h1).deriv h2).div (f_hol.mono h1) h4)]
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
Tactic:
set s : Set ℂ := { z ∈ U | f z ≠ 0 }
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
Tactic:
have e1 : IsCompact (closedBall c r) := isCompact_closedBall _ _
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
Tactic:
have e2 : IsOpen s := f_hol.continuousOn.isOpen_inter_preimage hU isOpen_compl_singleton
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
Tactic:
have e3 : closedBall c r ⊆ s := λ z hz => ⟨hcr hz, hf z hz⟩
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
Tactic:
obtain ⟨δ, e4, e5⟩ := e1.exists_thickening_subset_open e2 e3
State after:
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0

State before:
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ ∃ V ⊆ U, IsOpen V ∧ closedBall c r ⊆ V ∧ ∀ z ∈ V, f z ≠ 0
Tactic:
refine ⟨thickening δ (closedBall c r), ?_, isOpen_thickening, self_subset_thickening e4 _, ?_⟩
State after:
case intro.intro.refine_1
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ thickening δ (closedBall c r) ⊆ U

case intro.intro.refine_2
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ ∀ z ∈ thickening δ (closedBall c r), f z ≠ 0

State before:
case intro.intro.refine_1
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ thickening δ (closedBall c r) ⊆ U
Tactic:
exact (e5.trans $ Set.sep_subset _ _)
State after:
no goals

State before:
case intro.intro.refine_2
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
hcr : closedBall c r ⊆ U
f_hol : DifferentiableOn ℂ f U
hf : ∀ z ∈ closedBall c r, f z ≠ 0
s : Set ℂ := {z | z ∈ U ∧ f z ≠ 0}
e1 : IsCompact (closedBall c r)
e2 : IsOpen s
e3 : closedBall c r ⊆ s
δ : ℝ
e4 : 0 < δ
e5 : thickening δ (closedBall c r) ⊆ s
⊢ ∀ z ∈ thickening δ (closedBall c r), f z ≠ 0
Tactic:
exact λ z hz => (e5 hz).2
State after:
no goals