-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem ker_toZModPow (n : ℕ) :
    RingHom.ker (toZModPow n : ℤ_[p] →+* ZMod (p ^ n)) = Ideal.span {(p : ℤ_[p]) ^ n}

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
this : x.appr n = 0
⊢ x ∈ Ideal.span {↑p ^ n}

Tactic:
convert appr_spec n x

Result:
case h.e'_5
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
this : x.appr n = 0
⊢ x = x - ↑(x.appr n)

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0

Tactic:
rw [← sub_zero x] at h

Result:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0

Proof state:
case h.e'_5
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
this : x.appr n = 0
⊢ x = x - ↑(x.appr n)

Tactic:
simp only [this, sub_zero, cast_zero]

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
⊢ RingHom.ker (toZModPow n) = Ideal.span {↑p ^ n}

Tactic:
ext x

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ x ∈ RingHom.ker (toZModPow n) ↔ x ∈ Ideal.span {↑p ^ n}

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
constructor

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (toZModPow n) x = 0 → x ∈ Ideal.span {↑p ^ n}

case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ x ∈ Ideal.span {↑p ^ n} → (toZModPow n) x = 0

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ x ∈ RingHom.ker (toZModPow n) ↔ x ∈ Ideal.span {↑p ^ n}

Tactic:
rw [RingHom.mem_ker]

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (toZModPow n) x = 0 ↔ x ∈ Ideal.span {↑p ^ n}

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}

Tactic:
apply appr_spec

Result:
no goals

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ x ∈ Ideal.span {↑p ^ n} → (toZModPow n) x = 0

Tactic:
intro h

Result:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : ↑(x.appr n) = 0
⊢ x.appr n = 0

Tactic:
rw [ZMod.natCast_zmod_eq_zero_iff_dvd] at h

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ x.appr n
⊢ x.appr n = 0

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : p ^ n ∣ x.appr n
⊢ x.appr n = 0

Tactic:
apply eq_zero_of_dvd_of_lt h (appr_lt _ _)

Result:
no goals

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
⊢ x ∈ Ideal.span {↑p ^ n}

Tactic:
suffices x.appr n = 0 by
  convert appr_spec n x
  simp only [this, sub_zero, cast_zero]

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
⊢ x.appr n = 0

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ (toZModPow n) x = 0

Tactic:
dsimp [toZModPow, toZModHom]

Result:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(x.appr n) = 0

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
⊢ (toZModPow n) x = 0 → x ∈ Ideal.span {↑p ^ n}

Tactic:
intro h

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
⊢ x ∈ Ideal.span {↑p ^ n}

Proof state:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
⊢ x.appr n = 0

Tactic:
dsimp [toZModPow, toZModHom] at h

Result:
case h.mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : ↑(x.appr n) = 0
⊢ x.appr n = 0

Proof state:
case h.mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ ↑(x.appr n) = 0

Tactic:
rw [zmod_congr_of_sub_mem_span n x _ 0 _ h, cast_zero]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x - 0 ∈ Ideal.span {↑p ^ n}
⊢ x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}