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 : ℕ
hn : OfNat.ofNat n < p
h : ∀ (hn : OfNat.ofNat 0 < p), Eq (α := ℤ_[p]) (OfNat.ofNat 0) (↑(OfNat.ofNat 0) : ℤ_[p])
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℤ_[p])
have h₁ : ∀ (hn : OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1) < p),
  Eq (α := ℤ_[p]) (OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) (↑(OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) : ℤ_[p])
Tactic: rcases n with _ | _ | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
hn : OfNat.ofNat n < p
h : ∀ (hn : OfNat.ofNat 0 < p), Eq (α := ℤ_[p]) (OfNat.ofNat 0) (↑(OfNat.ofNat 0) : ℤ_[p])
h₁ :
  ∀ (hn : OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1) < p),
    Eq (α := ℤ_[p]) (OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) (↑(OfNat.ofNat (HAdd.hAdd (α := ℕ) 0 1)) : ℤ_[p])
⊢ Eq (α := ℤ_[p]) (OfNat.ofNat n) (↑(OfNat.ofNat n) : ℤ_[p])
have h₂ : ∀ (n : ℕ) (hn : OfNat.ofNat (n + 1 + 1) < p),
  Eq (α := ℤ_[p]) (OfNat.ofNat (n + 1 + 1)) (↑(OfNat.ofNat (n + 1 + 1)) : ℤ_[p])
Tactic: rcases n with _ | _ | n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ (↑x : ℤ_[p]).zmodRepr ≠ 0
have rw : ¬(↑p : ℤ_[p]) ∣ (↑x : ℤ_[p])
Tactic: rw [ne_eq, zmodRepr_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Eq (α := ZMod v) (↑(f 1) : ZMod v) 1
have a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑(f 1) : ℤ_[p]))
Tactic: rw [f_congr (1 : ℤ_[p]) _ 1, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑(f 1) : ℤ_[p]))
⊢ Eq (α := ZMod v) (↑(f 1) : ZMod v) 1
have a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 1 (↑1 : ℤ_[p]))
Tactic: rw [f_congr (1 : ℤ_[p]) _ 1, cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ (↑(f (x * y)) : ZMod v) = HMul.hMul (α := ZMod v) (↑(f x) : ZMod v) (↑(f y) : ZMod v)
have a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f (x * y)) : ℤ_[p]))
Tactic: rw [f_congr (x * y) _ (f x * f y), cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f (x * y)) : ℤ_[p]))
⊢ (↑(f (x * y)) : ZMod v) = HMul.hMul (α := ZMod v) (↑(f x) : ZMod v) (↑(f y) : ZMod v)
have a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f x * f y) : ℤ_[p]))
Tactic: rw [f_congr (x * y) _ (f x * f y), cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {(↑v : ℤ_[p])}
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x * y - (↑(f x * f y) : ℤ_[p]))
have h : x * y - (↑(f x * f y) : ℤ_[p]) = x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])
Tactic: convert! I.add_mem (I.mul_mem_left x (f_spec y)) (I.mul_mem_right ↑(f y) (f_spec x)) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
I : Ideal ℤ_[p] := Ideal.span {(↑v : ℤ_[p])}
⊢ x * y - (↑(f x * f y) : ℤ_[p]) = x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])
have h : x * y - HMul.hMul (α := ℤ_[p]) (↑(f x) : ℤ_[p]) (↑(f y) : ℤ_[p]) =
  x * (y - (↑(f y) : ℤ_[p])) + (x - (↑(f x) : ℤ_[p])) * (↑(f y) : ℤ_[p])
Tactic: rw [cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
⊢ Eq (α := ZMod v) (↑(f 0) : ZMod v) 0
have a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑(f 0) : ℤ_[p]))
Tactic: rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑(f 0) : ℤ_[p]))
⊢ Eq (α := ZMod v) (↑(f 0) : ZMod v) 0
have a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (HSub.hSub (α := ℤ_[p]) 0 (↑0 : ℤ_[p]))
Tactic: rw [f_congr (0 : ℤ_[p]) _ 0, cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ (↑(f (x + y)) : ZMod v) = HAdd.hAdd (α := ZMod v) (↑(f x) : ZMod v) (↑(f y) : ZMod v)
have a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f (x + y)) : ℤ_[p]))
Tactic: rw [f_congr (x + y) _ (f x + f y), cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f (x + y)) : ℤ_[p]))
⊢ (↑(f (x + y)) : ZMod v) = HAdd.hAdd (α := ZMod v) (↑(f x) : ZMod v) (↑(f y) : ZMod v)
have a₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f x + f y) : ℤ_[p]))
Tactic: rw [f_congr (x + y) _ (f x + f y), cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x + y - (↑(f x + f y) : ℤ_[p]))
have h : x + y - (↑(f x + f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))
Tactic: convert! Ideal.add_mem _ (f_spec x) (f_spec y) using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑(f x) : ℤ_[p]))
f_congr :
  ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑v : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod v) (↑a : ZMod v) (↑b : ZMod v)
