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]), 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)
have 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)
Tactic: apply add_lt_add_of_lt_of_le (ih _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 *
      (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)
have 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
Tactic: apply Nat.mul_le_mul_left
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 - 1
have 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
Tactic: apply le_pred_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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)
have neg : p ^ n + (p ^ (n + 1) - p ^ n) = p ^ (n + 1)
Tactic: rw [mul_tsub, mul_one, ← _root_.pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ x.appr n < p ^ n
have zero : ∀ (x : ℤ_[p]), x.appr 0 < HPow.hPow (β := ℕ) p 0
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)
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
zero : ∀ (x : ℤ_[p]), x.appr 0 < HPow.hPow (β := ℕ) p 0
⊢ x.appr n < p ^ n
have succ : ∀ (n : ℕ) (ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n) (x : ℤ_[p]), x.appr (n + 1) < p ^ (n + 1)
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)
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Monotone x.appr
have hf : ∀ (n : ℕ), x.appr n ≤ x.appr (n + 1)
Tactic: apply monotone_nat_of_le_succ
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ 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))
have pos : x - (↑(x.appr n) : ℤ_[p]) = 0 → x.appr n ≤ x.appr n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
pos : x - (↑(x.appr n) : ℤ_[p]) = 0 → x.appr n ≤ x.appr n
⊢ 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))
have 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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m n : ℕ
h : m ≤ n
⊢ p ^ m ∣ x.appr n - x.appr m
have obtain : ∀ (k : ℕ) (h : m ≤ m + k), p ^ m ∣ x.appr (m + k) - x.appr m
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
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
have succ : p ^ m ∣ x.appr (m + k + 1) - x.appr m
Tactic: rw [← add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
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)) : ℤ_[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
have pos : ∀ (h : x - (↑(x.appr (m + k)) : ℤ_[p]) = 0), p ^ m ∣ x.appr (m + k) - x.appr m
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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) +
        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
have 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)
Tactic: rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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) *
        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)
have 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))
Tactic: apply dvd_add _ ih
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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) *
      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))
have h₁ : p ^ m ∣ p ^ (m + k)
Tactic: apply dvd_mul_of_dvd_left
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
⊢ p ^ m ∣ x.appr (m + k) - x.appr m
have zero : p ^ m ∣ x.appr (m + 0) - 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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
m k : ℕ
zero : p ^ m ∣ x.appr (m + 0) - x.appr m
⊢ p ^ m ∣ x.appr (m + k) - x.appr m
have succ : ∀ (k : ℕ) (ih : p ^ m ∣ x.appr (m + k) - x.appr m), p ^ m ∣ x.appr (m + (k + 1)) - 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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (x : ℤ_[p]),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑(x.appr n) : ℤ_[p]))
have simp : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
Tactic: simp only [Ideal.mem_span_singleton]
-- 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]
⊢ 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])
have pos : ∀ (h : x - (↑(x.appr n) : ℤ_[p]) = 0), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr n) : ℤ_[p])
Tactic: split_ifs with h
-- 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]
pos : ∀ (h : x - (↑(x.appr n) : ℤ_[p]) = 0), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr n) : ℤ_[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])
have 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])
Tactic: split_ifs with h
-- 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
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr n) : ℤ_[p])
have pos : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ 0
Tactic: rw [h]
-- 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
⊢ 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])
have 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]))
Tactic: push_cast
-- 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
⊢ 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]))
have 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])
Tactic: rw [sub_add_eq_sub_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
⊢ 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])
have 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])
Tactic: obtain ⟨c, hc⟩ := ih x
-- 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
⊢ 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])
have 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
Tactic: simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]
-- 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
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * 0
⊢ False
have hc₁ : x - (↑(x.appr n) : ℤ_[p]) = 0
Tactic: simp only [mul_zero] at hc
Cleared hypotheses: hc
-- 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
⊢ 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 hc' : c ≠ 0
Tactic: have hc' : c ≠ 0 := by
      rintro rfl
      simp only [mul_zero] at hc
      contradiction
-- 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 : x - (↑(x.appr n) : ℤ_[p])
| 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
-- 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])
have a : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
Tactic: 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]) -
    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 * c
Tactic: congr
      simp only [hc]