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
r : R
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
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
r : R
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
intro ε hε
case intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'0 : 0 < ↑ε'
hε' : ↑ε' < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
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
r : R
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
obtain ⟨ε', hε'0, hε'⟩ : ∃ v : ℚ, (0 : ℝ) < v ∧ ↑v < ε := exists_rat_btwn hε
case intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
case intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'0 : 0 < ↑ε'
hε' : ↑ε' < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
norm_cast  at hε'0
case intro.intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
case intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0
case intro.intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
case intro.intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
use N
case intro.intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
case intro.intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
⊢ ∀ (n : ℕ), n ≥ N → ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
intro n hn
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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ↑ε'
case intro.intro.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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
apply _root_.lt_trans _ 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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑(↑padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n))) < ↑ε'
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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ↑ε'
change (padicNormE _  : ℝ) < _
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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n)) < ε'
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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑(↑padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n))) < ↑ε'
norm_cast
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
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : ↑ε' < ε
hε'0 : 0 < ε'
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (mk (nthHomSeq f_compat r) - ↑(↑(nthHomSeq f_compat r) i)) < ε'
n : ℕ
hn : n ≥ N
⊢ ↑padicNormE ↑(limNthHom f_compat r - ↑(nthHom f r n)) < ε'
exact hN _ hn