awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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]) -
    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
have 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
Tactic: congr
      simp only [hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ 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
have 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
Tactic: conv_rhs =>
      congr
      simp only [hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (x - (↑(x.appr n) : ℤ_[p])).valuation = (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation
have rw : (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation = (HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c).valuation
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ 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
have 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
Tactic: rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ 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
have 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)
Tactic: rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ 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)
have 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
Tactic: apply mul_dvd_mul_left
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (↑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
have 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
Tactic: obtain hc0 | hc0 := eq_or_ne c.valuation 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (↑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
have 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
Tactic: obtain hc0 | hc0 := eq_or_ne c.valuation 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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]) ∣
    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
have neg : (↑p : ℤ_[p]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))
Tactic: simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))
have hc₁ : (↑(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
Cleared hypotheses: hc, hc', hc0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])
⊢ (↑p : ℤ_[p]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))
have rw : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) c))
Tactic: rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (↑p : ℤ_[p]) ∣ c - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) (↑(unitCoeff h) : ℤ_[p]))
have neg : c = (↑(unitCoeff h) : ℤ_[p])
Tactic: suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ c = (↑(unitCoeff h) : ℤ_[p])
have 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])
Tactic: lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
Cleared hypotheses: c, hc, hc', hc0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (↑c : ℤ_[p]) = (↑(unitCoeff h) : ℤ_[p])
have rw : Irreducible (M := ℤ_[p]) (↑p : ℤ_[p])
Tactic: rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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]) ∣
    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
have neg : (↑p : ℤ_[p]) ∣ c
Tactic: simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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]) ∣ c
have neg : (↑p : ℤ_[p]) ∣ (↑(unitCoeff hc') : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) c.valuation
Tactic: rw [unitCoeff_spec hc']
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
have zero : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 0 ∣ x - (↑(x.appr 0) : ℤ_[p])
Tactic: induction n with
  | zero => simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
  | succ n ih =>
    intro x
    dsimp only [appr]
    split_ifs with h
    · rw [h]
      apply dvd_zero
    push_cast
    rw [sub_add_eq_sub_sub]
    obtain ⟨c, hc⟩ := ih x
    simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]
    have hc' : c ≠ 0 := by
      rintro rfl
      simp only [mul_zero] at hc
      contradiction
    conv_rhs =>
      congr
      simp only [hc]
    rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
    rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]
    apply mul_dvd_mul_left
    obtain hc0 | hc0 := eq_or_ne c.valuation 0
    · simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
      rw [mul_comm, unitCoeff_spec h] at hc
      suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
      lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
      rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
      exact irreducible_p
    · simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
      rw [unitCoeff_spec hc']
      exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
zero : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 0 ∣ x - (↑(x.appr 0) : ℤ_[p])
⊢ ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
have succ : ∀ (n : ℕ) (ih : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])) (x : ℤ_[p]),
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr (n + 1)) : ℤ_[p])
Tactic: induction n with
  | zero => simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
  | succ n ih =>
    intro x
    dsimp only [appr]
    split_ifs with h
    · rw [h]
      apply dvd_zero
    push_cast
    rw [sub_add_eq_sub_sub]
    obtain ⟨c, hc⟩ := ih x
    simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]
    have hc' : c ≠ 0 := by
      rintro rfl
      simp only [mul_zero] at hc
      contradiction
    conv_rhs =>
      congr
      simp only [hc]
    rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
    rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]
    apply mul_dvd_mul_left
    obtain hc0 | hc0 := eq_or_ne c.valuation 0
    · simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
      rw [mul_comm, unitCoeff_spec h] at hc
      suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
      lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
      rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
      exact irreducible_p
    · simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
      rw [unitCoeff_spec hc']
      exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x_1 : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])})
    (x_1 - (↑((fun (x : ℤ_[p]) ↦ x.appr n) x_1) : ℤ_[p]))
have rw : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
  (x_1 - (↑((fun (x : ℤ_[p]) ↦ x.appr n) x_1) : ℤ_[p]))
Tactic: rw [Nat.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑b : ℤ_[p]))
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))
have ha₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑a : ℤ_[p]))
Tactic: apply zmod_congr_of_sub_mem_span n x a b
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑b : ℤ_[p]))
ha₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑a : ℤ_[p]))
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))
have hb₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑b : ℤ_[p]))
Tactic: apply zmod_congr_of_sub_mem_span n x a b
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n)) (toZModPow m)
have h₁ : Eq (α := Ideal ℤ_[p])
  (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m))) (toZModPow n)))
  (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m))
Tactic: apply ZMod.ringHom_eq_of_ker_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ Eq (α := Ideal ℤ_[p])
    (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n)))
    (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m))
have h₁ : ∀ (x : ℤ_[p]),
  Membership.mem (γ := Ideal ℤ_[p])
      (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m))) (toZModPow n))) x ↔
    Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p])
      (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n))) x ↔
    Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m)) x
have h₁ : Eq (α := ZMod (p ^ m))
    ((RingHom.comp (ZMod.castHom sorry (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
    (0 : ZMod (p ^ m)) ↔
  Eq (α := ZMod (p ^ m)) ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m)) (0 : ZMod (p ^ m))
Tactic: rw [RingHom.mem_ker, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Eq (α := ZMod (p ^ m))
      ((RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
      (0 : ZMod (p ^ m)) ↔
    Eq (α := ZMod (p ^ m)) ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m)) (0 : ZMod (p ^ m))
have h₁ : Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x)) 0 ↔
  Eq (α := ZMod (p ^ m)) ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m)) (0 : ZMod (p ^ m))
Tactic: simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Eq (α := ZMod (p ^ m))
      (ZMod.cast (n := p ^ n)
        (({ toFun := fun (x : ℤ_[p]) ↦ (↑(x.appr n) : ZMod (p ^ n)), map_one' := ⋯, map_mul' := ⋯ } :
            (a : ℤ_[p]) → ZMod (p ^ n))
          x))
      0 ↔
    Eq (α := ZMod (p ^ m))
      (({ toFun := fun (x : ℤ_[p]) ↦ (↑(x.appr m) : ZMod (p ^ m)), map_one' := ⋯, map_mul' := ⋯ } :
            (a : ℤ_[p]) → ZMod (p ^ m))
          x :
        ZMod (p ^ m))
      (0 : ZMod (p ^ m))
have h₁ : Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) (↑(x.appr n) : ZMod (p ^ n))) 0 ↔
  Eq (α := ZMod (p ^ m)) (↑(x.appr m) : ZMod (p ^ m)) 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) (↑(x.appr n) : ZMod (p ^ n))) 0 ↔
    Eq (α := ZMod (p ^ m)) (↑(x.appr m) : ZMod (p ^ m)) 0
have h₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
  (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr n) : ℤ_[p]))
Tactic: rw [ZMod.cast_natCast (pow_dvd_pow p h),
    zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr n) : ℤ_[p]))
⊢ Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) (↑(x.appr n) : ZMod (p ^ n))) 0 ↔
    Eq (α := ZMod (p ^ m)) (↑(x.appr m) : ZMod (p ^ m)) 0
have h₂ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
  (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]))
Tactic: rw [ZMod.cast_natCast (pow_dvd_pow p h),
    zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr n) : ℤ_[p]))
have h₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m}) 0
Tactic: rw [sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]))
have h₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])
Tactic: rw [Ideal.mem_span_singleton]