Theorem: has_primitives.has_logs (RMT4/has_sqrt.lean)

State before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
⊢ _root_.has_logs U
Tactic:
by_cases h : U = ∅
State after:
case pos
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U

case neg
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U

State before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U
Tactic:
case pos => exact λ f => by simp [h, DifferentiableOn]
State after:
no goals

State before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U
Tactic:
case neg =>
  obtain ⟨z₀, hz₀⟩ := nonempty_iff_ne_empty.2 h
  rintro f hf hfz
  obtain ⟨lf, hlf1, hlf2⟩ := hp (deriv f / f) ((hf.deriv hU).div hf hfz)
  let g : ℂ → ℂ := λ z => lf z + (log (f z₀) - lf z₀)
  set h : ℂ → ℂ := f / (exp ∘ g)
  have h3 : DifferentiableOn ℂ g U := hlf1.add (differentiableOn_const _)
  have e4 : DifferentiableOn ℂ (exp ∘ g) U := differentiable_exp.comp_differentiableOn h3
  have e1 : DifferentiableOn ℂ h U := hf.div e4 (λ z _ => exp_ne_zero _)
  refine ⟨g, h3, ?_⟩
  suffices h : EqOn h (λ _ => 1) U
    by exact λ z hz => eq_of_div_eq_one (h hz)
  have : 1 = h z₀ := by unfold_let ; simp [exp_log, hfz z₀ hz₀]
  rw [this]
  refine EqOn_of_deriv_eq_zero hU hU' e1 (λ z hz => ?_) hz₀
  have f0 : U ∈ 𝓝 z := hU.mem_nhds hz
  dsimp
  unfold_let
  rw [Pi.div_def, deriv_div (hf.differentiableAt f0) (e4.differentiableAt f0) (exp_ne_zero _)]
  rw [deriv.scomp z differentiableAt_exp (h3.differentiableAt f0)]
  have e5 : deriv g z = deriv lf z := by unfold_let ; simp
  field_simp [exp_ne_zero, hlf2 hz, hfz z hz, e5]
  ring
State after:
no goals

State before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
⊢ _root_.has_logs U
Tactic:
exact λ f => by simp [h, DifferentiableOn]
State after:
no goals

State before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : U = ∅
f : ℂ → ℂ
⊢ DifferentiableOn ℂ f U → (∀ z ∈ U, f z ≠ 0) → ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
simp [h, DifferentiableOn]
State after:
no goals

State before:
z z₀ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
⊢ _root_.has_logs U
Tactic:
obtain ⟨z₀, hz₀⟩ := nonempty_iff_ne_empty.2 h
State after:
case intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ _root_.has_logs U

State before:
case intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ _root_.has_logs U
Tactic:
rintro f hf hfz
State after:
case intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
obtain ⟨lf, hlf1, hlf2⟩ := hp (deriv f / f) ((hf.deriv hU).div hf hfz)
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
let g : ℂ → ℂ := λ z => lf z + (log (f z₀) - lf z₀)
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
set h : ℂ → ℂ := f / (exp ∘ g)
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
have h3 : DifferentiableOn ℂ g U := hlf1.add (differentiableOn_const _)
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
have e4 : DifferentiableOn ℂ (exp ∘ g) U := differentiable_exp.comp_differentiableOn h3
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
have e1 : DifferentiableOn ℂ h U := hf.div e4 (λ z _ => exp_ne_zero _)
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (cexp ∘ g) U
Tactic:
refine ⟨g, h3, ?_⟩
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ EqOn f (cexp ∘ g) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ EqOn f (cexp ∘ g) U
Tactic:
suffices h : EqOn h (λ _ => 1) U
  by exact λ z hz => eq_of_div_eq_one (h hz)
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ EqOn h (fun x => 1) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ EqOn h (fun x => 1) U
Tactic:
have : 1 = h z₀ := by unfold_let ; simp [exp_log, hfz z₀ hz₀]
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
⊢ EqOn h (fun x => 1) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
⊢ EqOn h (fun x => 1) U
Tactic:
rw [this]
State after:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
⊢ EqOn h (fun x => h z₀) U

