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)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])
have 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])
Tactic: rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m ∣ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p])
have h₁ : HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
  HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
Tactic: use c
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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
⊢ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
have h₁ : (↑(x.appr n - 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])
⊢ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
have h₂ : (↑(p ^ m * c) : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
Tactic: rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])
⊢ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
have h₃ : HMul.hMul (α := ℤ_[p]) (↑(p ^ m) : ℤ_[p]) (↑c : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
Tactic: rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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])
⊢ HSub.hSub (α := ℤ_[p]) (↑(x.appr n) : ℤ_[p]) (↑(x.appr m) : ℤ_[p]) =
    HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
have h₄ : HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p]) = HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) m * (↑c : ℤ_[p])
Tactic: rw [← Nat.cast_sub (appr_mono _ h), hc, Nat.cast_mul, Nat.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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))
    ((toZModPow m : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
have 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 sorry (ZMod (p ^ m))) (toZModPow n) : (a : ℤ_[p]) → ZMod (p ^ m)) x : ZMod (p ^ m))
Tactic: rw [← zmod_cast_comp_toZModPow _ _ h]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Nat.cast)) x
have rw : ∀ ε > 0, ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε
Tactic: rw [Metric.mem_closure_range_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
⊢ ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε), ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε
Tactic: obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ ∃ (k : ℕ), dist x (↑k : ℤ_[p]) < ε
have h : dist x (↑(x.appr n) : ℤ_[p]) < ε
Tactic: use x.appr n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ dist x (↑(x.appr n) : ℤ_[p]) < ε
have h : ‖x - (↑(x.appr n) : ℤ_[p])‖ < ε
Tactic: rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ ‖x - (↑(x.appr n) : ℤ_[p])‖ < ε
have apply : ‖x - (↑(x.appr n) : ℤ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
Tactic: apply lt_of_le_of_lt _ hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
ε : ℝ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) < ε
⊢ ‖x - (↑(x.appr n) : ℤ_[p])‖ ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (↑p : ℤ_[p]) n}) (x - (↑(x.appr n) : ℤ_[p]))
Tactic: rw [norm_le_pow_iff_mem_span_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) x
have refine_1 : IsClosed (X := ℤ_[p]) {b : ℤ_[p] | Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) b}
Tactic: refine DenseRange.induction_on denseRange_natCast x ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
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}
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) x
have refine_2 : ∀ (a : ℕ), Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) (↑a : ℤ_[p])
Tactic: refine DenseRange.induction_on denseRange_natCast x ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
a : ℕ
⊢ Membership.mem (γ := Set ℤ_[p]) (closure (Set.range Int.cast)) (↑a : ℤ_[p])
have refine_2 : Membership.mem (γ := Set ℤ_[p]) (Set.range Int.cast) (↑a : ℤ_[p])
Tactic: apply subset_closure
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ nthHom f r j - nthHom f r i
have f_compat₁ : RingHom.comp (ZMod.castHom sorry (ZMod (p ^ i))) (f j) = f i
Tactic: specialize f_compat i j h
Cleared hypotheses: f_compat
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
r : R
i j : ℕ
h : i ≤ j
f_compat : RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ i))) (f j) = f i
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) i ∣ nthHom f r j - nthHom f r i
have rw : HSub.hSub (α := ZMod (p ^ i)) (↑(nthHom f r j) : ZMod (p ^ i)) (↑(nthHom f r i) : ZMod (p ^ i)) = 0
Tactic: rw [← Int.natCast_pow, ← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
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)) (↑(nthHom f r j) : ZMod (p ^ i)) (↑(nthHom f r i) : ZMod (p ^ i)) = 0
have 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
Tactic: dsimp [nthHom]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
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) ((f i : (a : R) → ZMod (p ^ i)) r)) : ℤ) : ZMod (p ^ i)) =
    0
have 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 sorry (ZMod (p ^ i)) : (a : ZMod (p ^ j)) → ZMod (p ^ i))
                ((f j : (a : R) → ZMod (p ^ j)) r))) :
          ℤ) :
      ZMod (p ^ i)) =
  0
Tactic: rw [← f_compat, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i,
      padicNorm p
          (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
            ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) i)) <
        ε
have 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)) <
        ε
Tactic: obtain ⟨k, hk⟩ : ∃ k : ℕ, (p : ℚ) ^ (-((k : ℕ) : ℤ)) < ε := exists_pow_neg_lt_rat p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
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)) <
        ε
have h : ∀ j ≥ k,
  padicNorm p
      (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
        ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) <
    ε
Tactic: use k
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p
      (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
        ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) <
    ε
have h : padicNorm p
    (HSub.hSub (α := ℚ) ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) j)
      ((fun (n : ℕ) ↦ ((↑(nthHom f r n) : ℚ) : ℚ)) k)) ≤
  HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))
