case pos
x✝ y x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

case neg
x✝ y x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x
x✝ y x : ℝ
⊢ log x⁻¹ = -log x
by_cases hx : x = 0
no goals
case neg
x✝ y x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x
rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
no goals
case pos
x✝ y x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x
simp [hx]