case inl
y z : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

case inr
x y z : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
x y z : ℝ
hx : 0 ≤ x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
rcases hx.eq_or_lt with (rfl | hx)
no goals
case inl
y z : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y
rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, lt_irrefl, zero_lt_one]
no goals
case inr
x y z : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm]