awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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'
mp : ∀ (x : R), Eq (α := ℤ_[p]) ((g : (a : R) → ℤ_[p]) x : ℤ_[p]) ((g' : (a : R) → ℤ_[p]) x : ℤ_[p])
⊢ g = g'

Tactic:
ext x : 1
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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
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))
⊢ Eq (α := ℤ_[p]) ((g : (a : R) → ℤ_[p]) x : ℤ_[p]) ((g' : (a : R) → ℤ_[p]) x : ℤ_[p])

Tactic:
apply ext_of_toZModPow.mp

Premises used: PadicInt.ext_of_toZModPow, Iff.mp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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
n : ℕ
mp :
  Eq (α := ZMod (p ^ n)) ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((RingHom.comp (toZModPow n) g' : (a : R) → ZMod (p ^ n)) x : ZMod (p ^ 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:
change (toZModPow n).comp g x = (toZModPow n).comp g' x

Premises used: RingHom.comp, DFunLike.coe, PadicInt.toZModPow
-- Module: Mathlib.NumberTheory.Padics.RingHoms
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
n : ℕ
mp mp₁ :
  Eq (α := ZMod (p ^ n)) ((RingHom.comp (toZModPow n) g' : (a : R) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((RingHom.comp (toZModPow n) g' : (a : R) → ZMod (p ^ n)) x : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((RingHom.comp (toZModPow n) g : (a : R) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((RingHom.comp (toZModPow n) g' : (a : R) → ZMod (p ^ n)) x : ZMod (p ^ n))

Tactic:
rw [hg n]
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
R : Type u_1
inst : NonAssocSemiring R
g : R →+* ℤ_[p]
n : ℕ
⊢ RingHom.comp (toZModPow n) g = RingHom.comp (toZModPow n) g

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
obtain :
  ∀ (k : ℕ) (hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε),
    ∃ (i : ℕ),
      ∀ j ≥ i,
        padicNorm p (HSub.hSub (α := ℚ) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) j) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) i)) <
          ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      padicNorm p (HSub.hSub (α := ℚ) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) j) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) i)) < ε

Tactic:
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt_rat p hε

Premises used: PadicInt.exists_pow_neg_lt_rat
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
simp : ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (↑(f j - f i) : ℚ) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      padicNorm p (HSub.hSub (α := ℚ) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) j) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) i)) < ε

Tactic:
simp only [← Int.cast_sub]

Premises used: Int.cast_sub
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (↑(f j - f i) : ℚ) < ε

Tactic:
⟨k, fun i hik ↦ (padicNorm.dvd_iff_norm_le.mp ?_).trans_lt hk⟩

Premises used: padicNorm.dvd_iff_norm_le, Exists.intro, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
refine : ∀ (i : ℕ) (hik : i ≥ k), (↑(p ^ k) : ℤ) ∣ f i - f k
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (↑(f j - f i) : ℚ) < ε

Tactic:
refine ⟨k, fun i hik ↦ (padicNorm.dvd_iff_norm_le.mp ?_).trans_lt hk⟩
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
i : ℕ
hik : i ≥ k
obtain : ∀ (i : ℕ) (hik : k + i ≥ k), (↑(p ^ k) : ℤ) ∣ f (k + i) - f k
⊢ (↑(p ^ k) : ℤ) ∣ f i - f k

Tactic:
obtain ⟨i, rfl⟩ := exists_add_of_le hik

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
⊢ (↑(p ^ k) : ℤ) ∣ f (k + 0) - f k

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
n : ℕ
IH : (↑(p ^ k) : ℤ) ∣ f (k + n) - f k
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) (k + n) = (↑(p ^ k) : ℤ) * HPow.hPow (α := ℤ) (↑p : ℤ) n

Tactic:
simp [pow_add]

Premises used: pow_add
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
n : ℕ
IH : (↑(p ^ k) : ℤ) ∣ f (k + n) - f k
⊢ (↑(p ^ k) : ℤ) ∣ HPow.hPow (α := ℤ) (↑p : ℤ) (k + n)

Tactic:
have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
n : ℕ
IH : (↑(p ^ k) : ℤ) ∣ f (k + n) - f k
this : (↑(p ^ k) : ℤ) ∣ HPow.hPow (α := ℤ) (↑p : ℤ) (k + n)
⊢ (↑(p ^ k) : ℤ) ∣ f (k + (n + 1)) - f k

Tactic:
simpa using (this.trans (hi _)).add IH

Premises used: Dvd.dvd.add, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
i : ℕ
zero : (↑(p ^ k) : ℤ) ∣ f (k + 0) - f k
succ : ∀ (n : ℕ) (IH : (↑(p ^ k) : ℤ) ∣ f (k + n) - f k), (↑(p ^ k) : ℤ) ∣ f (k + (n + 1)) - f k
⊢ (↑(p ^ k) : ℤ) ∣ f (k + i) - f k

Tactic:
induction i with
  | zero => simp
  | succ n IH =>
    have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
    simpa using (this.trans (hi _)).add IH

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
set :
  let x : ℤ_[p] := ofIntSeq f ⋯;
  Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) (ofIntSeq f ⋯) : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))

Tactic:
set x := PadicInt.ofIntSeq _ (isCauSeq_padicNorm_of_pow_dvd_sub f p hi)

Premises used: PadicInt.ofIntSeq, PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
⊢ (↑x : ℚ_[p]) = mk s

