-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem dvd_appr_sub_appr (x : ℤ_[p]) (m n : ℕ) (h : m ≤ n) : p ^ m ∣ x.appr n - x.appr m

Proof state:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    x.appr (m + k) +
        p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val -
      x.appr m

Tactic:
rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]

Result:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val +
      (x.appr (m + k) - x.appr m)

Proof state:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
h : m ≤ m + k
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Tactic:
clear h

Result:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val

Tactic:
apply dvd_mul_of_dvd_left

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ p ^ (m + k)

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ p ^ (m + k)

Tactic:
apply pow_dvd_pow _ (Nat.le_add_right m k)

Result:
no goals

Proof state:
case intro.zero
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m : ℕ
⊢ p ^ m ∣ x.appr (m + 0) - x.appr m

Tactic:
simp only [zero_eq, add_zero, le_refl, tsub_eq_zero_of_le, ne_eq, Nat.isUnit_iff, dvd_zero]

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ p ^ m ∣ x.appr n - x.appr m

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Result:
case intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
h : m ≤ m + k
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Proof state:
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣
    (if hy : x - ↑(x.appr (m + k)) = 0 then x.appr (m + k)
      else
        x.appr (m + k) +
          p ^ (m + k) * (toZMod (↑(unitCoeff hy) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val) -
      x.appr m

Tactic:
split_ifs with h

Result:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    x.appr (m + k) +
        p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val -
      x.appr m

Proof state:
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣ x.appr (m + k + 1) - x.appr m

Tactic:
dsimp [appr]

Result:
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣
    (if hy : x - ↑(x.appr (m + k)) = 0 then x.appr (m + k)
      else
        x.appr (m + k) +
          p ^ (m + k) * (toZMod (↑(unitCoeff hy) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val) -
      x.appr m

Proof state:
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣ x.appr (m + (k + 1)) - x.appr m

Tactic:
rw [← add_assoc]

Result:
case intro.succ
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣ x.appr (m + k + 1) - x.appr m

Proof state:
case pos
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Tactic:
exact ih

Result:
no goals

Proof state:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣
    p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val +
      (x.appr (m + k) - x.appr m)

Tactic:
apply dvd_add _ ih

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
h : ¬x - ↑(x.appr (m + k)) = 0
⊢ p ^ m ∣ p ^ (m + k) * (toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr (m + k))).valuation - ↑(m + k)).natAbs)).val