Theorem: deriv_div_self_eq_div_add_deriv_div_self (RMT4/cindex.lean)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
have h1 : DifferentiableAt ℂ (λ y => (y - z₀) ^ n) z :=
  ((differentiable_id'.sub_const z₀).pow n).differentiableAt
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
have h4 : DifferentiableAt ℂ (λ y => y - z₀) z := (differentiable_id'.sub_const z₀).differentiableAt
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
have h5 : deriv (fun y => y - z₀) z = 1 := by simp only [deriv_sub_const, deriv_id'']
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z
Tactic:
simp [hfg.deriv_eq, hfg.self_of_nhds, deriv_mul h1 hg, _root_.add_div, deriv_pow'' n h4, deriv_sub_const, h5]
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ ↑n * (z - z₀) ^ (n - 1) * g z / ((z - z₀) ^ n * g z) + (z - z₀) ^ n * deriv g z / ((z - z₀) ^ n * g z) =
    ↑n / (z - z₀) + deriv g z / g z

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
⊢ ↑n * (z - z₀) ^ (n - 1) * g z / ((z - z₀) ^ n * g z) + (z - z₀) ^ n * deriv g z / ((z - z₀) ^ n * g z) =
    ↑n / (z - z₀) + deriv g z / g z
Tactic:
cases n
State after:
case zero
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z

case succ
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n✝ : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n✝ * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n✝) z
⊢ ↑(succ n✝) * (z - z₀) ^ (succ n✝ - 1) * g z / ((z - z₀) ^ succ n✝ * g z) +
      (z - z₀) ^ succ n✝ * deriv g z / ((z - z₀) ^ succ n✝ * g z) =
    ↑(succ n✝) / (z - z₀) + deriv g z / g z

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z
Tactic:
case zero => simp
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ↑(succ n) * (z - z₀) ^ (succ n - 1) * g z / ((z - z₀) ^ succ n * g z) +
      (z - z₀) ^ succ n * deriv g z / ((z - z₀) ^ succ n * g z) =
    ↑(succ n) / (z - z₀) + deriv g z / g z
Tactic:
case succ n =>
  field_simp [_root_.pow_succ, sub_ne_zero.mpr hz]
  ring
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ n * g w
hz : z ≠ z₀
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ n) z
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
⊢ deriv (fun y => y - z₀) z = 1
Tactic:
simp only [deriv_sub_const, deriv_id'']
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ zero * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ zero) z
⊢ ↑zero * (z - z₀) ^ (zero - 1) * g z / ((z - z₀) ^ zero * g z) +
      (z - z₀) ^ zero * deriv g z / ((z - z₀) ^ zero * g z) =
    ↑zero / (z - z₀) + deriv g z / g z
Tactic:
simp
State after:
no goals

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ↑(succ n) * (z - z₀) ^ (succ n - 1) * g z / ((z - z₀) ^ succ n * g z) +
      (z - z₀) ^ succ n * deriv g z / ((z - z₀) ^ succ n * g z) =
    ↑(succ n) / (z - z₀) + deriv g z / g z
Tactic:
field_simp [_root_.pow_succ, sub_ne_zero.mpr hz]
State after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ((↑n + 1) * (z - z₀) ^ n * g z + (z - z₀) * (z - z₀) ^ n * deriv g z) * ((z - z₀) * g z) =
    ((↑n + 1) * g z + deriv g z * (z - z₀)) * ((z - z₀) * (z - z₀) ^ n * g z)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
U : Set ℂ
r : ℝ
hg : DifferentiableAt ℂ g z
hgz : g z ≠ 0
hz : z ≠ z₀
h4 : DifferentiableAt ℂ (fun y => y - z₀) z
h5 : deriv (fun y => y - z₀) z = 1
n : ℕ
hfg : f =ᶠ[𝓝 z] fun w => (w - z₀) ^ succ n * g w
h1 : DifferentiableAt ℂ (fun y => (y - z₀) ^ succ n) z
⊢ ((↑n + 1) * (z - z₀) ^ n * g z + (z - z₀) * (z - z₀) ^ n * deriv g z) * ((z - z₀) * g z) =
    ((↑n + 1) * g z + deriv g z * (z - z₀)) * ((z - z₀) * (z - z₀) ^ n * g z)
Tactic:
ring
State after:
no goals