x y : ℤ_[p]
⊢ x + y - (↑(f x + f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))
have h : x + y - HAdd.hAdd (α := ℤ_[p]) (↑(f x) : ℤ_[p]) (↑(f y) : ℤ_[p]) = x - (↑(f x) : ℤ_[p]) + (y - (↑(f y) : ℤ_[p]))
Tactic: rw [cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑x.zmodRepr : ℤ_[p]))
have rw : ∀ (x : ℤ_[p]), Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))
Tactic: rw [← maximalIdeal_eq_span_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
⊢ ∀ (x : ℤ_[p]) (a b : ℕ),
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑a : ℤ_[p])) →
      Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) (x - (↑b : ℤ_[p])) →
        Eq (α := ZMod p) (↑a : ZMod p) (↑b : ZMod p)
have rw : ∀ (x : ℤ_[p]) (a b : ℕ),
  Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑a : ℤ_[p])) →
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑b : ℤ_[p])) →
      Eq (α := ZMod p) (↑a : ZMod p) (↑b : ZMod p)
Tactic: rw [← maximalIdeal_eq_span_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x))
have h : Eq (α := ℤ_[p]) (ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x)) (↑x.zmodRepr : ℤ_[p])
Tactic: convert! sub_zmodRepr_mem x using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Eq (α := ℤ_[p]) (ZMod.cast (n := p) ((toZMod : (a : ℤ_[p]) → ZMod p) x)) (↑x.zmodRepr : ℤ_[p])
have h : Eq (α := ℤ_[p]) (ZMod.cast (n := p) (↑x.zmodRepr : ZMod p)) (↑x.zmodRepr : ℤ_[p])
Tactic: dsimp [toZMod, toZModHom]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Eq (α := ℤ_[p]) (ZMod.cast (n := p) (↑x.zmodRepr : ZMod p)) (↑x.zmodRepr : ℤ_[p])
have h : ∀ (p' : ℕ) [hp_prime : Fact (Nat.Prime (0 + p' + 1))] (x : ℤ_[0 + p' + 1]),
  Eq (α := ℤ_[0 + p' + 1]) (ZMod.cast (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1)))
    (↑x.zmodRepr : ℤ_[0 + p' + 1])
Tactic: rcases Nat.exists_eq_add_of_lt hp_prime.1.pos with ⟨p', rfl⟩
Cleared hypotheses: p, hp_prime, x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ Eq (α := ℤ_[0 + p' + 1]) (↑(ZMod.val (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1))) : ℤ_[0 + p' + 1])
    (↑x.zmodRepr : ℤ_[0 + p' + 1])
have h : ZMod.val (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1)) = x.zmodRepr
Tactic: rw [Nat.cast_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ZMod.val (n := 0 + p' + 1) (↑x.zmodRepr : ZMod (0 + p' + 1)) = x.zmodRepr
have h : x.zmodRepr < (0 + p').succ
Tactic: apply mod_eq_of_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ Eq (α := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod p) toZMod) (maximalIdeal ℤ_[p])
have h : ∀ (x : ℤ_[p]),
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod p) toZMod) x ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod p) toZMod) x ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
have h : Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) ↔
  Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
Tactic: rw [RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
have h : Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) →
  Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h :
  Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) →
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
⊢ Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
have h₁ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x →
  Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) x
⊢ Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p)
have h₁ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
Tactic: rw [← sub_zero x] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
⊢ Eq (α := ZMod p) ((toZMod : (a : ℤ_[p]) → ZMod p) x : ZMod p) (0 : ZMod p)
have h₁ : Eq (α := ZMod p) (↑x.zmodRepr : ZMod p) 0
Tactic: dsimp [toZMod, toZModHom]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
have h₁ : Eq (α := ZMod p) 0 (↑0 : ZMod p)
Tactic: convert! zmod_congr_of_sub_mem_max_ideal x _ 0 _ h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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)
⊢ Eq (α := ZMod p) (↑x.zmodRepr : ZMod p) 0
have h₂ : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - (↑x.zmodRepr : ℤ_[p]))
Tactic: convert! zmod_congr_of_sub_mem_max_ideal x _ 0 _ h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (maximalIdeal ℤ_[p]) (x - 0)
⊢ Eq (α := ZMod p) 0 (↑0 : ZMod p)
have h₁ : Eq (α := ZMod p) 0 0
Tactic: norm_cast
-- 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]
⊢ x.appr (n + 1) < p ^ (n + 1)
have 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)
Tactic: simp only [appr, map_natCast, ZMod.natCast_self, map_pow, Int.natAbs, map_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
⊢ (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)
have hp : 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
-- 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)
⊢ (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)
have pos : ∀ (h : x - (↑(x.appr n) : ℤ_[p]) = 0), x.appr n < p ^ (n + 1)
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]), 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)
⊢ (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)
have 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)
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]), 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 + 1)
have 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)
Tactic: calc
        _ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_
-- 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
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)
⊢ 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)
have neg₁ : p ^ n + p ^ n * (p - 1) = p ^ (n + 1)
Tactic: calc
        _ < p ^ n + p ^ n * (p - 1) := ?_
        _ = p ^ (n + 1) := ?_