x : ℝ
hx : x ≠ 0
y z : ℝ≥0∞
hyz : (fun y => y ^ x) y = (fun y => y ^ x) z
⊢ y = z
x : ℝ
hx : x ≠ 0
⊢ Function.Injective fun y => y ^ x
intro y z hyz
x : ℝ
hx : x ≠ 0
y z : ℝ≥0∞
hyz : y ^ x = z ^ x
⊢ y = z
x : ℝ
hx : x ≠ 0
y z : ℝ≥0∞
hyz : (fun y => y ^ x) y = (fun y => y ^ x) z
⊢ y = z
dsimp only at hyz
no goals
x : ℝ
hx : x ≠ 0
y z : ℝ≥0∞
hyz : y ^ x = z ^ x
⊢ y = z
rw [← rpow_one y, ← rpow_one z, ← _root_.mul_inv_cancel hx, rpow_mul, rpow_mul, hyz]