x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (exp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
x : ℝ
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
have : HasStrictDerivAt log (exp <| log x)⁻¹ x :=
  (hasStrictDerivAt_exp <| log x).of_local_left_inverse (continuousAt_log hx.ne')
      (ne_of_gt <| exp_pos _) <|
    Eventually.mono (lt_mem_nhds hx) @exp_log
no goals
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (exp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
rwa [exp_log hx] at this