p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ valuation ↑p = 1
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation ↑p = 1
have h : (1 : ℝ) < p := by exact_mod_cast (Fact.out : p.Prime).one_lt
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ ↑p ≠ 0

case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ ‖↑p‖ = (fun x x_1 => x ^ x_1) (↑p) (-1)
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ valuation ↑p = 1
refine' neg_injective ((zpow_strictMono h).injective <| (norm_eq_pow_val _).symm.trans _)
no goals
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
exact_mod_cast (Fact.out : p.Prime).one_lt
no goals
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ ↑p ≠ 0
exact_mod_cast (Fact.out : p.Prime).ne_zero
no goals
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ ‖↑p‖ = (fun x x_1 => x ^ x_1) (↑p) (-1)
simp