case inl
y : ℝ
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1

case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
x y : ℝ
hx : 0 ≤ x
⊢ log x ≤ 0 ↔ x ≤ 1
rcases hx.eq_or_lt with (rfl | hx)
no goals
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ log x ≤ 0 ↔ x ≤ 1
exact log_nonpos_iff hx
no goals
case inl
y : ℝ
hx : 0 ≤ 0
⊢ log 0 ≤ 0 ↔ 0 ≤ 1
simp [le_refl, zero_le_one]