awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])
x : ℤ_[p]
h : ¬x - (↑(x.appr n) : ℤ_[p]) = 0
c : ℤ_[p]
hc : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * c
hc' : c ≠ 0
hc0 : c.valuation ≠ 0
⊢ (↑p : ℤ_[p]) ∣ (↑(unitCoeff hc') : ℤ_[p]) * HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) c.valuation

Tactic:
exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _

Premises used: Dvd.dvd.mul_left, Nat.cast, dvd_pow_self
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
zero : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 0 ∣ x - (↑(x.appr 0) : ℤ_[p])
succ :
  ∀ (n : ℕ) (ih : ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])) (x : ℤ_[p]),
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) (n + 1) ∣ x - (↑(x.appr (n + 1)) : ℤ_[p])
⊢ ∀ (x : ℤ_[p]), HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n ∣ x - (↑(x.appr n) : ℤ_[p])

Tactic:
induction n with
  | zero => simp only [_root_.pow_zero, isUnit_one, IsUnit.dvd, forall_const]
  | succ n ih =>
    intro x
    dsimp only [appr]
    split_ifs with h
    · rw [h]
      apply dvd_zero
    push_cast
    rw [sub_add_eq_sub_sub]
    obtain ⟨c, hc⟩ := ih x
    simp only [map_natCast, ZMod.natCast_self, map_pow, map_mul, ZMod.natCast_val]
    have hc' : c ≠ 0 := by
      rintro rfl
      simp only [mul_zero] at hc
      contradiction
    conv_rhs =>
      congr
      simp only [hc]
    rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]]
    rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub]
    apply mul_dvd_mul_left
    obtain hc0 | hc0 := eq_or_ne c.valuation 0
    · simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero]
      rw [mul_comm, unitCoeff_spec h] at hc
      suffices c = unitCoeff h by
        rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p]
        apply toZMod_spec
      lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0]
      rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc]
      exact irreducible_p
    · simp only [Int.natAbs_natCast, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero]
      rw [unitCoeff_spec hc']
      exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _

Premises used: dvd_zero, PadicInt.irreducible_p, mul_sub, ZMod.natCast_self, sub_zero, add_sub_cancel_left, pow_succ, Int.natAbs_zero, mul_dvd_mul_left, ZMod.natCast_val, map_pow, pow_zero, MulZeroClass.mul_zero, IsUnit.dvd, Nat.cast_add, ZMod.cast_zero, map_mul, sub_add_eq_sub_sub, map_natCast, isUnit_one, mul_comm, Nat.zero, forall_const, PadicInt.appr, Nat.cast_zero, Int.natAbs_natCast, mul_one, Nat.succ
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
⊢ Eq (α := ℤ_[p] →+* ZMod p) toZMod (RingHom.comp (RingEquiv.toRingHom residueField) (residue ℤ_[p]))

Tactic:
rfl

Premises used: PadicInt.toZModHom, Quotient.liftOn', AddCon.liftOn, PadicInt.toZMod, rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x_1 : ℤ_[p]
rw :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (x_1 - (↑((fun (x : ℤ_[p]) ↦ x.appr n) x_1) : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])})
    (x_1 - (↑((fun (x : ℤ_[p]) ↦ x.appr n) x_1) : ℤ_[p]))

Tactic:
rw [Nat.cast_pow]

Premises used: Nat.cast_pow
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x_1 : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (x_1 - (↑((fun (x : ℤ_[p]) ↦ x.appr n) x_1) : ℤ_[p]))

Tactic:
appr_spec n _

Premises used: PadicInt.appr_spec, Set.Mem, setOf
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x : ℤ_[p]
n : ℕ
x_1 : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n})
    (x_1 - (↑((fun (x : ℤ_[p]) ↦ x.appr n) x_1) : ℤ_[p]))

Tactic:
exact appr_spec n _

Premises used: PadicInt.appr_spec
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑b : ℤ_[p]))
ha₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑a : ℤ_[p]))
hb₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑b : ℤ_[p]))
⊢ Eq (α := ZMod (p ^ n)) (↑a : ZMod (p ^ n)) (↑b : ZMod (p ^ n))

Tactic:
apply zmod_congr_of_sub_mem_span n x a b

Premises used: PadicInt.zmod_congr_of_sub_mem_span
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑b : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑a : ℤ_[p]))

Tactic:
simpa using ha
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x_1 : ℤ_[p]
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑a : ℤ_[p]))
hb : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑(p ^ n) : ℤ_[p])}) (x - (↑b : ℤ_[p]))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑b : ℤ_[p]))

Tactic:
simpa using hb
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
h₁ :
  Eq (α := Ideal ℤ_[p])
    (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n)))
    (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m))
⊢ Eq (α := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n)) (toZModPow m)

Tactic:
apply ZMod.ringHom_eq_of_ker_eq

Premises used: ZMod.ringHom_eq_of_ker_eq
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
h₁ :
  ∀ (x : ℤ_[p]),
    Membership.mem (γ := Ideal ℤ_[p])
        (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n))) x ↔
      Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m)) x
