case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x

case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt log x⁻¹ x
cases' hx.lt_or_lt with hx hx
case h.e'_6
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg

case h.e'_7
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt log x⁻¹ x
convert (hasStrictDerivAt_log_of_pos (neg_pos.mpr hx)).comp x (hasStrictDerivAt_neg x) using 1
case h.e'_6.h
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y
case h.e'_6
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ log = log ∘ Neg.neg
ext y
no goals
case h.e'_6.h
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
y : ℝ
⊢ log y = (log ∘ Neg.neg) y
exact (log_neg_eq_log y).symm
no goals
case h.e'_7
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ x⁻¹ = (-x)⁻¹ * -1
field_simp [hx.ne]
no goals
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt log x⁻¹ x
exact hasStrictDerivAt_log_of_pos hx