-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem lift_sub_val_mem_span (r : R) (n : ℕ) :
    lift f_compat r - (f n r).val ∈ (Ideal.span {(p : ℤ_[p]) ^ n})

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n ∣ ↑(nthHom f r (n ⊔ k)) - ↑((f n) r).val

Tactic:
convert
  (Int.castRingHom ℤ_[p]).map_dvd (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))

Result:
case h.e'_3
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n = (Int.castRingHom ℤ_[p]) (↑p ^ n)

case h.e'_4
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (n ⊔ k)) - ↑((f n) r).val = (Int.castRingHom ℤ_[p]) (nthHom f r (n ⊔ k) - nthHom f r n)

Proof state:
case h.e'_4
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (n ⊔ k)) - ↑((f n) r).val =
    (Int.castRingHom ℤ_[p]) (nthHom f r (n ⊔ k)) - (Int.castRingHom ℤ_[p]) (nthHom f r n)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑p ^ n = (Int.castRingHom ℤ_[p]) ↑p ^ n

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_4
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (n ⊔ k)) - ↑((f n) r).val = (Int.castRingHom ℤ_[p]) (nthHom f r (n ⊔ k) - nthHom f r n)

Tactic:
rw [map_sub]

Result:
case h.e'_4
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
this : limNthHom f_compat r - ↑(nthHom f r (n ⊔ k)) ∈ Ideal.span {↑p ^ n}
⊢ ↑(nthHom f r (n ⊔ k)) - ↑((f n) r).val =
    (Int.castRingHom ℤ_[p]) (nthHom f r (n ⊔ k)) - (Int.castRingHom ℤ_[p]) (nthHom f r n)

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n : ℕ
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
obtain ⟨k, hk⟩ :=
  limNthHom_spec f_compat r _
    (show (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) from zpow_pos (mod_cast hp_prime.1.pos) _)

Result:
case intro
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
n k : ℕ
hk : ∀ n_1 ≥ k, ‖limNthHom f_compat r - ↑(nthHom f r n_1)‖ < ↑p ^ (-↑n)
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}