awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p
      (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
        ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) <
    ε

Tactic:
lt_of_le_of_lt ?_ hk

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
h :
  padicNorm p
      (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
        ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))
⊢ padicNorm p
      (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
        ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) <
    ε

Tactic:
refine lt_of_le_of_lt ?_ hk

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
h : padicNorm p (↑(nthHom f r j - nthHom f r k) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))
⊢ padicNorm p (HSub.hSub (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f r k) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
h : (↑(p ^ k) : ℤ) ∣ nthHom f r j - nthHom f r k
⊢ padicNorm p (↑(nthHom f r j - nthHom f r k) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))

Tactic:
rw [← padicNorm.dvd_iff_norm_le]

Premises used: padicNorm.dvd_iff_norm_le
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
⊢ (↑(p ^ k) : ℤ) ∣ nthHom f r j - nthHom f r k

Tactic:
mod_cast pow_dvd_nthHom_sub f_compat r k j hj

Premises used: Dvd.dvd, PadicInt.pow_dvd_nthHom_sub, congrArg, HSub.hSub, cast, congrFun', PadicInt.nthHom, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
⊢ (↑(p ^ k) : ℤ) ∣ nthHom f r j - nthHom f r k

Tactic:
exact mod_cast pow_dvd_nthHom_sub f_compat r k j hj

Premises used: PadicInt.pow_dvd_nthHom_sub
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : ε > 0
⊢ 0 < ε

Tactic:
change _ < _ at hε
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
h : ∀ j ≥ 1, padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε

Tactic:
use 1
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ j ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ Fact (1 < p ^ j)

Tactic:
haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow (by lia) hp_prime.1.one_lt⟩
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this_1 : Fact (1 < p ^ j)
this : Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1
⊢ padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε

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

Premises used: PadicInt.nthHomSeq, PadicInt.nthHom
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
h : Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1
⊢ padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε

