case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
cases' hx.lt_or_lt with hx hx
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
rw [sqrt_eq_zero_of_nonpos hx.le, MulZeroClass.mul_zero, div_zero]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
this : sqrt =ᶠ[𝓝 x] fun x => 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
have : sqrt =ᶠ[𝓝 x] fun _ => 0 := (gt_mem_nhds hx).mono fun x hx => sqrt_eq_zero_of_nonpos hx.le
no goals
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
this : sqrt =ᶠ[𝓝 x] fun x => 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
exact
  ⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
    contDiffAt_const.congr_of_eventuallyEq this⟩
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
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
have : ↑2 * sqrt x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
case inr.left
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x

case inr.right
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
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
constructor
no goals
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ 2 * sqrt x ^ (2 - 1) ≠ 0
simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
no goals
case inr.left
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x
simpa using sqLocalHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)
no goals
case inr.right
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
exact fun n => sqLocalHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (sqrt x))
  (contDiffAt_id.pow 2)