internlm/Lean-Github huggingface dataset:
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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)
Proof 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
Theorem: has_primitives.has_logs
Proof 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₀)
Proof 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
Theorem: has_primitives.has_logs
Proof 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)
Proof 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
Theorem: has_primitives.has_logs
Proof 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 _)
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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 _)
Proof 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
Theorem: has_primitives.has_logs
Proof 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, ?_⟩
Proof 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
Theorem: has_primitives.has_logs
Proof 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)
Proof 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
Theorem: has_primitives.has_logs
Proof 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₀]
Proof 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
Theorem: has_primitives.has_logs
Proof 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]
Proof 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
Theorem: has_primitives.has_logs
Proof 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₀
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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 _)]
Proof 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
Theorem: has_primitives.has_logs
Proof 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)]
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof 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
Theorem: has_primitives.has_logs
Proof 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]
Proof 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
Theorem: has_primitives.has_logs
Proof 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
Proof state after:
no goals
Theorem: has_primitives.has_logs
Proof 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)
Proof state after:
no goals
Theorem: has_primitives.has_logs
Proof 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
Proof 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₀
Theorem: has_primitives.has_logs
Proof 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₀]
Proof state after:
no goals