Tactic:
have hs : x = Padic.mk s := rfl
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
obtain :
  ∀ (e : ℤ_[p]) (he : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e),
    Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
      ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))

Tactic:
obtain ⟨e, he⟩ := Ideal.mem_span_singleton.mp (PadicInt.appr_spec n x)

Premises used: PadicInt.appr_spec, Iff.mp, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x - (↑(x.appr n) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e
⊢ x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])

Tactic:
rw [sub_eq_iff_eq_add] at he

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
simp : 0 < HPow.hPow (α := ℚ) (↑p : ℚ) n
⊢ 0 < HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
simp only [zpow_neg, zpow_natCast, inv_pos]

Premises used: zpow_natCast, inv_pos, zpow_neg
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
⊢ 0 < HPow.hPow (α := ℚ) (↑p : ℚ) n

Tactic:
exact_mod_cast Nat.pos_of_neZero _

Premises used: Nat.pos_of_neZero
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
obtain :
  ∀ (N : ℕ)
    (hN :
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk s) (↑((↑s : ℕ → ℚ) i) : ℚ_[p])) <
          HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))),
    Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
      ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))

Tactic:
obtain ⟨N, hN⟩ := padicNormE.defn s (ε := p ^ (-n : ℤ))
    (by simp only [zpow_neg, zpow_natCast, inv_pos]; exact_mod_cast Nat.pos_of_neZero _)

Premises used: padicNormE.defn
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ∀ i ≥ N,
    (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk s) (↑((↑s : ℕ → ℚ) i) : ℚ_[p])) <
      HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk s) (↑((↑s : ℕ → ℚ) (N + n)) : ℚ_[p])) <
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))

Tactic:
replace hN := hN (N + n) (Nat.le_add_right N n)
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  (padicNormE : (a : ℚ_[p]) → ℚ) (HSub.hSub (α := ℚ_[p]) (mk s) (↑((↑s : ℕ → ℚ) (N + n)) : ℚ_[p])) <
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
⊢ LT.lt (α := ℝ)
    (↑((padicNormE : (a : ℚ_[p]) → ℚ)
          ((↑(HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])) : ℚ_[p]) -
            (↑((↑s : ℕ → ℚ) (N + n)) : ℚ_[p]))) :
      ℝ)
    (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))) : ℝ)

Tactic:
rw [← hs, he, ← Rat.cast_lt (K := ℝ)] at hN

Premises used: Rat.cast_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  LT.lt (α := ℝ)
    (↑((padicNormE : (a : ℚ_[p]) → ℚ)
          ((↑(HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])) : ℚ_[p]) -
            (↑((↑s : ℕ → ℚ) (N + n)) : ℚ_[p]))) :
      ℝ)
    (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))) : ℝ)
⊢ (↑((padicNormE : (a : ℚ_[p]) → ℚ)
          (HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑(x.appr n) : ℚ_[p]) -
            (↑((↑s : ℕ → ℚ) (N + n)) : ℚ_[p]))) :
      ℝ) <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
push_cast at hN
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  (↑((padicNormE : (a : ℚ_[p]) → ℚ)
          (HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑(x.appr n) : ℚ_[p]) -
            (↑((↑s : ℕ → ℚ) (N + n)) : ℚ_[p]))) :
      ℝ) <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
simp only [← add_sub, s, Rat.cast_intCast, padicNormE.is_norm,
    ← Int.cast_natCast (R := ℚ_[p]) (x.appr n), ← Int.cast_sub] at hN

Premises used: Int.cast_natCast, Rat.cast_intCast, Int.cast_sub, add_sub, Padic.padicNormE.is_norm, PadicInt.appr
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
by_contra! :
  ∀
    (H :
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])),
    False
⊢ norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])

Tactic:
LE.le.trans_lt ?_ H

Premises used: LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
refine : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])

Tactic:
refine LE.le.trans_lt ?_ H

Premises used: LE.le.trans_lt
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ 0 ≤ (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
simpa using mul_le_mul_of_nonneg le_rfl e.2 (show 0 ≤ (↑p ^ n)⁻¹ by simp) zero_le_one

Premises used: le_rfl, mul_le_mul_of_nonneg, zero_le_one, Subtype.property
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])

Tactic:
have H' : ‖(p ^ n * e : ℚ_[p])‖ < ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ := by
      refine LE.le.trans_lt ?_ H
      simpa using mul_le_mul_of_nonneg le_rfl e.2 (show 0 ≤ (↑p ^ n)⁻¹ by simp) zero_le_one
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
H' :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN

Premises used: Iff.mpr, LT.lt.le, sup_eq_right, Padic.add_eq_max_of_ne, LT.lt.ne
-- Module: Mathlib.NumberTheory.Padics.RingHoms
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n : ℕ
x : ℤ_[p] := ofIntSeq f ⋯
s : PadicSeq p := Subtype.mk (p := fun (f : ℕ → ℚ) ↦ IsCauSeq (padicNorm p) f) (fun (x : ℕ) ↦ (↑(f x) : ℚ)) ⋯
hs : (↑x : ℚ_[p]) = mk s
e : ℤ_[p]
he : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
N : ℕ
hN :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p]) + (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])‖ <
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
H' :
  ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])
hN₁ : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) < HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])

Tactic:
rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN

Premises used: Iff.mpr, LT.lt.le, sup_eq_right, Padic.add_eq_max_of_ne, LT.lt.ne