awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
⊢ ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε
have obtain : ∀ (x : ℚ_[p]) (hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε),
  ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε
Tactic: obtain ⟨x, hx⟩ := complete' f
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (q : ℚ_[p]), ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - q) < ε
have refine : ∀ (ε : ℚ) (hε : ε > 0), ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
Tactic: refine ⟨x, fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
have obtain : ∀ (N : ℕ) (hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε),
  ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
Tactic: obtain ⟨N, hN⟩ := hx ε hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
⊢ ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
have refine : ∀ (i : ℕ) (hi : i ≥ N), (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
Tactic: refine ⟨N, fun i hi => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : CauSeq (α := ℚ) ℚ_[p] (⇑padicNormE : (a : ℚ_[p]) → ℚ)
x : ℚ_[p]
hx : ∀ ε > 0, ∃ (N : ℕ), ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
i : ℕ
hi : i ≥ N
⊢ (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) i - x) < ε
have rw : (padicNormE : (a : ℚ_[p]) → ℚ) (x - (↑f : ℕ → ℚ_[p]) i) < ε
Tactic: rw [padicNormE.map_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
h : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0
⊢ x = y
have h₁ : x - y = 0
Tactic: apply eq_of_sub_eq_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
h : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (x - y)) : ℝ) 0
⊢ x - y = 0
have h₁ : Eq (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) (x - y) : ℚ) (0 : ℚ)
Tactic: apply padicNormE.eq_zero.1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = ‖-x + y‖
have rw : dist x y = ‖y - x‖
Tactic: rw [add_comm, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = ‖y - x‖
have change : ‖x - y‖ = ‖y - x‖
Tactic: change ‖x - y‖ = ‖y - x‖
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ ‖x - y‖ = ‖y - x‖
have this : y - x = -1 * (x - y)
Tactic: have : y - x = (-1) * (x - y) := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ Membership.mem (γ := Set ℚ_[p]) (closure (Set.range Rat.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.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ)
⊢ Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (q + r)) : ℝ)
    (max (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ))
