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
simp : Eq (α := ℤ_[p]) (ofIntSeq 0 ⋯) 0
⊢ Eq (α := ℤ_[p]) (limNthHom f_compat 0) 0

Tactic:
simp [limNthHom]

Premises used: PadicInt.limNthHom
-- 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
⊢ Eq (α := ℤ_[p]) (ofIntSeq 0 ⋯) 0

Tactic:
rfl
-- 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
⊢ Eq (α := ℤ_[p]) (limNthHom f_compat 1) 1

Tactic:
Subtype.ext <| Quot.sound <| nthHomSeq_one f_compat

Premises used: PadicInt, Quot.sound, PadicInt.nthHomSeq_one, Subtype.ext
-- 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
⊢ limNthHom f_compat (r + s) = HAdd.hAdd (α := ℤ_[p]) (limNthHom f_compat r) (limNthHom f_compat s)

Tactic:
Subtype.ext <| Quot.sound <| nthHomSeq_add f_compat _ _

Premises used: PadicInt, Quot.sound, PadicInt.nthHomSeq_add, Subtype.ext
-- 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
⊢ limNthHom f_compat (r * s) = HMul.hMul (α := ℤ_[p]) (limNthHom f_compat r) (limNthHom f_compat s)

Tactic:
Subtype.ext <| Quot.sound <| nthHomSeq_mul f_compat _ _

Premises used: PadicInt, Quot.sound, PadicInt.nthHomSeq_mul, Subtype.ext
-- 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
n : ℕ
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]))
⊢ 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) _)

Premises used: Nat.cast, PadicInt.limNthHom_spec, zpow_pos, Neg.neg
-- 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
n k : ℕ
hk :
  ∀ n_1 ≥ k,
    ‖HSub.hSub (α := ℤ_[p]) (limNthHom f_compat r) (↑(nthHom f r n_1) : ℤ_[p])‖ <
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖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 _ _))
-- 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
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]) (limNthHom f_compat r) (↑(nthHom f r (max n k)) : ℤ_[p]))

Tactic:
rw [norm_le_pow_iff_mem_span_pow] at this

Premises used: PadicInt.norm_le_pow_iff_mem_span_pow
-- 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
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]))
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]))
⊢ 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]))

Tactic:
rw [sub_eq_sub_add_sub (limNthHom f_compat r) _ ↑(nthHom f r (max n k))]

Premises used: Int.cast, PadicInt.limNthHom, Max.max, sub_eq_sub_add_sub, 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
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]))
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]))
⊢ 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:
apply Ideal.add_mem _ _ this

Premises used: Ideal.add_mem
-- 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
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]))
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])
⊢ 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:
rw [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- 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
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]))
⊢ Dvd.dvd (α := ℤ_[p]) ((Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (HPow.hPow (α := ℤ) (↑p : ℤ) n) : ℤ_[p])
    ((Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (nthHom f r (max n k) - nthHom f r n) : ℤ_[p])

Tactic:
map_dvd (Int.castRingHom ℤ_[p]) (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))

Premises used: PadicInt, PadicInt.pow_dvd_nthHom_sub, map_dvd, Max.max, Int.castRingHom, le_max_left
-- 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
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)
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)
⊢ 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:
convert!
    map_dvd (Int.castRingHom ℤ_[p]) (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))

Premises used: PadicInt, PadicInt.pow_dvd_nthHom_sub, map_dvd, Max.max, Int.castRingHom, le_max_left
-- 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
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 = (Int.castRingHom ℤ_[p] : (a : ℤ) → ℤ_[p]) (HPow.hPow (α := ℤ) (↑p : ℤ) n)

Tactic:
simp
-- 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
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]))
⊢ 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:
simp [nthHom]

Premises used: 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
n : ℕ
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))
⊢ RingHom.comp (β := ℤ_[p]) (toZModPow n) (lift f_compat) = f n

Tactic:
ext r
-- 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
n : ℕ
r : R
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]))
⊢ 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:
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]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, ZMod.natCast_zmod_val, PadicInt.ker_toZModPow, map_natCast, RingHom.comp_apply, DFunLike.coe, PadicInt.toZModPow
-- 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
n : ℕ
r : R
⊢ 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:
apply lift_sub_val_mem_span

Premises used: PadicInt.lift_sub_val_mem_span
-- 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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
a :
  ∀ (r : R),
    Eq (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p])
⊢ lift f_compat = g

Tactic:
ext1 r
-- 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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
a :
  ∀ ε > 0,
    dist (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p]) ≤
      ε
⊢ Eq (α := ℤ_[p]) (((lift f_compat : R →+* ℤ_[p]) : (a : R) → ℤ_[p]) r : ℤ_[p]) ((g : (a : R) → ℤ_[p]) r : ℤ_[p])

Tactic:
apply eq_of_forall_dist_le

Premises used: eq_of_forall_dist_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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
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]) ≤
      ε
⊢ 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ε

Premises used: PadicInt.exists_pow_neg_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
g : R →+* ℤ_[p]
hg : ∀ (n : ℕ), RingHom.comp (toZModPow n) g = f n
r : R
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
apply :
  dist (α := ℤ_[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]) ≤ ε

Tactic:
apply le_trans _ (le_of_lt hn)

Premises used: le_of_lt, le_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
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
rw₉ rw₁₀ : Eq (α := ZMod (p ^ n)) 0 0
⊢ dist (α := ℤ_[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]

Premises used: dist_eq_norm, map_sub, sub_self, RingHom.mem_ker, PadicInt.norm_le_pow_iff_mem_span_pow, PadicInt.ker_toZModPow, PadicInt.lift_spec, RingHom.comp_apply
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
change : Eq (α := ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p]) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p])
⊢ (lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) z = z

Tactic:
change _ = RingHom.id _ z

Premises used: RingHom.id, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
rw : ∀ (n : ℕ), Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow n) (RingHom.id ℤ_[p])) (toZModPow n)
⊢ Eq (α := ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p]) ((RingHom.id ℤ_[p] : (a : ℤ_[p]) → ℤ_[p]) z : ℤ_[p])

Tactic:
rw [lift_unique zmod_cast_comp_toZModPow (RingHom.id ℤ_[p])]

Premises used: PadicInt, PadicInt.zmod_cast_comp_toZModPow, PadicInt.lift_unique, RingHom.id
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
z : ℤ_[p]
n : ℕ
rw rw₁ : Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (toZModPow n) (toZModPow n)
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ n)) (RingHom.comp (toZModPow n) (RingHom.id ℤ_[p])) (toZModPow n)

Tactic:
rw [RingHom.comp_id]

Premises used: RingHom.comp_id
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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
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))
⊢ (∀ (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
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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))
mp : Eq (α := ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) y : ℤ_[p])
⊢ x = y

Tactic:
rw [← lift_self x, ← lift_self y]

Premises used: PadicInt.lift_self
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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))
⊢ Eq (α := ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) x : ℤ_[p]) ((lift ⋯ : (a : ℤ_[p]) → ℤ_[p]) y : ℤ_[p])

Tactic:
simp +unfoldPartialApp [lift, limNthHom, nthHom, h]

Premises used: PadicInt.lift, PadicInt.limNthHom, PadicInt.nthHom
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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'
mpr : g = g' → ∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g'
⊢ (∀ (n : ℕ), RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g') ↔ g = g'

Tactic:
constructor