awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ padicNorm p ((↑(nthHom f (r * s) j) : ℚ) - HMul.hMul (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have rw : Eq (α := ZMod (p ^ n)) (↑(nthHom f (r * s) j - nthHom f r j * nthHom f s j) : ZMod (p ^ n)) 0
Tactic: rw [← Int.cast_mul, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
    ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ 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
have 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
Tactic: simp only [ZMod.natCast_val, map_mul, Int.cast_sub, ZMod.intCast_cast, Int.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (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
have 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
Tactic: rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (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
have rw₁ : Eq (α := ZMod (p ^ n)) 0 0
Tactic: rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
have obtain : ∀ (ε' : ℚ) (hε'0 : LT.lt (α := ℝ) 0 (↑ε' : ℝ)) (hε' : (↑ε' : ℝ) < ε),
  ∃ (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ε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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ε' : (↑ε' : ℝ) < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
have hε'0₁ : 0 < ε'
Tactic: norm_cast at hε'0
Cleared hypotheses: hε'0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
have 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])‖ < ε
Tactic: obtain ⟨N, hN⟩ := padicNormE.defn (nthHomSeq f_compat r) hε'0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 : ℕ), ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
have h : ∀ n ≥ N, ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
Tactic: use N
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < ε
have apply : ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])‖ < (↑ε' : ℝ)
Tactic: apply _root_.lt_trans _ hε'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ LT.lt (α := ℝ)
    (↑((padicNormE : (a : ℚ_[p]) → ℚ)
          (↑(HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])) : ℚ_[p])) :
      ℝ)
    (↑ε' : ℝ)
have norm_cast : (padicNormE : (a : ℚ_[p]) → ℚ) (↑(HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n) : ℤ_[p])) : ℚ_[p]) < ε'
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ Eq (α := ℤ_[p]) (limNthHom f_compat 0) 0
have simp : Eq (α := ℤ_[p]) (ofIntSeq 0 sorry) 0
Tactic: simp [limNthHom]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n : ℕ
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) : ℤ_[p]))
have obtain : ∀ (k : ℕ)
  (hk :
    ∀ n_1 ≥ k,
      ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
        HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))),
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) : ℤ_[p]))
Tactic: obtain ⟨k, hk⟩ :=
    limNthHom_spec f_compat r _
      (show (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) from zpow_pos (mod_cast hp_prime.1.pos) _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) : ℤ_[p]))
have this : ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p])‖ ≤
  HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
Tactic: have := le_of_lt (hk (max n k) (le_max_right _ _))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this :
  ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p])‖ ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) : ℤ_[p]))
have this₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
  (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
Tactic: rw [norm_le_pow_iff_mem_span_pow] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r)
      (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]))
have rw : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
  (HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
      (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) +
    HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
Tactic: rw [sub_eq_sub_add_sub (limNthHom f_compat r) _ ↑(nthHom f r (max n k))]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
        (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) +
      HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
have apply : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
  (HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
    (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]))
Tactic: apply Ideal.add_mem _ _ this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
      (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]))
have rw : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣
  HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
    (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p])
Tactic: rw [Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣
    HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
      (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p])
have h : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n = (Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (HPow.hPow (α := ℤ) (↑p : ℤ) n)
Tactic: convert!
    map_dvd (Int.castRingHom ℤ_[p]) (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
this :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))
h : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n = (Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (HPow.hPow (α := ℤ) (↑p : ℤ) n)
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣
    HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
      (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p])
have h₁ : HSub.hSub (α := ℤ_[p]) (↑(nthHom f r (max n k)) : ℤ_[p])
    (↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) =
  (Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (nthHom f r (max n k) - nthHom f r n)
Tactic: convert!
    map_dvd (Int.castRingHom ℤ_[p]) (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n : ℕ
⊢ RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) = f n
have a : ∀ (r : R),
  Eq (α := ZMod (p ^ n))
    ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
    ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
Tactic: ext r
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
n : ℕ
r : R
⊢ Eq (α := ZMod (p ^ n))
    ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
    ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
have a : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
  (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
    ((↑(ZMod.val (n := p ^ n) ((f n : (a : R) → ZMod (p ^ n)) r)) : ℤ_[p]) : ℤ_[p]))
Tactic: rw [RingHom.comp_apply, ← ZMod.natCast_zmod_val (f n r), ← map_natCast <| toZModPow n, ←
    sub_eq_zero, ← map_sub, ← RingHom.mem_ker, ker_toZModPow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
⊢ lift f_compat = g
have a : ∀ (r : R),
  Eq (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p])
Tactic: ext1 r
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
⊢ Eq (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p])
have a : ∀ ε > 0,
  dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤ ε
Tactic: apply eq_of_forall_dist_le
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤ ε
have a : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε),
  dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤ ε
Tactic: obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤ ε
have apply : dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
  HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
Tactic: apply le_trans _ (le_of_lt hn)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw : ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p])‖ ≤
  HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
Tactic: rw [dist_eq_norm, norm_le_pow_iff_mem_span_pow, ← ker_toZModPow, RingHom.mem_ker,
    map_sub, ← RingHom.comp_apply, ← RingHom.comp_apply, lift_spec, hg, sub_self]