case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
r : R
⊢ ↑(RingHom.comp (toZModPow n) (lift f_compat)) r = ↑(f n) r
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
⊢ RingHom.comp (toZModPow n) (lift f_compat) = f n
ext r
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
r : R
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
r : R
⊢ ↑(RingHom.comp (toZModPow n) (lift f_compat)) r = ↑(f n) r
rw [RingHom.comp_apply, ← ZMod.nat_cast_zmod_val (f n r), ← map_natCast <| toZModPow n, ←
  sub_eq_zero, ← RingHom.map_sub, ← RingHom.mem_ker, ker_toZModPow]
no goals
case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst✝ : NonAssocSemiring R
f : (k : ℕ) → R →+* ZMod (p ^ k)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom (_ : p ^ k1 ∣ p ^ k2) (ZMod (p ^ k1))) (f k2) = f k1
n : ℕ
r : R
⊢ ↑(lift f_compat) r - ↑(ZMod.val (↑(f n) r)) ∈ Ideal.span {↑p ^ n}
apply lift_sub_val_mem_span