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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
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 : ℤ))
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw₁ : 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])
    ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw₂ : Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
  (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
    ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw₃ : Eq (α := ZMod (p ^ n))
  ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
      (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
        ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
    ZMod (p ^ n))
  (0 : ZMod (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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₃ :
  Eq (α := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
          ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
      ZMod (p ^ n))
    (0 : ZMod (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 (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r) : ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
  0
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₃ :
  Eq (α := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
          ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
      ZMod (p ^ n))
    (0 : ZMod (p ^ n))
rw₄ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r) : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
⊢ 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 (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
    ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
  0
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₃ :
  Eq (α := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
          ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
      ZMod (p ^ n))
    (0 : ZMod (p ^ n))
rw₄ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r) : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₅ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
⊢ 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 (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
    ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
    ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
  0
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₃ :
  Eq (α := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
          ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
      ZMod (p ^ n))
    (0 : ZMod (p ^ n))
rw₄ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r) : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₅ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₆ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
    0
⊢ 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 (α := ZMod (p ^ n)) (β := ZMod (p ^ n)) ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
    ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
  0
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₃ :
  Eq (α := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
          ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
      ZMod (p ^ n))
    (0 : ZMod (p ^ n))
rw₄ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r) : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₅ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₆ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
    0
rw₇ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n)) ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
    0
⊢ 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 (α := ZMod (p ^ n)) (β := ZMod (p ^ n)) ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
    ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
  0
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]
-- 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 : ℤ)) < ε
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 : ℤ))
rw₁ :
  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])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n))
    (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
      ((g : (a : R) → ℤ_[p]) r : ℤ_[p]))
rw₃ :
  Eq (α := ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n))
        (HSub.hSub (α := ℤ_[p]) (β := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p])
          ((g : (a : R) → ℤ_[p]) r : ℤ_[p])) :
      ZMod (p ^ n))
    (0 : ZMod (p ^ n))
rw₄ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r) : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₅ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) r) : ZMod (p ^ n)) =
    0
rw₆ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n))
      ((RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
    0
rw₇ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n)) ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
    0
rw₈ :
  HSub.hSub (α := ZMod (p ^ n)) (β := ZMod (p ^ n)) ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n))
      ((f n : (a : R) → ZMod (p ^ n)) r : ZMod (p ^ n)) =
    0
⊢ dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw₉ : Eq (α := ZMod (p ^ n)) 0 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ (lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) z = z
have change : Eq (α := ℤ_[p]) ((lift sorry : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p]) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p])
Tactic: change _ = RingHom.id _ z
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ Eq (α := ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p]) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p])
have rw : ∀ (n : ℕ), Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow n) (RingHom.id ℤ_[p])) (toZModPow n)
Tactic: rw [lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
n : ℕ
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow n) (RingHom.id ℤ_[p])) (toZModPow n)
have rw : Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n) (toZModPow n)
Tactic: rw [RingHom.comp_id]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ),
      Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
        ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) y : ZMod (p ^ n))) ↔
    x = y
have mp : (∀ (n : ℕ),
    Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) y : ZMod (p ^ n))) →
  x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
mp :
  (∀ (n : ℕ),
      Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
        ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) y : ZMod (p ^ n))) →
    x = y
⊢ (∀ (n : ℕ),
      Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
        ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) y : ZMod (p ^ n))) ↔
    x = y
have mpr : x = y →
  ∀ (n : ℕ),
    Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) y : ZMod (p ^ n))
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h :
  ∀ (n : ℕ),
    Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
      ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) y : ZMod (p ^ n))
⊢ x = y
have mp : Eq (α := ℤ_[p]) ((lift sorry : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p]) ((lift sorry : (a : ℤ_[p]) → ℤ_[p]) y : ℤ_[p])
Tactic: rw [← lift_self x, ← lift_self y]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst : NonAssocSemiring R
g g' : R →+* ℤ_[p]
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') ↔ g = g'
have mp : (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') → g = g'
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst : NonAssocSemiring R
g g' : R →+* ℤ_[p]
mp : (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') → g = g'
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') ↔ g = g'
have mpr : g = g' → ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
⊢ g = g'
have mp : ∀ (x : R), Eq (α := ℤ_[p]) ((g : (a : R) → ℤ_[p]) x : ℤ_[p]) ((g' : (a : R) → ℤ_[p]) x : ℤ_[p])
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst : NonAssocSemiring R
g g' : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
x : R
⊢ Eq (α := ℤ_[p]) ((g : (a : R) → ℤ_[p]) x : ℤ_[p]) ((g' : (a : R) → ℤ_[p]) x : ℤ_[p])
have mp : ∀ (n : ℕ),
  Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g : (a : R) → ℤ_[p]) x) : ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) ((g' : (a : R) → ℤ_[p]) x) : ZMod (p ^ n))
Tactic: apply ext_of_toZModPow.mp