case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (n : ℕ), appr x n ≤ appr x (n + 1)
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ Monotone (appr x)
apply monotone_nat_of_le_succ
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n ≤ appr x (n + 1)
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
⊢ ∀ (n : ℕ), appr x n ≤ appr x (n + 1)
intro n
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n ≤
    if hy : x - ↑(appr x (n + 0)) = 0 then appr x (n + 0)
    else
      appr x (n + 0) +
        p ^ (n + 0) *
          ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (n + 0))) - ↑(n + 0))))
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n ≤ appr x (n + 1)
dsimp [appr]
case hf.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
h✝ : x - ↑(appr x (n + 0)) = 0
⊢ appr x n ≤ appr x (n + 0)

case hf.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(appr x (n + 0)) = 0
⊢ appr x n ≤
    appr x (n + 0) +
      p ^ (n + 0) *
        ZMod.val
          (↑toZMod
            (↑(unitCoeff (_ : ¬x - ↑(appr x (n + 0)) = 0)) *
              ↑p ^ Int.natAbs (valuation (x - ↑(appr x (n + 0))) - ↑(n + 0))))
case hf
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n ≤
    if hy : x - ↑(appr x (n + 0)) = 0 then appr x (n + 0)
    else
      appr x (n + 0) +
        p ^ (n + 0) *
          ZMod.val (↑toZMod (↑(unitCoeff hy) * ↑p ^ Int.natAbs (valuation (x - ↑(appr x (n + 0))) - ↑(n + 0))))
split_ifs
no goals
case hf.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
h✝ : ¬x - ↑(appr x (n + 0)) = 0
⊢ appr x n ≤
    appr x (n + 0) +
      p ^ (n + 0) *
        ZMod.val
          (↑toZMod
            (↑(unitCoeff (_ : ¬x - ↑(appr x (n + 0)) = 0)) *
              ↑p ^ Int.natAbs (valuation (x - ↑(appr x (n + 0))) - ↑(n + 0))))
apply Nat.le_add_right
no goals
case hf.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
h✝ : x - ↑(appr x (n + 0)) = 0
⊢ appr x n ≤ appr x (n + 0)
rfl