⊢ Eq (α := Ideal ℤ_[p])
    (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n)))
    (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m))

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ :
  Eq (α := ZMod (p ^ m))
      ((RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
      (0 : ZMod (p ^ m)) ↔
    Eq (α := ZMod (p ^ m)) ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m)) (0 : ZMod (p ^ m))
⊢ Membership.mem (γ := Ideal ℤ_[p])
      (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n))) x ↔
    Membership.mem (γ := Ideal ℤ_[p]) (RingHom.ker (F := ℤ_[p] →+* ZMod (p ^ m)) (toZModPow m)) x

Tactic:
rw [RingHom.mem_ker, RingHom.mem_ker]

Premises used: RingHom.mem_ker
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ :
  Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x)) 0 ↔
    Eq (α := ZMod (p ^ m)) ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m)) (0 : ZMod (p ^ m))
⊢ Eq (α := ZMod (p ^ m))
      ((RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
      (0 : ZMod (p ^ m)) ↔
    Eq (α := ZMod (p ^ m)) ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m)) (0 : ZMod (p ^ m))

Tactic:
simp only [Function.comp_apply, ZMod.castHom_apply, RingHom.coe_comp]

Premises used: ZMod.castHom_apply, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ :
  Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) (↑(x.appr n) : ZMod (p ^ n))) 0 ↔
    Eq (α := ZMod (p ^ m)) (↑(x.appr m) : ZMod (p ^ m)) 0
⊢ Eq (α := ZMod (p ^ m))
      (ZMod.cast (n := p ^ n)
        (({ toFun := fun (x : ℤ_[p]) ↦ (↑(x.appr n) : ZMod (p ^ n)), map_one' := ⋯, map_mul' := ⋯ } :
            (a : ℤ_[p]) → ZMod (p ^ n))
          x))
      0 ↔
    Eq (α := ZMod (p ^ m))
      (({ toFun := fun (x : ℤ_[p]) ↦ (↑(x.appr m) : ZMod (p ^ m)), map_one' := ⋯, map_mul' := ⋯ } :
            (a : ℤ_[p]) → ZMod (p ^ m))
          x :
        ZMod (p ^ m))
      (0 : ZMod (p ^ m))

Tactic:
dsimp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr n) : ℤ_[p]))
h₂ :
  Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]))
⊢ Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) (↑(x.appr n) : ZMod (p ^ n))) 0 ↔
    Eq (α := ZMod (p ^ m)) (↑(x.appr m) : ZMod (p ^ m)) 0

Tactic:
rw [ZMod.cast_natCast (pow_dvd_pow p h),
    zmod_congr_of_sub_mem_span m (x.appr n) (x.appr n) (x.appr m)]

Premises used: PadicInt.zmod_congr_of_sub_mem_span, pow_dvd_pow, Nat.cast, ZMod.cast_natCast, PadicInt.appr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m}) 0
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr n) : ℤ_[p]))

Tactic:
rw [sub_self]

Premises used: sub_self
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m}) 0

Tactic:
apply Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m})
    (HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]))

Tactic:
rw [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
h₁ :
  ∀ (c : ℕ) (hc : x.appr n - x.appr m = p ^ m * c),
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])

Tactic:
rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩

Premises used: PadicInt.dvd_appr_sub_appr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
h₁ :
  HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])

Tactic:
use c
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
h₁ : (↑(x.appr n - x.appr m) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
h₂ : (↑(p ^ m * c) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
h₃ : HMul.hMul (α := ℤ_[p]) (↑(p ^ m) : ℤ_[p]) (↑c : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
h₄ h₅ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
⊢ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])

Tactic:
rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]

Premises used: Nat.cast_sub, Nat.cast_mul, PadicInt.appr_mono, Nat.cast_pow
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
rw :
  Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x) : ZMod (p ^ m))
    ((RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
⊢ Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x) : ZMod (p ^ m))
    ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))

Tactic:
rw [← zmod_cast_comp_toZModPow _ _ h]

Premises used: PadicInt.zmod_cast_comp_toZModPow
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ Eq (α := ZMod (p ^ m)) (ZMod.cast (n := p ^ n) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x) : ZMod (p ^ m))
    ((RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
rw : ∀ ε > 0, ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Nat.cast)) x

Tactic:
rw [Metric.mem_closure_range_iff]

Premises used: Metric.mem_closure_range_iff
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε), ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε
⊢ ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε

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

Premises used: PadicInt.exists_pow_neg_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
h : dist x (↑(x.appr n) : ℤ_[p]) < ε
⊢ ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε

Tactic:
use x.appr n

Premises used: PadicInt.appr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
h : ‖x - (↑(x.appr n) : ℤ_[p])‖ < ε
⊢ dist x (↑(x.appr n) : ℤ_[p]) < ε

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
apply : ‖x - (↑(x.appr n) : ℤ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖x - (↑(x.appr n) : ℤ_[p])‖ < ε

Tactic:
apply lt_of_le_of_lt _ hn

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
rw : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑(x.appr n) : ℤ_[p]))
⊢ ‖x - (↑(x.appr n) : ℤ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
rw [norm_le_pow_iff_mem_span_pow]

Premises used: PadicInt.norm_le_pow_iff_mem_span_pow
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑(x.appr n) : ℤ_[p]))

