awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
⊢ Eq (α := ZMod p) (↑x.zmodRepr : ZMod p) (↑0 : ZMod p)

Tactic:
zmod_congr_of_sub_mem_max_ideal x _ 0 _ h

Premises used: PadicInt.zmod_congr_of_sub_mem_max_ideal, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
h₁ : Eq (α := ZMod p) 0 (↑0 : ZMod p)
h₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))
⊢ Eq (α := ZMod p) (↑x.zmodRepr : ZMod p) 0

Tactic:
convert! zmod_congr_of_sub_mem_max_ideal x _ 0 _ h

Premises used: PadicInt.zmod_congr_of_sub_mem_max_ideal, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
h₁ h₂ h₃ h₄ : Eq (α := ZMod p) 0 0
⊢ Eq (α := ZMod p) 0 (↑0 : ZMod p)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))

Tactic:
apply sub_zmodRepr_mem

Premises used: PadicInt.sub_zmodRepr_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p])
    (x - (↑(ZMod.val (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x)) : ℤ_[p]))

Tactic:
simpa using toZMod_spec _

Premises used: PadicInt.toZMod_spec
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (x * y).zmodRepr = x.zmodRepr * y.zmodRepr % p

Tactic:
simp [← val_toZMod_eq_zmodRepr, ZMod.val_mul]

Premises used: ZMod.val_mul, PadicInt.val_toZMod_eq_zmodRepr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ x.appr 0 < HPow.hPow (β := ℕ) p 0

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

Premises used: pow_zero, zero_lt_one, PadicInt.appr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
succ :
  (if hy : x - (↑(x.appr n) : ℤ_[p]) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff hy) : ℤ_[p]) : ZMod p)
              (HPow.hPow (α := ZMod p) (β := ℕ) 0
                (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
                  | Int.ofNat m => m
                  | Int.negSucc m => m.succ :
                  ℕ))).val) <
    p ^ (n + 1)
⊢ x.appr (n + 1) < p ^ (n + 1)

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

Premises used: ZMod.natCast_self, map_pow, map_mul, map_natCast, Int.natAbs, PadicInt.appr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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

Premises used: Nat.Prime.one_lt, Nat.lt_add_one, Nat.pow_lt_pow_right, Fact.out
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ p ^ n < 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
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
pos : ∀ (h : x - (↑(x.appr n) : ℤ_[p]) = 0), x.appr n < p ^ (n + 1)
neg :
  ∀ (h : ¬x - (↑(x.appr n) : ℤ_[p]) = 0),
    x.appr n +
        p ^ n *
          (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
              (HPow.hPow (α := ZMod p) (β := ℕ) 0
                (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
                  | Int.ofNat m => m
                  | Int.negSucc m => m.succ :
                  ℕ))).val <
      p ^ (n + 1)
⊢ (if hy : x - (↑(x.appr n) : ℤ_[p]) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff hy) : ℤ_[p]) : ZMod p)
              (HPow.hPow (α := ZMod p) (β := ℕ) 0
                (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
                  | Int.ofNat m => m
                  | Int.negSucc m => m.succ :
                  ℕ))).val) <
    p ^ (n + 1)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
⊢ x.appr n < p ^ (n + 1)

Tactic:
apply lt_trans (ih _) hp

Premises used: lt_trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
⊢ x.appr n +
      p ^ n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) (β := ℕ) 0
              (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ :
                ℕ))).val <
    p ^ n + p ^ n * (p - 1)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)

Tactic:
?_
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
neg :
  x.appr n +
      p ^ n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) (β := ℕ) 0
              (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
                | Int.ofNat m => m
                | Int.negSucc m => m.succ :
                ℕ))).val <
    p ^ n + p ^ n * (p - 1)
neg₁ : p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
⊢ x.appr n +
      p ^ n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) (β := ℕ) 0
              (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).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) := ?_

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
neg :
  p ^ n *
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) (β := ℕ) 0
            (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ :
              ℕ))).val ≤
    p ^ n * (p - 1)