have this : Ne (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) q : ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) r : ℚ)
Tactic: have : padicNormE q ≠ padicNormE r := mod_cast h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p])) : ℝ) (↑(padicNorm p q) : ℝ)
have rw : Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p])) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p])) : ℝ)
Tactic: rw [← padicNormE.eq_padic_norm']
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (E := ℚ_[p]) (↑p : ℚ_[p]) < 1
have rw : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
Tactic: rw [norm_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
have rw : norm (E := ℚ_[p]) (↑p : ℚ_[p]) ^ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
Tactic: rw [norm_zpow, norm_p, zpow_neg, inv_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
rw : norm (E := ℚ_[p]) (↑p : ℚ_[p]) ^ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
have rw₁ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
Tactic: rw [norm_zpow, norm_p, zpow_neg, inv_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
rw : norm (E := ℚ_[p]) (↑p : ℚ_[p]) ^ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
rw₁ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
have rw₂ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ n = (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
Tactic: rw [norm_zpow, norm_p, zpow_neg, inv_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
rw : norm (E := ℚ_[p]) (↑p : ℚ_[p]) ^ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
rw₁ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ n = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
rw₂ : HPow.hPow (α := ℝ) (↑p : ℝ)⁻¹ n = (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)
have rw₃ : (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
Tactic: rw [norm_zpow, norm_p, zpow_neg, inv_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = ‖HPow.hPow (α := ℚ_[p]) (β := ℤ) (↑p : ℚ_[p]) (↑n : ℤ)‖
Tactic: rw [← norm_p_zpow, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = ‖HPow.hPow (α := ℚ_[p]) (β := ℤ) (↑p : ℚ_[p]) (↑n : ℤ)‖
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))
have rw₁ : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖
Tactic: rw [← norm_p_zpow, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < norm (E := ℚ_[p]) (↑p : ℚ_[p])⁻¹
have rw : LT.lt (α := ℝ) 1 (↑p : ℝ)
Tactic: rw [norm_inv, norm_p, inv_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Ne (α := ℚ_[p]) ⟦f⟧ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = HPow.hPow (α := ℚ) (↑p : ℚ) (-n)
⊢ norm (E := ℚ_[p]) ⟦f⟧ = (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-n)) : ℝ)
have rw : norm (E := ℚ_[p]) ⟦f⟧ = (↑(PadicSeq.norm f) : ℝ)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
⊢ norm (E := ℚ_[p]) (↑{ num := n, den := d, den_nz := hn, reduced := hd : ℚ } : ℚ_[p]) ≤ 1
have this : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } = 0
Tactic: have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
⊢ norm (E := ℚ_[p]) (↑{ num := n, den := d, den_nz := hn, reduced := hd : ℚ } : ℚ_[p]) ≤ 1
have hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
Tactic: have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
⊢ norm (E := ℚ_[p]) (↑{ num := n, den := d, den_nz := hn, reduced := hd : ℚ } : ℚ_[p]) ≤ 1
have rw : LE.le (α := ℝ) (↑(padicNorm p { num := n, den := d, den_nz := hn, reduced := hd }) : ℝ) 1
Tactic: rw [eq_padicNorm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
⊢ LE.le (α := ℝ) (↑(padicNorm p { num := n, den := d, den_nz := hn, reduced := hd }) : ℝ) 1
have norm_cast : padicNorm p { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≤ 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
⊢ padicNorm p { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≤ 1
have rw : (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num))⁻¹ ≤ 1
Tactic: rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub,
        padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
⊢ (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num))⁻¹ ≤ 1
have ha : 1 ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num)
Tactic: apply inv_le_one_of_one_le₀
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
⊢ 1 ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num)
have ha : 1 ≤ p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≠ 0
⊢ 1 ≤ p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num
have ha : 0 < p
Tactic: apply one_le_pow
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 ↔ (↑p : ℤ) ∣ k
have mp : norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 → (↑p : ℤ) ∣ k
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
mp : norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 → (↑p : ℤ) ∣ k
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 ↔ (↑p : ℤ) ∣ k
have mpr : (↑p : ℤ) ∣ k → norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1
⊢ (↑p : ℤ) ∣ k
have mp : ∀ (h : ¬(↑p : ℤ) ∣ k), 1 ≤ norm (E := ℚ_[p]) (↑k : ℚ_[p])
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
⊢ 1 ≤ norm (E := ℚ_[p]) (↑k : ℚ_[p])
have mp : 1 = norm (E := ℚ_[p]) (↑k : ℚ_[p])
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
⊢ 1 = norm (E := ℚ_[p]) (↑k : ℚ_[p])
have mp : norm (E := ℚ_[p]) (↑k : ℚ_[p]) = 1
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) = norm (E := ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p])
have norm_cast : norm (E := ℚ_[p]) (↑k : ℚ_[p]) = norm (E := ℚ_[p]) (↑k : ℚ_[p])
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) = 1
have by : norm (E := ℚ_[p]) (↑k : ℚ_[p]) = norm (E := ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p])
Tactic: calc
      ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
      _ = padicNorm p k := eq_padicNorm _
      _ = 1 := mod_cast (int_eq_one_iff k).mpr h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ norm (E := ℚ_[p]) (↑((↑p : ℤ) * x) : ℚ_[p]) < 1
have mpr : ‖HMul.hMul (α := ℚ_[p]) (↑p : ℚ_[p]) (↑x : ℚ_[p])‖ < 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖HMul.hMul (α := ℚ_[p]) (↑p : ℚ_[p]) (↑x : ℚ_[p])‖ < 1
have mpr : norm (E := ℚ_[p]) (↑p : ℚ_[p]) * norm (E := ℚ_[p]) (↑x : ℚ_[p]) < 1
Tactic: rw [padicNormE.mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ norm (E := ℚ_[p]) (↑p : ℚ_[p]) * 1 < 1
have rw : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
Tactic: rw [mul_one, norm_p]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ norm (E := ℚ_[p]) (↑p : ℚ_[p]) * norm (E := ℚ_[p]) (↑x : ℚ_[p]) < 1
have _ : norm (E := ℚ_[p]) (↑p : ℚ_[p]) * 1 < 1
Tactic: calc
      _ ≤ ‖(p : ℚ_[p])‖ * 1 :=
        mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
      _ < 1 := by
        rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ norm (E := ℚ_[p]) (↑z : ℚ_[p]) = 1 ↔ IsCoprime z (↑p : ℤ)
have rw : ¬norm (E := ℚ_[p]) (↑z : ℚ_[p]) = 1 ↔ ¬IsCoprime z (↑p : ℤ)
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k
have this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
Tactic: have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
⊢ Eq (α := ℚ_[p]) (↑k : ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p])
have norm_cast : k = k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k
have rw : (↑(padicNorm p (↑k : ℚ)) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ)) ↔
  HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k
