case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ x ≤ exp (log x)

case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ exp (log x)
x✝ y x : ℝ
⊢ x ≤ exp (log x)
by_cases h_zero : x = 0
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ x ≤ exp (log x)
rw [h_zero, log, dif_pos rfl, exp_zero]
no goals
case pos
x✝ y x : ℝ
h_zero : x = 0
⊢ 0 ≤ 1
exact zero_le_one
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ abs x
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ exp (log x)
rw [exp_log_eq_abs h_zero]
no goals
case neg
x✝ y x : ℝ
h_zero : ¬x = 0
⊢ x ≤ abs x
exact le_abs_self _