awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    x -
      ((↑(x.appr n) : ℤ_[p]) +
        HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[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 -
      (↑(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])

Tactic:
push_cast
-- 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
neg :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    x - (↑(x.appr n) : ℤ_[p]) -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[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 -
      ((↑(x.appr n) : ℤ_[p]) +
        HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[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]))

Tactic:
rw [sub_add_eq_sub_sub]

Premises used: sub_add_eq_sub_sub
-- 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
neg :
  ∀ (c : ℤ_[p]) (hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c),
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
      x - (↑(x.appr n) : ℤ_[p]) -
        HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[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 - (↑(x.appr n) : ℤ_[p]) -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[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])

Tactic:
obtain ⟨c, hc⟩ := ih x
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
neg :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    x - (↑(x.appr n) : ℤ_[p]) -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0
              (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    x - (↑(x.appr n) : ℤ_[p]) -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[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])

Tactic:
simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]

Premises used: ZMod.natCast_self, ZMod.natCast_val, map_pow, map_mul, map_natCast
-- 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
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * 0
⊢ x - (↑(x.appr n) : ℤ_[p]) = 0

Tactic:
simp only [mul_zero] at hc

Premises used: MulZeroClass.mul_zero
-- 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
hc : x - (↑(x.appr n) : ℤ_[p]) = 0
⊢ False

Tactic:
contradiction
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
⊢ c ≠ 0

Tactic:
have hc' : c ≠ 0 := by
      rintro rfl
      simp only [mul_zero] at hc
      contradiction
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
a : x - (↑(x.appr n) : ℤ_[p])
a₁ :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
    (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
        (HPow.hPow (α := ZMod p) 0
          (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast
| x - (↑(x.appr n) : ℤ_[p]) -
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) 0
            (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast

Tactic:
congr
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
a : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
| x - (↑(x.appr n) : ℤ_[p])

Tactic:
simp only [hc]
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
a : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
a₁ :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
    (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
        (HPow.hPow (α := ZMod p) 0
          (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast
| x - (↑(x.appr n) : ℤ_[p]) -
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) 0
            (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast

Tactic:
congr
      simp only [hc]
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
neg :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0
              (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    x - (↑(x.appr n) : ℤ_[p]) -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0
              (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast

Tactic:
conv_rhs =>
      congr
      simp only [hc]
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
rw rw₁ : (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation = (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation
⊢ (x - (↑(x.appr n) : ℤ_[p])).valuation = (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation

Tactic:
rw [hc]
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
neg :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0
              (HSub.hSub (α := ℤ) (↑(HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation : ℤ) (↑n : ℤ)).natAbs)).cast
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0
              (HSub.hSub (α := ℤ) (↑(x - (↑(x.appr n) : ℤ_[p])).valuation : ℤ) (↑n : ℤ)).natAbs)).cast

Tactic:
rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
neg :
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * (↑p : ℤ_[p]) ∣
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
      (c -
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast)
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c -
      HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0
              (HSub.hSub (α := ℤ) (↑(HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation : ℤ) (↑n : ℤ)).natAbs)).cast

Tactic:
rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]

Premises used: mul_sub, add_sub_cancel_left, pow_succ, Nat.cast_add, PadicInt.valuation_p_pow_mul
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
neg :
  (↑p : ℤ_[p]) ∣
    c -
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * (↑p : ℤ_[p]) ∣
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n *
      (c -
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast)

Tactic:
apply mul_dvd_mul_left

Premises used: mul_dvd_mul_left
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
neg :
  ∀ (hc0 : c.valuation = 0),
    (↑p : ℤ_[p]) ∣
      c -
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast
neg₁ :
  ∀ (hc0 : c.valuation ≠ 0),
    (↑p : ℤ_[p]) ∣
      c -
        (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
            (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast
⊢ (↑p : ℤ_[p]) ∣
    c -
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast

Tactic:
obtain hc0 | hc0 := eq_or_ne c.valuation 0

Premises used: eq_or_ne, OfNat.ofNat, PadicInt.valuation
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
neg : (↑p : ℤ_[p]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))
⊢ (↑p : ℤ_[p]) ∣
    c -
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast

Tactic:
simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]

Premises used: Int.natAbs_zero, pow_zero, Nat.cast_zero, mul_one
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n

Tactic:
rw [mul_comm, unitCoeff_spec h] at hc

Premises used: mul_comm, PadicInt.unitCoeff_spec
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
hc₁ :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
⊢ c ≠ 0

Tactic:
rw [mul_comm, unitCoeff_spec h] at hc

Premises used: mul_comm, PadicInt.unitCoeff_spec
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation = 0
hc₁ :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc'₁ : c ≠ 0
⊢ c.valuation = 0

Tactic:
rw [mul_comm, unitCoeff_spec h] at hc

Premises used: mul_comm, PadicInt.unitCoeff_spec
-- 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
c : ℤ_[p]
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = (↑(unitCoeff h) : ℤ_[p])
rw : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) c))
⊢ (↑p : ℤ_[p]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))

Tactic:
rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]

Premises used: PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton
-- 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
c : ℤ_[p]
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : c ≠ 0
hc0 : c.valuation = 0
this : c = (↑(unitCoeff h) : ℤ_[p])
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) c))

