Theorem: Imo2008P4.positive_pow_eq_pow (Compfiles/Imo2008P4.lean)

State before:
n : ℕ
h : 0 < n
a b : PosReal
⊢ a ^ n = b ^ n ↔ a = b
Tactic:
rw [← Subtype.coe_inj, Positive.val_pow, ← Subtype.coe_inj, Positive.val_pow]
State after:
n : ℕ
h : 0 < n
a b : PosReal
⊢ ↑a ^ n = ↑b ^ n ↔ ↑a = ↑b

State before:
n : ℕ
h : 0 < n
a b : PosReal
⊢ ↑a ^ n = ↑b ^ n ↔ ↑a = ↑b
Tactic:
exact pow_left_inj (le_of_lt a.2) (le_of_lt b.2) (Nat.ne_of_gt h)
State after:
no goals