⊢ x.appr n +
      p ^ n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) (β := ℕ) 0
              (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).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 _)

Premises used: add_lt_add_of_lt_of_le
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
neg :
  (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
        (HPow.hPow (α := ZMod p) (β := ℕ) 0
          (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
            | Int.ofNat m => m
            | Int.negSucc m => m.succ :
            ℕ))).val ≤
    p - 1
⊢ p ^ n *
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) (β := ℕ) 0
            (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
              | Int.ofNat m => m
              | Int.negSucc m => m.succ :
              ℕ))).val ≤
    p ^ n * (p - 1)

Tactic:
apply Nat.mul_le_mul_left

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
neg :
  (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
        (HPow.hPow (α := ZMod p) (β := ℕ) 0
          (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
            | Int.ofNat m => m
            | Int.negSucc m => m.succ :
            ℕ))).val <
    p.sub 0
⊢ (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
        (HPow.hPow (α := ZMod p) (β := ℕ) 0
          (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
            | Int.ofNat m => m
            | Int.negSucc m => m.succ :
            ℕ))).val ≤
    p - 1

Tactic:
apply le_pred_of_lt

Premises used: Nat.le_pred_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
⊢ (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
        (HPow.hPow (α := ZMod p) (β := ℕ) 0
          (match (motive := ℤ → ℕ) HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ) with
            | Int.ofNat m => m
            | Int.negSucc m => m.succ :
            ℕ))).val <
    p.sub 0

Tactic:
apply ZMod.val_lt

Premises used: ZMod.val_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
neg : p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)
⊢ p ^ n + p ^ n * (p - 1) = p ^ (n + 1)

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

Premises used: pow_succ, mul_one, mul_tsub
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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) : ℤ_[p]) = 0
⊢ p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)

Tactic:
apply add_tsub_cancel_of_le (le_of_lt hp)

Premises used: le_of_lt, add_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
zero : ∀ (x : ℤ_[p]), x.appr 0 < HPow.hPow (β := ℕ) p 0
succ : ∀ (n : ℕ) (ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n) (x : ℤ_[p]), x.appr (n + 1) < p ^ (n + 1)
⊢ x.appr n < p ^ n

Tactic:
induction n generalizing x with
  | zero => simp only [appr, _root_.pow_zero, zero_lt_one]
  | succ n ih =>
    simp only [appr, map_natCast, ZMod.natCast_self, map_pow, Int.natAbs, map_mul]
    have hp : p ^ n < p ^ (n + 1) := by apply Nat.pow_lt_pow_right hp_prime.1.one_lt n.lt_add_one
    split_ifs with h
    · apply lt_trans (ih _) hp
    · calc
        _ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_
      · apply add_lt_add_of_lt_of_le (ih _)
        apply Nat.mul_le_mul_left
        apply le_pred_of_lt
        apply ZMod.val_lt
      · rw [mul_tsub, mul_one, ← _root_.pow_succ]
        apply add_tsub_cancel_of_le (le_of_lt hp)

Premises used: ZMod.natCast_self, pow_succ, HSub.hSub, Nat.mul_le_mul_left, map_pow, pow_zero, zero_lt_one, map_mul, Nat.le_pred_of_lt, map_natCast, HAdd.hAdd, Int.natAbs, Nat.zero, PadicInt.appr, mul_one, OfNat.ofNat, ZMod.val_lt, Nat.succ, mul_tsub
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
hf : ∀ (n : ℕ), x.appr n ≤ x.appr (n + 1)
⊢ Monotone x.appr

