[GOAL]
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
cases' hx.lt_or_lt with hx hx
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
have : sqrt =ᶠ[𝓝 x] fun _ => 0 := (gt_mem_nhds hx).mono fun x hx => sqrt_eq_zero_of_nonpos hx.le
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
this : sqrt =ᶠ[𝓝 x] fun x => 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
exact
  ⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
    contDiffAt_const.congr_of_eventuallyEq this⟩
[GOAL]
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
have : ↑2 * sqrt x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
[GOAL]
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ 2 * sqrt x ^ (2 - 1) ≠ 0
[PROOFSTEP]
simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
[GOAL]
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
constructor
[GOAL]
case inr.left
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x
[PROOFSTEP]
simpa using sqLocalHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)
[GOAL]
case inr.right
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
exact fun n => sqLocalHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (sqrt x)) (contDiffAt_id.pow 2)
[GOAL]
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.sqrt (f y)) (f' / (2 * Real.sqrt (f x))) s x
[PROOFSTEP]
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasDerivAt_sqrt hx).comp_hasDerivWithinAt x hf
[GOAL]
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y => Real.sqrt (f y)) (f' / (2 * Real.sqrt (f x))) x
[PROOFSTEP]
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasDerivAt_sqrt hx).comp x hf
[GOAL]
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun t => Real.sqrt (f t)) (f' / (2 * Real.sqrt (f x))) x
[PROOFSTEP]
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasStrictDerivAt_sqrt hx).comp x hf
