case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤

case inr.inl

⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ⊤

case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
y : ℝ
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
rcases lt_trichotomy (0 : ℝ) y with (H | rfl | H)
no goals
case inl
y : ℝ
H : 0 < y
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
simp [H, ne_of_gt, zero_rpow_of_pos, lt_irrefl]
no goals
case inr.inl

⊢ 0 ^ 0 = if 0 < 0 then 0 else if 0 = 0 then 1 else ⊤
simp [lt_irrefl]
no goals
case inr.inr
y : ℝ
H : y < 0
⊢ 0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
simp [H, asymm H, ne_of_lt, zero_rpow_of_neg]