x✝ y✝ z✝ x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z
x✝ y z x : ℝ
hx : x ≠ 0
⊢ InjOn (fun y => y ^ x) {y | 0 ≤ y}
rintro y hy z hz (hyz : y ^ x = z ^ x)
no goals
x✝ y✝ z✝ x : ℝ
hx : x ≠ 0
y : ℝ
hy : y ∈ {y | 0 ≤ y}
z : ℝ
hz : z ∈ {y | 0 ≤ y}
hyz : y ^ x = z ^ x
⊢ y = z
rw [← rpow_one y, ← rpow_one z, ← _root_.mul_inv_cancel hx, rpow_mul hy, rpow_mul hz, hyz]