Tactic:
apply monotone_nat_of_le_succ

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
pos : x - (↑(x.appr n) : ℤ_[p]) = 0 → x.appr n ≤ x.appr n
neg :
  ∀ (h : ¬x - (↑(x.appr n) : ℤ_[p]) = 0),
    x.appr n ≤
      x.appr n +
        p ^ n *
          ZMod.val (n := p)
            ((toZMod : (a : ℤ_[p]) → ZMod p)
              ((↑(unitCoeff h) : ℤ_[p]) *
                HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                  (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs))
⊢ x.appr n ≤
    if hy : x - (↑(x.appr n) : ℤ_[p]) = 0 then x.appr n
    else
      x.appr n +
        p ^ n *
          ZMod.val (n := p)
            ((toZMod : (a : ℤ_[p]) → ZMod p)
              ((↑(unitCoeff hy) : ℤ_[p]) *
                HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                  (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h : x - (↑(x.appr n) : ℤ_[p]) = 0
⊢ x.appr n ≤ x.appr n

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
h : ¬x - (↑(x.appr n) : ℤ_[p]) = 0
⊢ x.appr n ≤
    x.appr n +
      p ^ n *
        ZMod.val (n := p)
          ((toZMod : (a : ℤ_[p]) → ZMod p)
            ((↑(unitCoeff h) : ℤ_[p]) *
              HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs))

Tactic:
apply Nat.le_add_right

Premises used: Nat.le_add_right
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
h : m ≤ n
obtain : ∀ (k : ℕ) (h : m ≤ m + k), p ^ m ∣ x.appr (m + k) - x.appr m
⊢ p ^ m ∣ x.appr n - x.appr m

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

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m : ℕ
⊢ p ^ m ∣ x.appr (m + 0) - x.appr m

Tactic:
simp only [add_zero, le_refl, tsub_eq_zero_of_le, dvd_zero]

Premises used: dvd_zero, le_refl, tsub_eq_zero_of_le, add_zero
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
succ : p ^ m ∣ x.appr (m + k + 1) - x.appr m
⊢ p ^ m ∣ x.appr (m + (k + 1)) - x.appr m

Tactic:
rw [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
ih : p ^ m ∣ x.appr (m + k) - x.appr m
pos : ∀ (h : x - (↑(x.appr (m + k)) : ℤ_[p]) = 0), p ^ m ∣ x.appr (m + k) - x.appr m
neg :
  ∀ (h : ¬x - (↑(x.appr (m + k)) : ℤ_[p]) = 0),
    p ^ m ∣
      x.appr (m + k) +
          p ^ (m + k) *
            ZMod.val (n := p)
              ((toZMod : (a : ℤ_[p]) → ZMod p)
                ((↑(unitCoeff h) : ℤ_[p]) *
                  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                    ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) -
                        HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs)) -
        x.appr m
⊢ p ^ m ∣
    (if hy : x - (↑(x.appr (m + k)) : ℤ_[p]) = 0 then x.appr (m + k)
      else
        x.appr (m + k) +
          p ^ (m + k) *
            ZMod.val (n := p)
              ((toZMod : (a : ℤ_[p]) → ZMod p)
                ((↑(unitCoeff hy) : ℤ_[p]) *
                  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                    ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) -
                        HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs))) -
      x.appr m

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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)) : ℤ_[p]) = 0
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Tactic:
ih
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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)) : ℤ_[p]) = 0
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Tactic:
exact ih
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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)) : ℤ_[p]) = 0
neg :
  p ^ m ∣
    p ^ (m + k) *
        ZMod.val (n := p)
          ((toZMod : (a : ℤ_[p]) → ZMod p)
            ((↑(unitCoeff h) : ℤ_[p]) *
              HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs)) +
      (x.appr (m + k) - x.appr m)
⊢ p ^ m ∣
    x.appr (m + k) +
        p ^ (m + k) *
          ZMod.val (n := p)
            ((toZMod : (a : ℤ_[p]) → ZMod p)
              ((↑(unitCoeff h) : ℤ_[p]) *
                HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                  ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs)) -
      x.appr m

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

Premises used: add_tsub_assoc_of_le, Nat.le_add_right, add_comm, PadicInt.appr_mono
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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)) : ℤ_[p]) = 0
apply :
  p ^ m ∣
    p ^ (m + k) *
      ZMod.val (n := p)
        ((toZMod : (a : ℤ_[p]) → ZMod p)
          ((↑(unitCoeff h) : ℤ_[p]) *
            HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
              ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs))
