Theorem: derivWithin.clog (Ray/Misc/Bounds.lean)

State before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
have hz := DifferentiableWithinAt.hasDerivWithinAt hf
State after:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z

State before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
have h := HasDerivWithinAt.clog hz hx
State after:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z

State before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
have u := o.uniqueDiffWithinAt (𝕜 := ℂ) zs
State after:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
u : UniqueDiffWithinAt ℂ s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z

State before:
f : ℂ → ℂ
z : ℂ
s : Set ℂ
o : IsOpen s
zs : z ∈ s
hf : DifferentiableWithinAt ℂ f s z
hx : (f z).re > 0 ∨ (f z).im ≠ 0
hz : HasDerivWithinAt f (derivWithin f s z) s z
h : HasDerivWithinAt (fun t => (f t).log) (derivWithin f s z / f z) s z
u : UniqueDiffWithinAt ℂ s z
⊢ derivWithin (fun z => (f z).log) s z = derivWithin f s z / f z
Tactic:
rw [HasDerivWithinAt.derivWithin h u]
State after:
no goals