-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem zmod_cast_comp_toZModPow (m n : ℕ) (h : m ≤ n) :
    (ZMod.castHom (pow_dvd_pow p h) (ZMod (p ^ m))).comp (@toZModPow p _ n) = @toZModPow p _ m

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

Tactic:
rw [sub_self]

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

Proof state:
case h.h.hb.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
⊢ ↑p ^ m ∣ ↑(x.appr n) - ↑(x.appr m)

Tactic:
use c

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
⊢ ↑(x.appr n) - ↑(x.appr m) = ↑p ^ m * ↑c

Proof state:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ x ∈ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) ↔ x ∈ RingHom.ker (toZModPow m)

Tactic:
rw [RingHom.mem_ker, RingHom.mem_ker]

Result:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x = 0 ↔ (toZModPow m) x = 0

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

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)]

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

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

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n) = toZModPow m

Tactic:
apply ZMod.ringHom_eq_of_ker_eq

Result:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) = RingHom.ker (toZModPow m)

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
⊢ ↑(x.appr n) - ↑(x.appr m) = ↑p ^ m * ↑c

Tactic:
rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]

Result:
no goals

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

Tactic:
rw [Ideal.mem_span_singleton]

Result:
case h.h.hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑p ^ m ∣ ↑(x.appr n) - ↑(x.appr m)

Proof state:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ({ toFun := fun x => ↑(x.appr n), map_one' := ⋯, map_mul' := ⋯ } x).cast = 0 ↔
    { toFun := fun x => ↑(x.appr m), map_one' := ⋯, map_mul' := ⋯ } x = 0

Tactic:
dsimp

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

Proof state:
case h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) = RingHom.ker (toZModPow m)

Tactic:
ext x

Result:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ x ∈ RingHom.ker ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) ↔ x ∈ RingHom.ker (toZModPow m)

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

Tactic:
apply Ideal.zero_mem _

Result:
no goals

Proof state:
case h.h.hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑p ^ m ∣ ↑(x.appr n) - ↑(x.appr m)

Tactic:
rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩

Result:
case h.h.hb.intro
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
⊢ ↑p ^ m ∣ ↑(x.appr n) - ↑(x.appr m)

Proof state:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow n)) x = 0 ↔ (toZModPow m) x = 0

Tactic:
simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]

Result:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ((toZModPow n) x).cast = 0 ↔ (toZModPow m) x = 0

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

Tactic:
simp only [toZModPow, toZModHom, RingHom.coe_mk]

Result:
case h.h
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ({ toFun := fun x => ↑(x.appr n), map_one' := ⋯, map_mul' := ⋯ } x).cast = 0 ↔
    { toFun := fun x => ↑(x.appr m), map_one' := ⋯, map_mul' := ⋯ } x = 0