Tactic: rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
⊢ (↑(padicNorm p (↑k : ℚ)) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ)) ↔
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k
have norm_cast : padicNorm p (↑k : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) ↔ (↑(p ^ n) : ℤ) ∣ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
⊢ padicNorm p (↑k : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) ↔ (↑(p ^ n) : ℤ) ∣ k
have rw : (↑(p ^ n) : ℤ) ∣ k ↔ (↑(p ^ n) : ℤ) ∣ k
Tactic: rw [← padicNorm.dvd_iff_norm_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z2‖ ≤ ‖z1 + z2‖
have rw : ‖z2‖ ≤ max ‖z1‖ ‖z2‖
Tactic: rw [add_eq_max_of_ne hne]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ ‖z1 + z2‖
have rw : ‖z1‖ ≤ max ‖z1‖ ‖z2‖
Tactic: rw [add_eq_max_of_ne hne]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
⊢ ‖z1‖ = ‖z2‖
have rw : ‖z1‖ = ‖-z2‖
Tactic: rw [← norm_neg z2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
⊢ ‖z1‖ = ‖-z2‖
have h₁ : ‖z1 + -z2‖ < ‖-z2‖
Tactic: apply norm_eq_of_norm_add_lt_right
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z1‖ = ‖z2‖
have rw : ‖z2‖ = ‖z1‖
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z2‖ = ‖z1‖
have h₁ : ‖z2 - z1‖ < ‖z1‖
Tactic: apply norm_eq_of_norm_sub_lt_right
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (E := ℚ_[p]) (↑(p - 1) : ℚ_[p]) = 1
have rw : p.Coprime (p - 1)
Tactic: rw [norm_natCast_eq_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i) < ε
have h : ∃ (i : ℕ), ∀ j ≥ i, ‖(↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i‖ < (↑ε : ℝ)
Tactic: have h := isCauSeq f ε (mod_cast hε)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
⊢ ∃ (b : ℚ_[p]), f ≈ const norm b
have cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
Tactic: have cau_seq_norm_e : IsCauSeq padicNormE f := fun ε hε => by
      have h := isCauSeq f ε (mod_cast hε)
      dsimp [norm] at h
      exact mod_cast h
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
⊢ ∃ (b : ℚ_[p]), f ≈ const norm b
have obtain : ∀ (q : ℚ_[p])
  (hq :
    ∀ ε > 0,
      ∃ (N : ℕ),
        ∀ i ≥ N,
          (padicNormE : (a : ℚ_[p]) → ℚ)
              ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                        (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                    ℕ → ℚ_[p])
                  i -
                q) <
            ε),
  ∃ (b : ℚ_[p]), f ≈ const norm b
Tactic: obtain ⟨q, hq⟩ := Padic.complete'' ⟨f, cau_seq_norm_e⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
⊢ ∃ (b : ℚ_[p]), f ≈ const norm b
have exists : f ≈ const norm q
Tactic: exists q
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
have obtain : ∀ (ε' : ℚ) (hε' : LT.lt (α := ℝ) 0 (↑ε' : ℝ) ∧ (↑ε' : ℝ) < ε),
  ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
Tactic: obtain ⟨ε', hε'⟩ := exists_rat_btwn hε
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) (↑f : ℕ → ℚ_[p])
q : ℚ_[p]
hq :
  ∀ ε > 0,
    ∃ (N : ℕ),
      ∀ i ≥ N,
        (padicNormE : (a : ℚ_[p]) → ℚ)
            ((↑(Subtype.mk (p := fun (f : ℕ → ℚ_[p]) ↦ IsCauSeq (α := ℚ) (⇑padicNormE : (a : ℚ_[p]) → ℚ) f)
                      (↑f : ℕ → ℚ_[p]) cau_seq_norm_e) :
                  ℕ → ℚ_[p])
                i -
              q) <
          ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : LT.lt (α := ℝ) 0 (↑ε' : ℝ) ∧ (↑ε' : ℝ) < ε
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑(f - const norm q) : ℕ → ℚ_[p]) j‖ < ε
have hε'₁ : 0 < ε' ∧ (↑ε' : ℝ) < ε
Tactic: norm_cast at hε'
Cleared hypotheses: hε'