awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
have 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))
Tactic: change (toZModPow n).comp g x = (toZModPow n).comp g' x
-- 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
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))
have 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))
Tactic: rw [hg n]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      padicNorm p (HSub.hSub (α := ℚ) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) j) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) i)) < ε
have obtain : ∀ (k : ℕ) (hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε),
  ∃ (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ε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 (HSub.hSub (α := ℚ) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) j) ((fun (x : ℕ) ↦ ((↑(f x) : ℚ) : ℚ)) i)) < ε
have simp : ∃ (i : ℕ), ∀ j ≥ i, padicNorm p (↑(f j - f i) : ℚ) < ε
Tactic: simp only [← Int.cast_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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) : ℚ) < ε
have refine : ∀ (i : ℕ) (hik : i ≥ k), (↑(p ^ k) : ℤ) ∣ f i - f k
Tactic: refine ⟨k, fun i hik ↦ (padicNorm.dvd_iff_norm_le.mp ?_).trans_lt hk⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (↑(p ^ k) : ℤ) ∣ f i - f k
have obtain : ∀ (i : ℕ) (hik : k + i ≥ k), (↑(p ^ k) : ℤ) ∣ f (k + i) - f k
Tactic: obtain ⟨i, rfl⟩ := exists_add_of_le hik
Cleared hypotheses: i, hik
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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) : ℤ) ∣ f (k + (n + 1)) - f k
have this : (↑(p ^ k) : ℤ) ∣ HPow.hPow (α := ℤ) (↑p : ℤ) (k + n)
Tactic: have : (↑(p ^ k) : ℤ) ∣ ↑p ^ (k + n) := ⟨p ^ n, by simp [pow_add]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 : ℕ
⊢ (↑(p ^ k) : ℤ) ∣ f (k + i) - f k
have zero : (↑(p ^ k) : ℤ) ∣ f (k + 0) - 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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ (↑(p ^ k) : ℤ) ∣ f (k + i) - f k
have succ : ∀ (n : ℕ) (IH : (↑(p ^ k) : ℤ) ∣ f (k + n) - f k), (↑(p ^ k) : ℤ) ∣ f (k + (n + 1)) - 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
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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) : ℚ)) ⋯
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have hs : (↑x : ℚ_[p]) = mk s
Tactic: have hs : x = Padic.mk s := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have 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))
Tactic: obtain ⟨e, he⟩ := Ideal.mem_span_singleton.mp (PadicInt.appr_spec n x)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have he₁ : x = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n * e + (↑(x.appr n) : ℤ_[p])
Tactic: rw [sub_eq_iff_eq_add] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 : ℤ))
have simp : 0 < HPow.hPow (α := ℚ) (↑p : ℚ) n
Tactic: simp only [zpow_neg, zpow_natCast, inv_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have 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))
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 _)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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 : ℤ))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have hN₁ : (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)
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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 : ℤ))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have 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 : ℤ))) : ℝ)
Tactic: rw [← hs, he, ← Rat.cast_lt (K := ℝ)] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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 : ℤ))) : ℝ)
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have hN₁ : (↑((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
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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 : ℤ))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have hN₁ : ‖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
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 : ℤ))
⊢ norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have by_contra! : ∀ (H : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p])),
  False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])
have refine : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n * (↑e : ℚ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
Tactic: refine LE.le.trans_lt ?_ H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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])
⊢ False
have H' : ‖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
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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])
⊢ False
have hN₁ : 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
Cleared hypotheses: hN, H, H'
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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 : ℤ))
⊢ Eq (α := ZMod (p ^ n)) ((toZModPow n : (a : ℤ_[p]) → ZMod (p ^ n)) x : ZMod (p ^ n))
    ((↑(f n) : ZMod (p ^ n)) : ZMod (p ^ n))
have this : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
Tactic: have : ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ ≤ ↑p ^ (-n : ℤ) := by
    by_contra! H
    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
    rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN
    exact lt_asymm hN H
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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 : ℤ))
this : norm (E := ℚ_[p]) (↑((↑(x.appr n) : ℤ) - f (N + n)) : ℚ_[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))
have this₁ : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(x.appr n) : ZMod (p ^ n))
Tactic: rw [Padic.norm_int_le_pow_iff_dvd, ← Nat.cast_pow,
    ← ZMod.intCast_eq_intCast_iff_dvd_sub, Int.cast_natCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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 : ℤ))
this : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(x.appr 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))
have refine : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
Tactic: refine this.symm.trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
IH : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) (↑(f (N + 1 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
have succ : (↑(p ^ n) : ℤ) ∣ f (N + n + 1) - f (N + n)
Tactic: rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
⊢ Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
have zero : Eq (α := ZMod (p ^ n)) (↑(f (0 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
Tactic: induction N with
  | zero => simp
  | succ N IH =>
    rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
    exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
f : ℕ → ℤ
p : ℕ
inst : Fact (Nat.Prime p)
hi : ∀ (i : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ f (i + 1) - f i
n N : ℕ
zero : Eq (α := ZMod (p ^ n)) (↑(f (0 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
⊢ Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
have succ : ∀ (N : ℕ) (IH : Eq (α := ZMod (p ^ n)) (↑(f (N + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))),
  Eq (α := ZMod (p ^ n)) (↑(f (N + 1 + n)) : ZMod (p ^ n)) (↑(f n) : ZMod (p ^ n))
Tactic: induction N with
  | zero => simp
  | succ N IH =>
    rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
    exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ IsUniformInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
have hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
Tactic: have hp0' : 0 < (p : ℚ) := by simp [Nat.Prime.pos Fact.out]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
⊢ IsUniformInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
have hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
Tactic: have hp0 : 0 < (p : ℝ)⁻¹ := by simp [Nat.Prime.pos Fact.out]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
⊢ IsUniformInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
have hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
Tactic: have hp1' : 1 < (p : ℚ) := by simp [Nat.Prime.one_lt Fact.out]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.WithVal (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp0' : LT.lt (α := ℚ) 0 (↑p : ℚ)
hp0 : LT.lt (α := ℝ) 0 (↑p : ℝ)⁻¹
hp1' : LT.lt (α := ℚ) 1 (↑p : ℚ)
⊢ IsUniformInducing (α := WithVal (Rat.padicValuation p)) (β := ℚ_[p])
    (⇑(RingHom.comp (Rat.castHom ℚ_[p]) (WithVal.equiv (Rat.padicValuation p)).toRingHom) :
      (a : WithVal (Rat.padicValuation p)) → ℚ_[p])
have hp1 : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
Tactic: have hp1 : (p : ℝ)⁻¹ < 1 := by simp [inv_lt_one_iff₀, Nat.Prime.one_lt Fact.out]