Tactic: refine lt_of_le_of_lt ?_ hk
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p (HSub.hSub (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f r k) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))
have h : padicNorm p (↑(nthHom f r j - nthHom f r k) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ)) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p (↑(nthHom f r j - nthHom f r k) : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑k : ℤ))
have h : (↑(p ^ k) : ℤ) ∣ nthHom f r j - nthHom f r k
Tactic: rw [← padicNorm.dvd_iff_norm_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε
have hε₁ : 0 < ε
Tactic: change _ < _ at hε
Cleared hypotheses: hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε
have h : ∀ j ≥ 1, padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε
Tactic: use 1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (hypothesis)
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
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε
have this : Fact (1 < p ^ j)
Tactic: haveI : Fact (1 < p ^ j) := ⟨Nat.one_lt_pow (by lia) hp_prime.1.one_lt⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ padicNorm p ((↑(nthHomSeq f_compat 1 - 1) : ℕ → ℚ) j) < ε
have h : Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1
Tactic: suffices (ZMod.cast (1 : ZMod (p ^ j)) : ℚ) = 1 by simp [nthHomSeq, nthHom, this, hε]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
⊢ Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1
have h : Eq (α := ℚ) (↑(ZMod.val (n := p ^ j) 1) : ℚ) 1
Tactic: rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
h : Eq (α := ℚ) (↑(ZMod.val (n := p ^ j) 1) : ℚ) 1
⊢ Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1
have h₁ : Eq (α := ℚ) (↑1 : ℚ) 1
Tactic: rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
this : Fact (1 < p ^ j)
h : Eq (α := ℚ) (↑(ZMod.val (n := p ^ j) 1) : ℚ) 1
h₁ : Eq (α := ℚ) (↑1 : ℚ) 1
⊢ Eq (α := ℚ) (ZMod.cast (n := p ^ j) 1) 1
have h₂ : Eq (α := ℚ) 1 1
Tactic: rw [ZMod.cast_eq_val, ZMod.val_one, Nat.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε),
  ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε
Tactic: obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε
have h : ∀ j ≥ n, padicNorm p ((↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) : ℕ → ℚ) j) < ε
Tactic: use n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p ((↑(nthHom f (r + s) j) : ℚ) - HAdd.hAdd (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) < ε
have apply : padicNorm p ((↑(nthHom f (r + s) j) : ℚ) - HAdd.hAdd (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
  HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
Tactic: apply lt_of_le_of_lt _ hn
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p ((↑(nthHom f (r + s) j) : ℚ) - HAdd.hAdd (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
    HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
have rw : Eq (α := ZMod (p ^ n)) (↑(nthHom f (r + s) j - (nthHom f r j + nthHom f s j)) : ZMod (p ^ n)) 0
Tactic: rw [← Int.cast_add, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ←
    ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
⊢ Eq (α := ZMod (p ^ n))
    (↑((↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) (r + s))) : ℤ) -
          HAdd.hAdd (α := ℤ) (↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r)) : ℤ)
            (↑(ZMod.val (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) : ℤ)) :
      ZMod (p ^ n))
    0
have simp : (HAdd.hAdd (α := ZMod (p ^ j)) (β := ZMod (p ^ j)) ((f j : (a : R) → ZMod (p ^ j)) r : ZMod (p ^ j))
        ((f j : (a : R) → ZMod (p ^ j)) s : ZMod (p ^ j))).cast -
    HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
      (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
  0
Tactic: simp only [ZMod.natCast_val, map_add, Int.cast_sub, ZMod.intCast_cast, Int.cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
⊢ (HAdd.hAdd (α := ZMod (p ^ j)) (β := ZMod (p ^ j)) ((f j : (a : R) → ZMod (p ^ j)) r : ZMod (p ^ j))
          ((f j : (a : R) → ZMod (p ^ j)) s : ZMod (p ^ j))).cast -
      HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
        (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
    0
have rw : HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
      (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) -
    HAdd.hAdd (α := ZMod (p ^ n)) (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) r))
      (ZMod.cast (n := p ^ j) ((f j : (a : R) → ZMod (p ^ j)) s)) =
  0
Tactic: rw [ZMod.cast_add (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε),
  ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε
Tactic: obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
⊢ ∃ (i : ℕ),
    ∀ j ≥ i, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε
have h : ∀ j ≥ n, padicNorm p ((↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) : ℕ → ℚ) j) < ε
Tactic: use n
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.RingHoms (goal)
Goal:
R : Type u_1
inst : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ k1))) (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p ((↑(nthHom f (r * s) j) : ℚ) - HMul.hMul (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) < ε
have apply : padicNorm p ((↑(nthHom f (r * s) j) : ℚ) - HMul.hMul (α := ℚ) (↑(nthHom f r j) : ℚ) (↑(nthHom f s j) : ℚ)) ≤
  HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ))
Tactic: apply lt_of_le_of_lt _ hn