case pos
x✝ y x : ℝ
h : x = 0
⊢ log (abs x) = log x

case neg
x✝ y x : ℝ
h : ¬x = 0
⊢ log (abs x) = log x
x✝ y x : ℝ
⊢ log (abs x) = log x
by_cases h : x = 0
no goals
case pos
x✝ y x : ℝ
h : x = 0
⊢ log (abs x) = log x
simp [h]
no goals
case neg
x✝ y x : ℝ
h : ¬x = 0
⊢ log (abs x) = log x
rw [← exp_eq_exp, exp_log_eq_abs h, exp_log_eq_abs (abs_pos.2 h).ne', abs_abs]