p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x ↔ ↑n ≤ valuation x
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ x ∈ Ideal.span {↑p ^ n} ↔ ↑n ≤ valuation x
rw [Ideal.mem_span_singleton]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x → ↑n ≤ valuation x

case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ valuation x → ↑p ^ n ∣ x
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x ↔ ↑n ≤ valuation x
constructor
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ ↑n ≤ valuation (↑p ^ n * c)
case mp
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑p ^ n ∣ x → ↑n ≤ valuation x
rintro ⟨c, rfl⟩
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ c ≠ 0
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ ↑n ≤ valuation (↑p ^ n * c)
suffices c ≠ 0 by
  rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right]
  apply valuation_nonneg
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
⊢ c ≠ 0
contrapose! hx
no goals
case mp.intro
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : c = 0
⊢ ↑p ^ n * c = 0
rw [hx, MulZeroClass.mul_zero]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ 0 ≤ valuation c
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ ↑n ≤ valuation (↑p ^ n * c)
rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ 0 ≤ valuation c
apply valuation_nonneg
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ valuation x → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ valuation x → ↑p ^ n ∣ x
nth_rewrite 2 [unitCoeff_spec hx]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ↑n ≤ ↑k → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ Int.natAbs ↑k
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ↑n ≤ valuation x → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ Int.natAbs (valuation x)
lift x.valuation to ℕ using x.valuation_nonneg with k
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ n ≤ k → ↑p ^ n ∣ ↑p ^ k
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ ↑n ≤ ↑k → ↑p ^ n ∣ ↑(unitCoeff hx) * ↑p ^ Int.natAbs ↑k
simp only [Int.natAbs_ofNat, Units.isUnit, IsUnit.dvd_mul_left, Int.ofNat_le]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
H : n ≤ k
⊢ ↑p ^ n ∣ ↑p ^ k
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
⊢ n ≤ k → ↑p ^ n ∣ ↑p ^ k
intro H
case mpr.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
H : n ≤ n + k
⊢ ↑p ^ n ∣ ↑p ^ (n + k)
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
H : n ≤ k
⊢ ↑p ^ n ∣ ↑p ^ k
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le H
no goals
case mpr.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n k : ℕ
H : n ≤ n + k
⊢ ↑p ^ n ∣ ↑p ^ (n + k)
simp only [pow_add, dvd_mul_right]