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

State before:
z z₀ : ℂ
U : Set ℂ
h : has_logs U
⊢ _root_.has_sqrt U
Tactic:
rintro f hfz hf
State after:
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U

State before:
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
Tactic:
obtain ⟨l, hl, hlf⟩ := h f hf hfz
State after:
case intro.intro
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U

State before:
case intro.intro
z z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
⊢ ∃ g, DifferentiableOn ℂ g U ∧ EqOn f (g ^ 2) U
Tactic:
refine ⟨λ z => exp (l z / 2), differentiable_exp.comp_differentiableOn (hl.div_const _), λ z hz => ?_⟩
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
z : ℂ
hz : z ∈ U
⊢ f z = ((fun z => cexp (l z / 2)) ^ 2) z

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
h : has_logs U
f : ℂ → ℂ
hfz : ∀ z ∈ U, f z ≠ 0
hf : DifferentiableOn ℂ f U
l : ℂ → ℂ
hl : DifferentiableOn ℂ l U
hlf : EqOn f (cexp ∘ l) U
z : ℂ
hz : z ∈ U
⊢ f z = ((fun z => cexp (l z / 2)) ^ 2) z
Tactic:
simpa [pow_two, ← exp_add] using hlf hz
State after:
no goals