-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem appr_lt (x : ℤ_[p]) (n : ℕ) : x.appr n < p ^ n

Proof state:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
⊢ (if hy : x - ↑(x.appr n) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (toZMod ↑(unitCoeff hy) *
              0 ^
                match ↑(x - ↑(x.appr n)).valuation - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ).val) <
    p ^ (n + 1)

Tactic:
split_ifs with h

Result:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : x - ↑(x.appr n) = 0
⊢ x.appr n < p ^ (n + 1)

case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ (n + 1)

Proof state:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ (n + 1)

Tactic:
calc
  _ < p ^ n + p ^ n * (p - 1) := ?_
  _ = p ^ (n + 1) := ?_

Result:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ n + p ^ n * (p - 1)

case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ p ^ n < p ^ (n + 1)

Tactic:
apply Nat.pow_lt_pow_right hp_prime.1.one_lt n.lt_add_one

Result:
no goals

Proof state:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ x.appr n +
      p ^ n *
        (toZMod ↑(unitCoeff h) *
            0 ^
              match ↑(x - ↑(x.appr n)).valuation - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ).val <
    p ^ n + p ^ n * (p - 1)

Tactic:
apply add_lt_add_of_lt_of_le (ih _)

Result:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n *
      (toZMod ↑(unitCoeff h) *
          0 ^
            match ↑(x - ↑(x.appr n)).valuation - ↑n with
            | Int.ofNat m => m
            | Int.negSucc m => m.succ).val ≤
    p ^ n * (p - 1)

Proof state:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n *
      (toZMod ↑(unitCoeff h) *
          0 ^
            match ↑(x - ↑(x.appr n)).valuation - ↑n with
            | Int.ofNat m => m
            | Int.negSucc m => m.succ).val ≤
    p ^ n * (p - 1)

Tactic:
apply Nat.mul_le_mul_left

Result:
case neg.calc_1.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val ≤
    p - 1

Proof state:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ x.appr (n + 1) < p ^ (n + 1)

Tactic:
simp only [appr, map_natCast, ZMod.natCast_self, RingHom.map_pow, Int.natAbs, RingHom.map_mul]

Result:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ (if hy : x - ↑(x.appr n) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (toZMod ↑(unitCoeff hy) *
              0 ^
                match ↑(x - ↑(x.appr n)).valuation - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ).val) <
    p ^ (n + 1)

Proof state:
case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)

Tactic:
rw [mul_tsub, mul_one, ← _root_.pow_succ]

Result:
case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)

Proof state:
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.appr 0 < p ^ 0

Tactic:
simp only [appr, zero_eq, _root_.pow_zero, zero_lt_one]

Result:
no goals

Proof state:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ (if hy : x - ↑(x.appr n) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (toZMod ↑(unitCoeff hy) *
              0 ^
                match ↑(x - ↑(x.appr n)).valuation - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ).val) <
    p ^ (n + 1)

Tactic:
have hp : p ^ n < p ^ (n + 1) := by apply Nat.pow_lt_pow_right hp_prime.1.one_lt n.lt_add_one

Result:
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
⊢ (if hy : x - ↑(x.appr n) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (toZMod ↑(unitCoeff hy) *
              0 ^
                match ↑(x - ↑(x.appr n)).valuation - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ).val) <
    p ^ (n + 1)

Proof state:
case neg.calc_1.h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val <
    p.sub 0

Tactic:
apply ZMod.val_lt

Result:
no goals

Proof state:
case neg.calc_1.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val ≤
    p - 1

Tactic:
apply le_pred_of_lt

Result:
case neg.calc_1.h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val <
    p.sub 0

Proof state:
case neg.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)

Tactic:
apply add_tsub_cancel_of_le (le_of_lt hp)

Result:
no goals

Proof state:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : x - ↑(x.appr n) = 0
⊢ x.appr n < p ^ (n + 1)

Tactic:
apply lt_trans (ih _) hp

Result:
no goals