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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ ↑(lift f_compat) r = ↑g 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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
⊢ lift f_compat = g
ext1 r
case a.h
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ ∀ (ε : ℝ), ε > 0 → dist (↑(lift f_compat) r) (↑g 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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ ↑(lift f_compat) r = ↑g r
apply eq_of_forall_dist_le
case a.h
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ε
case a.h
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ ∀ (ε : ℝ), ε > 0 → dist (↑(lift f_compat) r) (↑g r) ≤ ε
intro ε hε
case a.h.intro
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ε
case a.h
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ε
obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ↑p ^ (-↑n)
case a.h.intro
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ε
apply le_trans _ (le_of_lt hn)
no goals
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
⊢ dist (↑(lift f_compat) r) (↑g r) ≤ ↑p ^ (-↑n)
rw [dist_eq_norm, norm_le_pow_iff_mem_span_pow, ← ker_toZModPow, RingHom.mem_ker,
  RingHom.map_sub, ← RingHom.comp_apply, ← RingHom.comp_apply, lift_spec, hg, sub_self]