p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
⊢ valuation (↑p ^ n * c) = ↑n + valuation c
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
⊢ valuation (↑p ^ n * c) = ↑n + valuation c
have : ‖(p : ℤ_[p]) ^ n * c‖ = ‖(p : ℤ_[p]) ^ n‖ * ‖c‖ := norm_mul _ _
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-(↑n + valuation c))
aux : ↑p ^ n * c ≠ 0
⊢ 0 < ↑p

case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-(↑n + valuation c))
aux : ↑p ^ n * c ≠ 0
⊢ ↑p ≠ 1

case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-↑n) * ↑p ^ (-valuation c)
aux : ↑p ^ n * c ≠ 0
⊢ ↑p ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
aux : ↑p ^ n * c ≠ 0
⊢ valuation (↑p ^ n * c) = ↑n + valuation c
rwa [norm_eq_pow_val aux, norm_p_pow, norm_eq_pow_val hc, ← zpow_add₀, ← neg_add,
  zpow_inj, neg_inj] at this
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n * c = 0
⊢ c = 0
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
⊢ ↑p ^ n * c ≠ 0
contrapose! hc
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0 ∨ c = 0
⊢ c = 0
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n * c = 0
⊢ c = 0
rw [mul_eq_zero] at hc
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0
⊢ c = 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : c = 0
⊢ c = 0
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0 ∨ c = 0
⊢ c = 0
cases' hc with hc hc
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0
⊢ p = 0
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0
⊢ c = 0
refine (hp.1.ne_zero ?_).elim
no goals
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : ↑p ^ n = 0
⊢ p = 0
exact_mod_cast pow_eq_zero hc
no goals
case inr
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖
hc : c = 0
⊢ c = 0
exact hc
no goals
case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-(↑n + valuation c))
aux : ↑p ^ n * c ≠ 0
⊢ 0 < ↑p
exact_mod_cast hp.1.pos
no goals
case h₁
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-(↑n + valuation c))
aux : ↑p ^ n * c ≠ 0
⊢ ↑p ≠ 1
exact_mod_cast hp.1.ne_one
no goals
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hc : c ≠ 0
this : ↑p ^ (-valuation (↑p ^ n * c)) = ↑p ^ (-↑n) * ↑p ^ (-valuation c)
aux : ↑p ^ n * c ≠ 0
⊢ ↑p ≠ 0
exact_mod_cast hp.1.ne_zero