-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem nthHomSeq_one : nthHomSeq f_compat 1 ≈ 1

Proof state:
case h
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
ε : ℚ
hε : 0 < ε
⊢ ∀ j ≥ 1, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
intro j hj

Result:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

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
ε : ℚ
hε : 0 < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
use 1

Result:
case h
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
ε : ℚ
hε : 0 < ε
⊢ ∀ j ≥ 1, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Proof state:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ ZMod.cast 1 = 1

Tactic:
rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]

Result:
no goals

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
⊢ nthHomSeq f_compat 1 ≈ 1

Tactic:
intro ε hε

Result:
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
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

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
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
change _ < _ at hε

Result:
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
ε : ℚ
hε : 0 < ε
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Proof state:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
suffices (ZMod.cast (1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]

Result:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ ZMod.cast 1 = 1

Proof state:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow (by omega) hp_prime.1.one_lt⟩

Result:
case h
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ j ≠ 0

Tactic:
omega

Result:
no goals

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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this✝ : Fact (1 < p ^ j)
this : ZMod.cast 1 = 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
simp [nthHomSeq, nthHom, this, hε]

Result:
no goals