case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (fun a => ↑a) x = (fun a => ↑a) (↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x))
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ x = ↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
apply Subtype.coe_injective
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ (fun a => ↑a) x = (fun a => ↑a) (↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x))
push_cast
case h.e'_3.h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
repr : ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
⊢ ↑p ^ Int.natAbs (valuation x) = ↑p ^ valuation x
case a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
repr : ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
convert repr using 2
no goals
case h.e'_3.h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
repr : ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
⊢ ↑p ^ Int.natAbs (valuation x) = ↑p ^ valuation x
rw [← zpow_ofNat, Int.natAbs_of_nonneg (valuation_nonneg x)]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-valuation x + valuation x)

case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑↑(unitCoeff hx) * ↑p ^ valuation x
rw [unitCoeff_coe, mul_assoc, ← zpow_add₀]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑x = ↑x * ↑p ^ (-valuation x + valuation x)
simp
no goals
case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
⊢ ↑p ≠ 0
exact_mod_cast hp.1.ne_zero