Tactic:
apply toZMod_spec

Premises used: PadicInt.toZMod_spec
-- 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
c : ℤ_[p]
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : c ≠ 0
hc0 : c.valuation = 0
neg : c = (↑(unitCoeff h) : ℤ_[p])
⊢ (↑p : ℤ_[p]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))

Tactic:
suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
-- 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
c : ℤ_[p]
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : c ≠ 0
hc0 : c.valuation = 0
⊢ IsUnit c

Tactic:
simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]

Premises used: PadicInt.norm_eq_zpow_neg_valuation, PadicInt.isUnit_iff
-- 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
c : ℤ_[p]
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    c * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : c ≠ 0
hc0 : c.valuation = 0
neg :
  ∀ (c : ℤ_[p]ˣ)
    (hc :
      (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
        (↑c : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n)
    (hc' : (↑c : ℤ_[p]) ≠ 0) (hc0 : (↑c : ℤ_[p]).valuation = 0), (↑c : ℤ_[p]) = (↑(unitCoeff h) : ℤ_[p])
⊢ c = (↑(unitCoeff h) : ℤ_[p])

Tactic:
lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
-- 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
c : ℤ_[p]ˣ
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    (↑c : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : (↑c : ℤ_[p]) ≠ 0
hc0 : (↑c : ℤ_[p]).valuation = 0
rw : Irreducible (M := ℤ_[p]) (↑p : ℤ_[p])
⊢ (↑c : ℤ_[p]) = (↑(unitCoeff h) : ℤ_[p])

Tactic:
rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]

Premises used: IsDiscreteValuationRing.unit_mul_pow_congr_unit
-- 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
c : ℤ_[p]ˣ
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    (↑c : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : (↑c : ℤ_[p]) ≠ 0
hc0 : (↑c : ℤ_[p]).valuation = 0
⊢ Irreducible (M := ℤ_[p]) (↑p : ℤ_[p])

Tactic:
irreducible_p

Premises used: PadicInt.irreducible_p
-- 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
c : ℤ_[p]ˣ
hc :
  (↑(unitCoeff h) : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (x - (↑(x.appr n) : ℤ_[p])).valuation =
    (↑c : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n
hc' : (↑c : ℤ_[p]) ≠ 0
hc0 : (↑c : ℤ_[p]).valuation = 0
⊢ Irreducible (M := ℤ_[p]) (↑p : ℤ_[p])

Tactic:
exact irreducible_p

Premises used: PadicInt.irreducible_p
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
neg : (↑p : ℤ_[p]) ∣ c
⊢ (↑p : ℤ_[p]) ∣
    c -
      (HMul.hMul (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]) : ZMod p)
          (HPow.hPow (α := ZMod p) 0 (Int.natAbs (↑c.valuation : ℤ)))).cast

Tactic:
simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]

Premises used: sub_zero, MulZeroClass.mul_zero, ZMod.cast_zero, Int.natAbs_natCast, zero_pow
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
neg : (↑p : ℤ_[p]) ∣ (↑(unitCoeff hc') : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) c.valuation
⊢ (↑p : ℤ_[p]) ∣ c

Tactic:
rw [unitCoeff_spec hc']

Premises used: PadicInt.unitCoeff_spec
-- 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
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ (↑p : ℤ_[p]) ∣ (↑(unitCoeff hc') : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) c.valuation

Tactic:
(dvd_pow_self (p : ℤ_[p]) hc0).mul_left _

Premises used: Dvd.dvd.mul_left, Nat.cast, dvd_pow_self