p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b
rw [Ideal.mem_span_singleton] at ha hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b
rw [← sub_eq_zero, ← Int.cast_sub, ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.coe_nat_pow]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha✝ : ↑p ^ n ∣ x - ↑a
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
rw [← dvd_neg, neg_sub] at ha
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha✝ : ↑p ^ n ∣ x - ↑a
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - x + (x - ↑b)
⊢ ↑p ^ n ∣ a - b
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha✝ : ↑p ^ n ∣ x - ↑a
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
have := dvd_add ha hb
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
n : ℕ
x : ℤ_[p]
a b : ℤ
ha✝ : ↑p ^ n ∣ x - ↑a
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - x + (x - ↑b)
⊢ ↑p ^ n ∣ a - b
rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ←
  Int.cast_sub, pow_p_dvd_int_iff, Nat.cast_pow] at this