case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
h : m ≤ m + k
⊢ p ^ m ∣ appr x (m + k) - appr x m
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ p ^ m ∣ appr x n - appr x m
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
⊢ p ^ m ∣ appr x (m + k) - appr x m
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
h : m ≤ m + k
⊢ p ^ m ∣ appr x (m + k) - appr x m
clear h
case intro.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m : ℕ
⊢ p ^ m ∣ appr x (m + zero) - appr x m

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

case intro.succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    appr x (m + k + 0) +
        p ^ (m + k + 0) *
          ZMod.val
            (↑toZMod
              (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
                ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k + 0))) - ↑(m + k + 0)))) -
      appr x m
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
⊢ p ^ m ∣
    (if hy : x - ↑(appr x (m + k + 0)) = 0 then appr x (m + k + 0)
      else
        appr x (m + k + 0) +
          p ^ (m + k + 0) *
            ZMod.val
              (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k + 0))) - ↑(m + k + 0))))) -
      appr x m
split_ifs with h
case intro.succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    appr x (m + k) +
        p ^ (m + k) *
          ZMod.val
            (↑toZMod
              (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
                ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k)))) -
      appr x m
case intro.succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    appr x (m + k + 0) +
        p ^ (m + k + 0) *
          ZMod.val
            (↑toZMod
              (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
                ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k + 0))) - ↑(m + k + 0)))) -
      appr x m
dsimp
case intro.succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    p ^ (m + k) *
        ZMod.val
          (↑toZMod
            (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
              ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k)))) +
      (appr x (m + k) - appr x m)
case intro.succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    appr x (m + k) +
        p ^ (m + k) *
          ZMod.val
            (↑toZMod
              (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
                ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k)))) -
      appr x m
rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    p ^ (m + k) *
      ZMod.val
        (↑toZMod
          (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
            ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k))))
case intro.succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    p ^ (m + k) *
        ZMod.val
          (↑toZMod
            (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
              ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k)))) +
      (appr x (m + k) - appr x m)
apply dvd_add _ ih
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣ p ^ (m + k)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣
    p ^ (m + k) *
      ZMod.val
        (↑toZMod
          (↑(unitCoeff (_ : ¬x - ↑(appr x (m + k + 0)) = 0)) *
            ↑p ^ Int.natAbs (valuation (x - ↑(appr x (m + k))) - ↑(m + k))))
apply dvd_mul_of_dvd_left
no goals
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : ¬x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣ p ^ (m + k)
apply pow_dvd_pow _ (Nat.le_add_right m k)
no goals
case intro.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m : ℕ
⊢ p ^ m ∣ appr x (m + zero) - appr x m
simp only [zero_eq, add_zero, le_refl, tsub_eq_zero_of_le, ne_eq, Nat.isUnit_iff, dvd_zero]
no goals
case intro.succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ appr x (m + k) - appr x m
h : x - ↑(appr x (m + k + 0)) = 0
⊢ p ^ m ∣ appr x (m + k + 0) - appr x m
exact ih