internlm/Lean-Github huggingface dataset:
Theorem: eventually_deriv_div_self_eq
Proof state before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
have lh3 := eventually_eventually_nhds.mpr hp.eq_pow_order_mul_iterate_dslope
Proof state after:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
lh3 :
  ∀ᶠ (y : ℂ) in 𝓝 z₀,
    ∀ᶠ (x : ℂ) in 𝓝 y,
      f x = (x - z₀) ^ FormalMultilinearSeries.order p • (swap dslope z₀)^[FormalMultilinearSeries.order p] f x
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Theorem: eventually_deriv_div_self_eq
Proof state before:
case intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
r : ENNReal
h2 :
  HasFPowerSeriesOnBall ((swap dslope z₀)^[FormalMultilinearSeries.order p] f)
    (FormalMultilinearSeries.fslope^[FormalMultilinearSeries.order p] p) z₀ r
lh1 : ∀ᶠ (y : ℂ) in 𝓝 z₀, DifferentiableAt ℂ ((swap dslope z₀)^[FormalMultilinearSeries.order p] f) y
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, (swap dslope z₀)^[FormalMultilinearSeries.order p] f z ≠ 0
lh3 :
  ∀ᶠ (y : ℂ) in 𝓝 z₀,
    ∀ᶠ (x : ℂ) in 𝓝 y,
      f x = (x - z₀) ^ FormalMultilinearSeries.order p • (swap dslope z₀)^[FormalMultilinearSeries.order p] f x
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
Tactic:
filter_upwards [lh1, lh2, lh3] with z using deriv_div_self_eq_div_add_deriv_div_self
Proof state after:
no goals
Theorem: cindex_eq_zero
Proof 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)]
Proof state after:
no goals
Theorem: cindex_eq_zero
Proof 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 }
Proof 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
Theorem: cindex_eq_zero
Proof 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 _ _
Proof 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
Theorem: cindex_eq_zero
Proof 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
Proof 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
Theorem: cindex_eq_zero
Proof 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⟩
Proof 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
Theorem: cindex_eq_zero
Proof 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
Proof 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
Theorem: cindex_eq_zero
Proof 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 _, ?_⟩
Proof 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
Theorem: cindex_eq_zero
Proof 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 _ _)
Proof state after:
no goals
Theorem: cindex_eq_zero
Proof 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
Proof state after:
no goals
Theorem: cindex_eq_order_aux
Proof 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
Proof 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
Theorem: cindex_eq_order_aux
Proof 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)
Proof 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
Theorem: cindex_eq_order_aux
Proof 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
Proof 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
Theorem: cindex_eq_order_aux
Proof 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
Proof 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
Theorem: cindex_eq_order_aux
Proof 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]
Proof 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)
Theorem: cindex_eq_order_aux
Proof 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
Proof state after:
no goals
Theorem: cindex_eq_order_aux
Proof 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
Proof 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
Theorem: cindex_eq_order_aux
Proof 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
Proof 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)
Theorem: cindex_eq_order_aux
Proof 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)
Proof 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
Theorem: cindex_eq_order_aux
Proof 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)
Proof state after:
no goals
Theorem: cindex_eq_order_aux
Proof 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
Proof 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)
Theorem: cindex_eq_order_aux
Proof 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))
Proof 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)
Theorem: cindex_eq_order_aux
Proof 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
Proof 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