case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0

case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x
rcases eq_or_lt_of_le h1 with (rfl | h1')
no goals
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0
rw [tan_zero]
no goals
case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x
exact le_of_lt (lt_tan h1' h2)