case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ x : ℤ_[p]
⊢ appr x zero < p ^ zero

case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ appr x (succ n) < p ^ succ n
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ x : ℤ_[p]
n : ℕ
⊢ appr x n < p ^ n
induction' n with n ih generalizing x
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ (if h : x - ↑(appr x n) = 0 then appr x n
    else
      appr x n +
        p ^ n *
          ZMod.val
            (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
              0 ^
                match valuation (x - ↑(appr x n)) - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => succ m)) <
    p ^ succ n
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ appr x (succ n) < p ^ succ n
simp only [appr, map_natCast, ZMod.nat_cast_self, RingHom.map_pow, Int.natAbs, RingHom.map_mul]
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
⊢ (if h : x - ↑(appr x n) = 0 then appr x n
    else
      appr x n +
        p ^ n *
          ZMod.val
            (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
              0 ^
                match valuation (x - ↑(appr x n)) - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => succ m)) <
    p ^ succ n
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ (if h : x - ↑(appr x n) = 0 then appr x n
    else
      appr x n +
        p ^ n *
          ZMod.val
            (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
              0 ^
                match valuation (x - ↑(appr x n)) - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => succ m)) <
    p ^ succ n
have hp : p ^ n < p ^ (n + 1) := by apply pow_lt_pow hp_prime.1.one_lt (lt_add_one n)
case succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : x - ↑(appr x n) = 0
⊢ appr x n < p ^ succ n

case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ appr x n +
      p ^ n *
        ZMod.val
          (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
            0 ^
              match valuation (x - ↑(appr x n)) - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => succ m) <
    p ^ succ n
case succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
⊢ (if h : x - ↑(appr x n) = 0 then appr x n
    else
      appr x n +
        p ^ n *
          ZMod.val
            (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
              0 ^
                match valuation (x - ↑(appr x n)) - ↑n with
                | Int.ofNat m => m
                | Int.negSucc m => succ m)) <
    p ^ succ n
split_ifs with h
no goals
case zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ x : ℤ_[p]
⊢ appr x zero < p ^ zero
simp only [appr, zero_eq, _root_.pow_zero, zero_lt_one]
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
⊢ p ^ n < p ^ (n + 1)
apply pow_lt_pow hp_prime.1.one_lt (lt_add_one n)
no goals
case succ.inl
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : x - ↑(appr x n) = 0
⊢ appr x n < p ^ succ n
apply lt_trans (ih _) hp
case succ.inr.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ appr x n +
      p ^ n *
        ZMod.val
          (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
            0 ^
              match valuation (x - ↑(appr x n)) - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => succ m) <
    p ^ n + p ^ n * (p - 1)

case succ.inr.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
case succ.inr
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ appr x n +
      p ^ n *
        ZMod.val
          (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
            0 ^
              match valuation (x - ↑(appr x n)) - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => succ m) <
    p ^ succ n
calc
  _ < p ^ n + p ^ n * (p - 1) := ?_
  _ = p ^ (n + 1) := ?_
case succ.inr.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n *
      ZMod.val
        (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
          0 ^
            match valuation (x - ↑(appr x n)) - ↑n with
            | Int.ofNat m => m
            | Int.negSucc m => succ m) ≤
    p ^ n * (p - 1)
case succ.inr.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ appr x n +
      p ^ n *
        ZMod.val
          (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
            0 ^
              match valuation (x - ↑(appr x n)) - ↑n with
              | Int.ofNat m => m
              | Int.negSucc m => succ m) <
    p ^ n + p ^ n * (p - 1)
apply add_lt_add_of_lt_of_le (ih _)
case succ.inr.calc_1.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ ZMod.val
      (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
        0 ^
          match valuation (x - ↑(appr x n)) - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => succ m) ≤
    p - 1
case succ.inr.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n *
      ZMod.val
        (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
          0 ^
            match valuation (x - ↑(appr x n)) - ↑n with
            | Int.ofNat m => m
            | Int.negSucc m => succ m) ≤
    p ^ n * (p - 1)
apply Nat.mul_le_mul_left
case succ.inr.calc_1.h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ ZMod.val
      (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
        0 ^
          match valuation (x - ↑(appr x n)) - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => succ m) <
    p
case succ.inr.calc_1.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ ZMod.val
      (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
        0 ^
          match valuation (x - ↑(appr x n)) - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => succ m) ≤
    p - 1
apply le_pred_of_lt
no goals
case succ.inr.calc_1.h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ ZMod.val
      (↑toZMod ↑(unitCoeff (_ : ¬x - ↑(appr x n) = 0)) *
        0 ^
          match valuation (x - ↑(appr x n)) - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => succ m) <
    p
apply ZMod.val_lt
case succ.inr.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)
case succ.inr.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
rw [mul_tsub, mul_one, ← _root_.pow_succ']
no goals
case succ.inr.calc_2
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝¹ x✝ : ℤ_[p]
n : ℕ
ih : ∀ (x : ℤ_[p]), appr x n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(appr x n) = 0
⊢ p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)
apply add_tsub_cancel_of_le (le_of_lt hp)