pow left is injective for reals

Stream: Is there code for X?

[Snir Broshi]

theorem foo (n : ℕ) (hn : n ≠ 0) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ^ n = y ^ n ↔ x = y := by
  sorry

theorem bar (r : ℝ) (hr : 0 < r) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x ^ r = y ^ r ↔ x = y := by
  sorry

Do these exist, or does anyone have counterexamples?
I found a similar theorem for HPow.hPow ℕ ℕ ℕ: docs#Nat.pow_left_injective

[Damiano Testa]

Maybe docs#Real.rpow_left_inj ?

[Damiano Testa]

simp_all proves the first.

[Damiano Testa]

In fact, pow_left_inj₀ hx hy hn proves the first and Real.rpow_left_inj hx hy hr.ne' proves the second.