Tactic:
suffices (ZMod.cast (1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
h : Eq (α := ℚ) (↑(ZMod.val (n := p ^ j) 1) : ℚ) 1
h₁ : Eq (α := ℚ) (↑1 : ℚ) 1
h₂ h₃ : Eq (α := ℚ) 1 1
⊢ Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1

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

Premises used: ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
obtain :
  ∀ (n : ℕ) (hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε),
    ∃ (i : ℕ),
      ∀ j ≥ i,
        padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε

Premises used: PadicInt.exists_pow_neg_lt_rat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
h : ∀ j ≥ n, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε

Tactic:
use n
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
apply :
  padicNorm p ((↑(nthHom f (r + s) j) : ℚ) - HAdd.hAdd (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
⊢ padicNorm p ((↑(nthHom f (r + s) j) : ℚ) - HAdd.hAdd (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) < ε

Tactic:
apply lt_of_le_of_lt _ hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
rw : Eq (α := ZMod (p ^ n)) (↑(nthHom f (r + s) j - (nthHom f r j + nthHom f s j)) : ZMod (p ^ n)) 0
⊢ padicNorm p ((↑(nthHom f (r + s) j) : ℚ) - HAdd.hAdd (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
rw [← Int.cast_add, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
    ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: Int.cast_sub, Int.cast_add, padicNorm.dvd_iff_norm_le, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
simp :
  (HAdd.hAdd (α := ZMod (p ^ j)) (β := ZMod (p ^ j)) ((f j : (a : R) → ZMod (p ^ j)) r : ZMod (p ^ j))
          ((f j : (a : R) → ZMod (p ^ j)) s : ZMod (p ^ j))).cast -
      HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0
⊢ Eq (α := ZMod (p ^ n))
    (↑((↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) (r + s))) : ℤ) -
          HAdd.hAdd (α := ℤ) (↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ)
            (↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) : ℤ)) :
      ZMod (p ^ n))
    0

Tactic:
simp only [ZMod.natCast_val, map_add, Int.cast_sub, ZMod.intCast_cast, Int.cast_add]

Premises used: Int.cast_sub, Int.cast_add, map_add, ZMod.natCast_val, ZMod.intCast_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
rw :
  HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) -
      HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0
⊢ (HAdd.hAdd (α := ZMod (p ^ j)) (β := ZMod (p ^ j)) ((f j : (a : R) → ZMod (p ^ j)) r : ZMod (p ^ j))
          ((f j : (a : R) → ZMod (p ^ j)) s : ZMod (p ^ j))).cast -
      HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0

Tactic:
rw [ZMod.cast_add (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj)]

Premises used: pow_dvd_pow, ZMod.cast_add
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
⊢ HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) -
      HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0

Tactic:
simp only [sub_self]

Premises used: sub_self
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
obtain :
  ∀ (n : ℕ) (hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε),
    ∃ (i : ℕ),
      ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε

Premises used: PadicInt.exists_pow_neg_lt_rat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
h : ∀ j ≥ n, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε

Tactic:
use n
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
apply :
  padicNorm p ((↑(nthHom f (r * s) j) : ℚ) - HMul.hMul (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
⊢ padicNorm p ((↑(nthHom f (r * s) j) : ℚ) - HMul.hMul (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) < ε

Tactic:
apply lt_of_le_of_lt _ hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
rw : Eq (α := ZMod (p ^ n)) (↑(nthHom f (r * s) j - nthHom f r j * nthHom f s j) : ZMod (p ^ n)) 0
⊢ padicNorm p ((↑(nthHom f (r * s) j) : ℚ) - HMul.hMul (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
rw [← Int.cast_mul, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
    ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: Int.cast_sub, padicNorm.dvd_iff_norm_le, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_mul
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
simp :
  (HMul.hMul (α := ZMod (p ^ j)) (β := ZMod (p ^ j)) ((f j : (a : R) → ZMod (p ^ j)) r : ZMod (p ^ j))
          ((f j : (a : R) → ZMod (p ^ j)) s : ZMod (p ^ j))).cast -
      HMul.hMul (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0
⊢ Eq (α := ZMod (p ^ n))
    (↑((↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) (r * s))) : ℤ) -
          HMul.hMul (α := ℤ) (↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ)
            (↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) : ℤ)) :
      ZMod (p ^ n))
    0

Tactic:
simp only [ZMod.natCast_val, map_mul, Int.cast_sub, ZMod.intCast_cast, Int.cast_mul]

Premises used: Int.cast_sub, ZMod.natCast_val, map_mul, Int.cast_mul, ZMod.intCast_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
rw :
  HMul.hMul (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) -
      HMul.hMul (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0
rw₁ rw₂ : Eq (α := ZMod (p ^ n)) 0 0
⊢ (HMul.hMul (α := ZMod (p ^ j)) (β := ZMod (p ^ j)) ((f j : (a : R) → ZMod (p ^ j)) r : ZMod (p ^ j))
          ((f j : (a : R) → ZMod (p ^ j)) s : ZMod (p ^ j))).cast -
      HMul.hMul (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0

Tactic:
rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]

Premises used: sub_self, pow_dvd_pow, ZMod.cast_mul
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
⊢ ∃ (v : ℚ), LT.lt (α := ℝ) 0 (↑v : ℝ) ∧ (↑v : ℝ) < ε

Tactic:
exists_rat_btwn hε

Premises used: exists_rat_btwn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (ε' : ℚ) (hε'0 : LT.lt (α := ℝ) 0 (↑ε' : ℝ)) (hε' : (↑ε' : ℝ) < ε),
    ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε

Tactic:
obtain ⟨ε', hε'0, hε'⟩ : ∃ v : ℚ, (0 : ℝ) < v ∧ ↑v < ε := exists_rat_btwn hε

Premises used: exists_rat_btwn, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'0 : LT.lt (α := ℝ) 0 (↑ε' : ℝ)
hε' : (↑ε' : ℝ) < ε
⊢ 0 < ε'

Tactic:
norm_cast at hε'0
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : (↑ε' : ℝ) < ε
hε'0 : 0 < ε'
obtain :
  ∀ (N : ℕ)
    (hN :
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            (HSub.hSub (α := ℚ_[p]) (mk (nthHomSeq f_compat r)) (↑((↑(nthHomSeq f_compat r) : ℕ → ℚ) i) : ℚ_[p])) <
          ε'),
    ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε

Tactic:
obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0

Premises used: PadicInt.nthHomSeq, padicNormE.defn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : (↑ε' : ℝ) < ε
hε'0 : 0 < ε'
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        (HSub.hSub (α := ℚ_[p]) (mk (nthHomSeq f_compat r)) (↑((↑(nthHomSeq f_compat r) : ℕ → ℚ) i) : ℚ_[p])) <
      ε'
h : ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε

Tactic:
use N
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : (↑ε' : ℝ) < ε
hε'0 : 0 < ε'
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        (HSub.hSub (α := ℚ_[p]) (mk (nthHomSeq f_compat r)) (↑((↑(nthHomSeq f_compat r) : ℕ → ℚ) i) : ℚ_[p])) <
      ε'
n : ℕ
hn : n ≥ N
apply : ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < (↑ε' : ℝ)
⊢ ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε

Tactic:
apply _root_.lt_trans _ hε'

Premises used: lt_trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : (↑ε' : ℝ) < ε
hε'0 : 0 < ε'
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        (HSub.hSub (α := ℚ_[p]) (mk (nthHomSeq f_compat r)) (↑((↑(nthHomSeq f_compat r) : ℕ → ℚ) i) : ℚ_[p])) <
      ε'
n : ℕ
hn : n ≥ N
norm_cast :
  (padicNormE : (a : ℚ_[p]) → ℚ) (↑(HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])) : ℚ_[p]) <
    ε'
⊢ LT.lt (α := ℝ)
    (↑((padicNormE : (a : ℚ_[p]) → ℚ)
          (↑(HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])) : ℚ_[p])) :
      ℝ)
    (↑ε' : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : (↑ε' : ℝ) < ε
hε'0 : 0 < ε'
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        (HSub.hSub (α := ℚ_[p]) (mk (nthHomSeq f_compat r)) (↑((↑(nthHomSeq f_compat r) : ℕ → ℚ) i) : ℚ_[p])) <
      ε'
n : ℕ
hn : n ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (↑(HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])) : ℚ_[p]) <
    ε'

Tactic:
hN _ hn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
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), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε' : (↑ε' : ℝ) < ε
hε'0 : 0 < ε'
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ)
        (HSub.hSub (α := ℚ_[p]) (mk (nthHomSeq f_compat r)) (↑((↑(nthHomSeq f_compat r) : ℕ → ℚ) i) : ℚ_[p])) <
      ε'
n : ℕ
hn : n ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (↑(HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])) : ℚ_[p]) <
    ε'

Tactic:
exact hN _ hn