p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
⊢ ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      z =
    ↑(RingHom.id ℤ_[p]) z
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
⊢ ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      z =
    z
show _ = RingHom.id _ z
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
⊢ ∀ (n : ℕ), RingHom.comp (toZModPow n) (RingHom.id ℤ_[p]) = toZModPow n
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
⊢ ↑(lift
          (_ :
            ∀ (m n : ℕ) (h : m ≤ n),
              RingHom.comp (ZMod.castHom (_ : p ^ m ∣ p ^ n) (ZMod (p ^ m))) (toZModPow n) = toZModPow m))
      z =
    ↑(RingHom.id ℤ_[p]) z
rw [@lift_unique p _ ℤ_[p] _ _ zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
n✝ : ℕ
⊢ RingHom.comp (toZModPow n✝) (RingHom.id ℤ_[p]) = toZModPow n✝
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
⊢ ∀ (n : ℕ), RingHom.comp (toZModPow n) (RingHom.id ℤ_[p]) = toZModPow n
intro
no goals
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type ?u.654027
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
z : ℤ_[p]
n✝ : ℕ
⊢ RingHom.comp (toZModPow n✝) (RingHom.id ℤ_[p]) = toZModPow n✝
rw [RingHom.comp_id]