State before:
case intro.intro.intro
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
⊢ EqOn h (fun x => h z₀) U
Tactic:
refine EqOn_of_deriv_eq_zero hU hU' e1 (λ z hz => ?_) hz₀
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
⊢ deriv h z = 0 z

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
⊢ deriv h z = 0 z
Tactic:
have f0 : U ∈ 𝓝 z := hU.mem_nhds hz
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv h z = 0 z

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv h z = 0 z
Tactic:
dsimp
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv h z = 0

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv h z = 0
Tactic:
unfold_let
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv (f / cexp ∘ fun z => lf z + (log (f z₀) - lf z₀)) z = 0

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv (f / cexp ∘ fun z => lf z + (log (f z₀) - lf z₀)) z = 0
Tactic:
rw [Pi.div_def, deriv_div (hf.differentiableAt f0) (e4.differentiableAt f0) (exp_ne_zero _)]
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ (deriv f z * (cexp ∘ g) z - f z * deriv (cexp ∘ g) z) / (cexp ∘ g) z ^ 2 = 0

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ (deriv f z * (cexp ∘ g) z - f z * deriv (cexp ∘ g) z) / (cexp ∘ g) z ^ 2 = 0
Tactic:
rw [deriv.scomp z differentiableAt_exp (h3.differentiableAt f0)]
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ (deriv f z * (cexp ∘ g) z - f z * deriv g z • deriv cexp (g z)) / (cexp ∘ g) z ^ 2 = 0

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ (deriv f z * (cexp ∘ g) z - f z * deriv g z • deriv cexp (g z)) / (cexp ∘ g) z ^ 2 = 0
Tactic:
have e5 : deriv g z = deriv lf z := by unfold_let ; simp
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
e5 : deriv g z = deriv lf z
⊢ (deriv f z * (cexp ∘ g) z - f z * deriv g z • deriv cexp (g z)) / (cexp ∘ g) z ^ 2 = 0

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
e5 : deriv g z = deriv lf z
⊢ (deriv f z * (cexp ∘ g) z - f z * deriv g z • deriv cexp (g z)) / (cexp ∘ g) z ^ 2 = 0
Tactic:
field_simp [exp_ne_zero, hlf2 hz, hfz z hz, e5]
State after:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
e5 : deriv g z = deriv lf z
⊢ deriv f z * cexp (g z) * f z - f z * (deriv f z * cexp (g z)) = 0

State before:
case intro.intro.intro
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
e5 : deriv g z = deriv lf z
⊢ deriv f z * cexp (g z) * f z - f z * (deriv f z * cexp (g z)) = 0
Tactic:
ring
State after:
no goals

State before:
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝¹ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h✝ : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h✝ U
h : EqOn h✝ (fun x => 1) U
⊢ EqOn f (cexp ∘ g) U
Tactic:
exact λ z hz => eq_of_div_eq_one (h hz)
State after:
no goals

State before:
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ 1 = h z₀
Tactic:
unfold_let
State after:
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ 1 = (f / cexp ∘ fun z => lf z + (log (f z₀) - lf z₀)) z₀

State before:
z z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
⊢ 1 = (f / cexp ∘ fun z => lf z + (log (f z₀) - lf z₀)) z₀
Tactic:
simp [exp_log, hfz z₀ hz₀]
State after:
no goals

State before:
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv g z = deriv lf z
Tactic:
unfold_let
State after:
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv (fun z => lf z + (log (f z₀) - lf z₀)) z = deriv lf z

State before:
z✝ z₀✝ : ℂ
U : Set ℂ
hp : has_primitives U
hU : IsOpen U
hU' : IsPreconnected U
h✝ : ¬U = ∅
z₀ : ℂ
hz₀ : z₀ ∈ U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hfz : ∀ z ∈ U, f z ≠ 0
lf : ℂ → ℂ
hlf1 : DifferentiableOn ℂ lf U
hlf2 : EqOn (deriv lf) (deriv f / f) U
g : ℂ → ℂ := fun z => lf z + (log (f z₀) - lf z₀)
h : ℂ → ℂ := f / cexp ∘ g
h3 : DifferentiableOn ℂ g U
e4 : DifferentiableOn ℂ (cexp ∘ g) U
e1 : DifferentiableOn ℂ h U
this : 1 = h z₀
z : ℂ
hz : z ∈ U
f0 : U ∈ 𝓝 z
⊢ deriv (fun z => lf z + (log (f z₀) - lf z₀)) z = deriv lf z
Tactic:
simp
State after:
no goals