p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), x - ↑(appr x n) ∈ Ideal.span {↑p ^ n}
simp only [Ideal.mem_span_singleton]
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), ↑p ^ zero ∣ x - ↑(appr x zero)

case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
⊢ ∀ (x : ℤ_[p]), ↑p ^ succ n ∣ x - ↑(appr x (succ n))
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
⊢ ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
induction' n with n ih
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
⊢ ↑p ^ succ n ∣ x - ↑(appr x (succ n))
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
⊢ ∀ (x : ℤ_[p]), ↑p ^ succ n ∣ x - ↑(appr x (succ n))
intro x
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
⊢ ↑p ^ succ n ∣
    x -
      ↑(if hy : x - ↑(appr x n) = 0 then appr x n
        else
          appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
⊢ ↑p ^ succ n ∣ x - ↑(appr x (succ n))
dsimp only [appr]
case succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣ x - ↑(appr x n)

case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
⊢ ↑p ^ succ n ∣
    x -
      ↑(if hy : x - ↑(appr x n) = 0 then appr x n
        else
          appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
split_ifs with h
case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x -
      (↑(appr x n) +
        ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n)))))
case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n + p ^ n * ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
push_cast
case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n) -
      ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x -
      (↑(appr x n) +
        ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n)))))
rw [sub_add_eq_sub_sub]
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n) -
      ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n) -
      ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
obtain ⟨c, hc⟩ := ih x
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ ↑p ^ succ n ∣ x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ ↑p ^ succ n ∣
    x - ↑(appr x n) -
      ↑p ^ n * ↑(ZMod.val (↑toZMod (↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))))
simp only [map_natCast, ZMod.nat_cast_self, RingHom.map_pow, RingHom.map_mul, ZMod.nat_cast_val]
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ ↑p ^ succ n ∣ x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
have hc' : c ≠ 0 := by
  rintro rfl
  simp only [MulZeroClass.mul_zero] at hc
  contradiction
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ ↑p ^ n * c - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ x - ↑(appr x n) - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
conv_rhs =>
  congr
  simp only [hc]
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ ↑p ^ n * c - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (↑p ^ n * c) - ↑n))
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ ↑p ^ n * c - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (x - ↑(appr x n)) - ↑n))
rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * (c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c)))
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ succ n ∣ ↑p ^ n * c - ↑p ^ n * ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation (↑p ^ n * c) - ↑n))
rw [valuation_p_pow_mul _ _ hc', add_sub_cancel', _root_.pow_succ', ← mul_sub]
case succ.inr.intro.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
case succ.inr.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ^ n * ↑p ∣ ↑p ^ n * (c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c)))
apply mul_dvd_mul_left
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))

case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
case succ.inr.intro.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
obtain hc0 | hc0 := c.valuation.natAbs.eq_zero_or_pos
no goals
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), ↑p ^ zero ∣ x - ↑(appr x zero)
simp only [zero_eq, _root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
case succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣ 0
case succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣ x - ↑(appr x n)
rw [h]
no goals
case succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : x - ↑(appr x n) = 0
⊢ ↑p ^ succ n ∣ 0
apply dvd_zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
hc : x - ↑(appr x n) = ↑p ^ n * 0
⊢ False
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
⊢ c ≠ 0
rintro rfl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
hc : x - ↑(appr x n) = 0
⊢ False
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
hc : x - ↑(appr x n) = ↑p ^ n * 0
⊢ False
simp only [MulZeroClass.mul_zero] at hc
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
hc : x - ↑(appr x n) = 0
⊢ False
contradiction
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
⊢ valuation (x - ↑(appr x n)) = valuation (↑p ^ n * c)
rw [hc]
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
simp only [hc0, mul_one, _root_.pow_zero]
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
rw [mul_comm, unitCoeff_spec h] at hc
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ c = ↑(unitCoeff h)
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
suffices c = unitCoeff h by
  rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
  apply toZMod_spec
case succ.inr.intro.h.inl.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : Int.natAbs (valuation ↑c) = 0
⊢ ↑c = ↑(unitCoeff h)
case succ.inr.intro.h.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ c = ↑(unitCoeff h)
obtain ⟨c, rfl⟩ : IsUnit c := by
  rw [Int.natAbs_eq_zero] at hc0
  rw [isUnit_iff, norm_eq_pow_val hc', hc0, neg_zero, zpow_zero]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : Int.natAbs (valuation ↑c) = 0
⊢ Irreducible ↑p
case succ.inr.intro.h.inl.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : Int.natAbs (valuation ↑c) = 0
⊢ ↑c = ↑(unitCoeff h)
rw [DiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]ˣ
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = ↑c * ↑p ^ n
hc' : ↑c ≠ 0
hc0 : Int.natAbs (valuation ↑c) = 0
⊢ Irreducible ↑p
exact irreducible_p
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
this : c = ↑(unitCoeff h)
⊢ c - ↑(↑toZMod c) ∈ maximalIdeal ℤ_[p]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
this : c = ↑(unitCoeff h)
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h))
rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
this : c = ↑(unitCoeff h)
⊢ c - ↑(↑toZMod c) ∈ maximalIdeal ℤ_[p]
apply toZMod_spec
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : valuation c = 0
⊢ IsUnit c
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) = 0
⊢ IsUnit c
rw [Int.natAbs_eq_zero] at hc0
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : ↑(unitCoeff h) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x n))) = c * ↑p ^ n
hc' : c ≠ 0
hc0 : valuation c = 0
⊢ IsUnit c
rw [isUnit_iff, norm_eq_pow_val hc', hc0, neg_zero, zpow_zero]
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0)
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0 ^ Int.natAbs (valuation c))
rw [zero_pow hc0]
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c - ↑(↑toZMod ↑(unitCoeff h) * 0)
simp only [sub_zero, ZMod.cast_zero, MulZeroClass.mul_zero]
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ Int.natAbs (valuation c)
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ c
rw [unitCoeff_spec hc']
no goals
case succ.inr.intro.h.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(appr x n)
x : ℤ_[p]
h : ¬x - ↑(appr x n) = 0
c : ℤ_[p]
hc : x - ↑(appr x n) = ↑p ^ n * c
hc' : c ≠ 0
hc0 : Int.natAbs (valuation c) > 0
⊢ ↑p ∣ ↑(unitCoeff hc') * ↑p ^ Int.natAbs (valuation c)
exact (dvd_pow_self (p : ℤ_[p]) hc0.ne').mul_left _