Tactic:
apply appr_spec

Premises used: PadicInt.appr_spec
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) x

Tactic:
DenseRange.induction_on denseRange_natCast x ?_ ?_

Premises used: PadicInt.denseRange_natCast, DenseRange.induction_on
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
refine_1 : IsClosed (X := ℤ_[p]) {b : ℤ_[p] | Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) b}
refine_2 : ∀ (a : ℕ), Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) (↑a : ℤ_[p])
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) x

Tactic:
refine DenseRange.induction_on denseRange_natCast x ?_ ?_
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed (X := ℤ_[p]) {b : ℤ_[p] | Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) b}

Tactic:
isClosed_closure

Premises used: Set.Mem, setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ IsClosed (X := ℤ_[p]) {b : ℤ_[p] | Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) b}

Tactic:
exact isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
refine_2 : Membership.mem (γ := Set ℤ_[p]) (Set.range Int.cast) (↑a : ℤ_[p])
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) (↑a : ℤ_[p])

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ Membership.mem (γ := Set ℤ_[p]) (Set.range Int.cast) (↑a : ℤ_[p])

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self, Set.Mem
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ Membership.mem (γ := Set ℤ_[p]) (Set.range Int.cast) (↑a : ℤ_[p])

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
⊢ nthHom f 0 = 0

Tactic:
simp +unfoldPartialApp [nthHom, Pi.zero_def]

Premises used: Pi.zero_def, 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
i j : ℕ
h : i ≤ j
⊢ RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ i))) (f j) = f i

Tactic:
specialize f_compat i j 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)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ i))) (f j) = f i
rw : HSub.hSub (α := ZMod (p ^ i)) (↑(nthHom f r j) : ZMod (p ^ i)) (↑(nthHom f r i) : ZMod (p ^ i)) = 0
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ nthHom f r j - nthHom f r i

Tactic:
rw [← Int.natCast_pow, ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub]

Premises used: Int.cast_sub, Int.natCast_pow, 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)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ i))) (f j) = f i
dsimp :
  HSub.hSub (α := ZMod (p ^ i)) (↑(↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ) : ZMod (p ^ i))
      (↑(↑(ZMod.val (n := p ^ i) ((f i : (a : R) → ZMod (p ^ i)) r)) : ℤ) : ZMod (p ^ i)) =
    0
⊢ HSub.hSub (α := ZMod (p ^ i)) (↑(nthHom f r j) : ZMod (p ^ i)) (↑(nthHom f r i) : ZMod (p ^ i)) = 0

Tactic:
dsimp [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)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ i))) (f j) = f i
rw :
  HSub.hSub (α := ZMod (p ^ i)) (↑(↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ) : ZMod (p ^ i))
      (↑(↑(ZMod.val (n := p ^ i)
                ((ZMod.castHom ⋯ (ZMod (p ^ i)) : (a : ZMod (p ^ j)) → ZMod (p ^ i))
                  ((f j : (a : R) → ZMod (p ^ j)) r))) :
            ℤ) :
        ZMod (p ^ i)) =
    0
⊢ HSub.hSub (α := ZMod (p ^ i)) (↑(↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ) : ZMod (p ^ i))
      (↑(↑(ZMod.val (n := p ^ i) ((f i : (a : R) → ZMod (p ^ i)) r)) : ℤ) : ZMod (p ^ i)) =
    0

Tactic:
rw [← f_compat, RingHom.comp_apply]

Premises used: RingHom.comp_apply
-- 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)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ i))) (f j) = f i
⊢ HSub.hSub (α := ZMod (p ^ i)) (↑(↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ) : ZMod (p ^ i))
      (↑(↑(ZMod.val (n := p ^ i)
                ((ZMod.castHom ⋯ (ZMod (p ^ i)) : (a : ZMod (p ^ j)) → ZMod (p ^ i))
                  ((f j : (a : R) → ZMod (p ^ j)) r))) :
            ℤ) :
        ZMod (p ^ i)) =
    0

Tactic:
simp only [ZMod.cast_id, ZMod.castHom_apply, sub_self, ZMod.natCast_val, ZMod.intCast_cast]

Premises used: sub_self, ZMod.castHom_apply, ZMod.natCast_val, ZMod.cast_id, 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 : R
ε : ℚ
hε : ε > 0
⊢ ∃ (k : ℕ), HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε

Tactic:
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 : R
ε : ℚ
hε : ε > 0
obtain :
  ∀ (k : ℕ) (hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε),
    ∃ (i : ℕ),
      ∀ j ≥ i,
        padicNorm p
            (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
              ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) i)) <
          ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      padicNorm p
          (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
            ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) i)) <
        ε

Tactic:
obtain ⟨k, hk⟩ : ∃ k : ℕ, (p : ℚ) ^ (-((k : ℕ) : ℤ)) < ε := exists_pow_neg_lt_rat p hε

Premises used: Nat.cast, 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 : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
h :
  ∀ j ≥ k,
    padicNorm p
        (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
          ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) <
      ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      padicNorm p
          (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
            ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) i)) <
        ε

Tactic:
use k