⊢ p ^ m ∣
    p ^ (m + k) *
        ZMod.val (n := p)
          ((toZMod : (a : ℤ_[p]) → ZMod p)
            ((↑(unitCoeff h) : ℤ_[p]) *
              HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs)) +
      (x.appr (m + k) - x.appr m)

Tactic:
apply dvd_add _ ih

Premises used: dvd_add
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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)) : ℤ_[p]) = 0
h₁ : p ^ m ∣ p ^ (m + k)
⊢ p ^ m ∣
    p ^ (m + k) *
      ZMod.val (n := p)
        ((toZMod : (a : ℤ_[p]) → ZMod p)
          ((↑(unitCoeff h) : ℤ_[p]) *
            HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
              ((↑(x - (↑(x.appr (m + k)) : ℤ_[p])).valuation : ℤ) - HAdd.hAdd (α := ℤ) (↑m : ℤ) (↑k : ℤ)).natAbs))

Tactic:
apply dvd_mul_of_dvd_left

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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)) : ℤ_[p]) = 0
⊢ p ^ m ∣ p ^ (m + k)

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

Premises used: Nat.le_add_right, pow_dvd_pow
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
zero : p ^ m ∣ x.appr (m + 0) - x.appr m
succ : ∀ (k : ℕ) (ih : p ^ m ∣ x.appr (m + k) - x.appr m), p ^ m ∣ x.appr (m + (k + 1)) - x.appr m
⊢ p ^ m ∣ x.appr (m + k) - x.appr m

Tactic:
induction k with
  | zero =>
    simp only [add_zero, le_refl, tsub_eq_zero_of_le, dvd_zero]
  | succ k ih =>
    rw [← add_assoc]
    dsimp [appr]
    split_ifs with h
    · exact ih
    rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
    apply dvd_add _ ih
    apply dvd_mul_of_dvd_left
    apply pow_dvd_pow _ (Nat.le_add_right m k)

Premises used: dvd_mul_of_dvd_left, dvd_zero, le_refl, add_tsub_assoc_of_le, tsub_eq_zero_of_le, add_assoc, Nat.le_add_right, pow_dvd_pow, add_comm, PadicInt.appr_mono, Nat.zero, PadicInt.appr, add_zero, Nat.succ
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
simp : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
⊢ ∀ (x : ℤ_[p]),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑(x.appr n) : ℤ_[p]))

Tactic:
simp only [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 0 ∣ x - (↑(x.appr 0) : ℤ_[p])

Tactic:
simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]

Premises used: pow_zero, IsUnit.dvd, isUnit_one, forall_const
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
x : ℤ_[p]
pos : ∀ (h : x - (↑(x.appr n) : ℤ_[p]) = 0), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr n) : ℤ_[p])
neg :
  ∀ (h : ¬x - (↑(x.appr n) : ℤ_[p]) = 0),
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
      x -
        (↑(x.appr n +
              p ^ n *
                ZMod.val (n := p)
                  ((toZMod : (a : ℤ_[p]) → ZMod p)
                    ((↑(unitCoeff h) : ℤ_[p]) *
                      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                        (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs))) :
          ℤ_[p])
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    x -
      (↑(if hy : x - (↑(x.appr n) : ℤ_[p]) = 0 then x.appr n
          else
            x.appr n +
              p ^ n *
                ZMod.val (n := p)
                  ((toZMod : (a : ℤ_[p]) → ZMod p)
                    ((↑(unitCoeff hy) : ℤ_[p]) *
                      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p])
                        (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs))) :
        ℤ_[p])

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
x : ℤ_[p]
h : x - (↑(x.appr n) : ℤ_[p]) = 0
pos : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ 0
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr n) : ℤ_[p])

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
x : ℤ_[p]
h : x - (↑(x.appr n) : ℤ_[p]) = 0
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ 0

Tactic:
apply dvd_zero

Premises used: dvd_zero