awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ)
⊢ Ne (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) q : ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) r : ℚ)

Tactic:
have : padicNormE q ≠ padicNormE r := mod_cast h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ)
this : Ne (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) q : ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) r : ℚ)
⊢ Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (q + r)) : ℝ)
    (max (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ))

Tactic:
mod_cast padicNormE.add_eq_max_of_ne' this

Premises used: padicNormE, Rat.cast_max._simp_1, congrArg, Rat.cast_inj._simp_1, padicNormE.add_eq_max_of_ne', cast, Rat.cast, HAdd.hAdd, Eq.symm, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ)
this : Ne (α := ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) q : ℚ) ((padicNormE : (a : ℚ_[p]) → ℚ) r : ℚ)
⊢ Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (q + r)) : ℝ)
    (max (↑((padicNormE : (a : ℚ_[p]) → ℚ) q) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) r) : ℝ))

Tactic:
exact mod_cast padicNormE.add_eq_max_of_ne' this

Premises used: padicNormE.add_eq_max_of_ne'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
rw rw₁ :
  Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p])) : ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p])) : ℝ)
⊢ Eq (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) (↑q : ℚ_[p])) : ℝ) (↑(padicNorm p q) : ℝ)

Tactic:
rw [← padicNormE.eq_padic_norm']

Premises used: padicNormE.eq_padic_norm'
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm (E := ℚ_[p]) (↑(↑p : ℚ) : ℚ_[p]) = (↑(↑p : ℚ) : ℝ)⁻¹

Tactic:
simp [hp.1.ne_zero, norm, padicNorm, padicValRat, padicValInt, zpow_neg,
    -Rat.cast_natCast]

Premises used: Norm.norm, padicValInt, padicValRat, Rat.cast_natCast, Nat.Prime.ne_zero, zpow_neg, padicNorm, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
⊢ norm (E := ℚ_[p]) (↑p : ℚ_[p]) < 1

Tactic:
rw [norm_p]

Premises used: Padic.norm_p
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, inv_lt_one_of_one_lt₀, LT.lt, congrFun', Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Premises used: Nat.Prime.one_lt, inv_lt_one_of_one_lt₀, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)⁻¹
rw₃ rw₄ : (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹ = (HPow.hPow (α := ℝ) (↑p : ℝ) n)⁻¹
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (↑p : ℝ) (-n)

Tactic:
rw [norm_zpow, norm_p, zpow_neg, inv_zpow]

Premises used: inv_zpow, zpow_neg, norm_zpow, Padic.norm_p
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
rw : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = ‖HPow.hPow (α := ℚ_[p]) (β := ℤ) (↑p : ℚ_[p]) (↑n : ℤ)‖
rw₁ rw₂ : ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖
⊢ ‖HPow.hPow (α := ℚ_[p]) (↑p : ℚ_[p]) n‖ = HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ))

Tactic:
rw [← norm_p_zpow, zpow_natCast]

Premises used: zpow_natCast, Padic.norm_p_zpow
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : LT.lt (α := ℝ) 1 (↑p : ℝ)
⊢ 1 < norm (E := ℚ_[p]) (↑p : ℚ_[p])⁻¹

Tactic:
rw [norm_inv, norm_p, inv_inv]

Premises used: norm_inv, inv_inv, Padic.norm_p
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
mod_cast hp.1.one_lt

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
exact mod_cast hp.1.one_lt

Premises used: Nat.Prime.one_lt, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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)
rw : norm (E := ℚ_[p]) ⟦f⟧ = (↑(PadicSeq.norm f) : ℝ)
⊢ norm (E := ℚ_[p]) ⟦f⟧ = (↑(HPow.hPow (α := ℚ) (↑p : ℚ) (-n)) : ℝ)

Tactic:
rw [← hn]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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⟧ = (↑(PadicSeq.norm f) : ℝ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
h : q = 0
⊢ ‖q‖ = (↑0 : ℝ)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ∃ (q' : ℚ), ‖q‖ = (↑q' : ℝ)

Tactic:
exact if h : q = 0 then ⟨0, by simp [h]⟩
  else
    let ⟨n, hn⟩ := padicNormE.image h
    ⟨_, hn⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ∃ (q' : ℚ), ‖q‖ = (↑q' : ℝ)

Tactic:
classical
  exact if h : q = 0 then ⟨0, by simp [h]⟩
  else
    let ⟨n, hn⟩ := padicNormE.image h
    ⟨_, hn⟩
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
⊢ ‖q‖ = (↑q.ratNorm : ℝ)

Tactic:
Classical.choose_spec (padicNormE.is_rat q)

Premises used: Padic.padicNormE.is_rat, Classical.choose_spec, Padic.ratNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
⊢ { num := n, den := d, den_nz := hn, reduced := hd : ℚ } = 0

Tactic:
have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : n = 0
this : { num := n, den := d, den_nz := hn, reduced := hd : ℚ } = 0
⊢ norm (E := ℚ_[p]) (↑{ num := n, den := d, den_nz := hn, reduced := hd : ℚ } : ℚ_[p]) ≤ 1

Tactic:
norm_num [this]
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : n.natAbs.Coprime d
hq : ¬p ∣ d
hnz : ¬n = 0
⊢ { 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
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw : LE.le (α := ℝ) (↑(padicNorm p { num := n, den := d, den_nz := hn, reduced := hd }) : ℝ) 1
⊢ norm (E := ℚ_[p]) (↑{ num := n, den := d, den_nz := hn, reduced := hd : ℚ } : ℚ_[p]) ≤ 1

Tactic:
rw [eq_padicNorm]

Premises used: Padic.eq_padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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_cast : padicNorm p { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≤ 1
⊢ LE.le (α := ℝ) (↑(padicNorm p { num := n, den := d, den_nz := hn, reduced := hd }) : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
rw : (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num))⁻¹ ≤ 1
⊢ padicNorm p { num := n, den := d, den_nz := hn, reduced := hd : ℚ } ≤ 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]

Premises used: zpow_natCast, neg_sub, padicNorm.eq_zpow_of_nonzero, padicValRat, zpow_neg, Nat.cast_zero, padicValNat.eq_zero_of_not_dvd, zero_sub
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
ha : 1 ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num)
⊢ (HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num))⁻¹ ≤ 1

Tactic:
apply inv_le_one_of_one_le₀

Premises used: inv_le_one_of_one_le₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
ha : 1 ≤ p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num
⊢ 1 ≤ HPow.hPow (α := ℚ) (↑p : ℚ) (padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
ha : 0 < p
⊢ 1 ≤ p ^ padicValInt p { num := n, den := d, den_nz := hn, reduced := hd : ℚ }.num

Tactic:
apply one_le_pow

Premises used: Nat.one_le_pow
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ 0 < p

Tactic:
hp.1.pos

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
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
⊢ 0 < p

Tactic:
exact hp.1.pos

Premises used: Nat.Prime.pos, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬p ∣ Rat.den (↑z : ℚ)

Tactic:
simp [hp.1.ne_one]

Premises used: Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
this : norm (E := ℚ_[p]) (↑(↑z : ℚ) : ℚ_[p]) ≤ 1
⊢ norm (E := ℚ_[p]) (↑z : ℚ_[p]) ≤ 1

Tactic:
simpa
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
mp : norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 → (↑p : ℤ) ∣ k
mpr : (↑p : ℤ) ∣ k → norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1 ↔ (↑p : ℤ) ∣ k

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : norm (E := ℚ_[p]) (↑k : ℚ_[p]) < 1
mp : ∀ (h : ¬(↑p : ℤ) ∣ k), 1 ≤ norm (E := ℚ_[p]) (↑k : ℚ_[p])
⊢ (↑p : ℤ) ∣ k

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
mp : 1 = norm (E := ℚ_[p]) (↑k : ℚ_[p])
⊢ 1 ≤ norm (E := ℚ_[p]) (↑k : ℚ_[p])

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
mp : norm (E := ℚ_[p]) (↑k : ℚ_[p]) = 1
⊢ 1 = norm (E := ℚ_[p]) (↑k : ℚ_[p])

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : norm (E := ℚ_[p]) (↑k : ℚ_[p]) = norm (E := ℚ_[p]) (↑k : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) = norm (E := ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p])

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
⊢ norm (E := ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p]) = (↑(padicNorm p (↑k : ℚ)) : ℝ)

Tactic:
eq_padicNorm _

Premises used: Padic.eq_padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
⊢ Eq (α := ℝ) (↑(padicNorm p (↑k : ℚ)) : ℝ) 1

Tactic:
mod_cast (int_eq_one_iff k).mpr h

Premises used: Iff.mpr, Int.cast, padicNorm.int_eq_one_iff, congrArg, Rat.cast_inj._simp_1, cast, Rat.cast, padicNorm, Eq.symm, Eq, Nat.cast_one, Eq.trans, Rat.cast_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬(↑p : ℤ) ∣ k
by : norm (E := ℚ_[p]) (↑k : ℚ_[p]) = norm (E := ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p])
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) = 1

Tactic:
calc
      ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
      _ = padicNorm p k := eq_padicNorm _
      _ = 1 := mod_cast (int_eq_one_iff k).mpr h

Premises used: Iff.mpr, Int.cast, Padic.eq_padicNorm, padicNorm.int_eq_one_iff, Rat.cast, padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
mpr : ‖HMul.hMul (α := ℚ_[p]) (↑p : ℚ_[p]) (↑x : ℚ_[p])‖ < 1
⊢ norm (E := ℚ_[p]) (↑((↑p : ℤ) * x) : ℚ_[p]) < 1

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
mpr : norm (E := ℚ_[p]) (↑p : ℚ_[p]) * norm (E := ℚ_[p]) (↑x : ℚ_[p]) < 1
⊢ ‖HMul.hMul (α := ℚ_[p]) (↑p : ℚ_[p]) (↑x : ℚ_[p])‖ < 1

Tactic:
rw [padicNormE.mul]

Premises used: Padic.padicNormE.mul
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ norm (E := ℚ_[p]) (↑x : ℚ_[p]) ≤ 1

Tactic:
simpa using norm_int_le_one _

Premises used: Padic.norm_int_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
rw : LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1
⊢ norm (E := ℚ_[p]) (↑p : ℚ_[p]) * 1 < 1

Tactic:
rw [mul_one, norm_p]

Premises used: mul_one, Padic.norm_p
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Premises used: Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, inv_lt_one_of_one_lt₀, LT.lt, congrFun', Eq.symm, Nat.cast_one, Fact.out, Eq.trans
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ LT.lt (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Premises used: Nat.Prime.one_lt, inv_lt_one_of_one_lt₀, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
_ : norm (E := ℚ_[p]) (↑p : ℚ_[p]) * 1 < 1
⊢ norm (E := ℚ_[p]) (↑p : ℚ_[p]) * norm (E := ℚ_[p]) (↑x : ℚ_[p]) < 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

Premises used: le_rfl, Nat.cast, mul_le_mul, norm_nonneg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ norm (E := ℚ_[p]) (↑n : ℚ_[p]) < 1 ↔ p ∣ n

Tactic:
simpa [Int.natCast_dvd_natCast] using norm_intCast_lt_one_iff (p := p) (k := n)

Premises used: Padic.norm_intCast_lt_one_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
rw : ¬norm (E := ℚ_[p]) (↑z : ℚ_[p]) = 1 ↔ ¬IsCoprime z (↑p : ℤ)
⊢ norm (E := ℚ_[p]) (↑z : ℚ_[p]) = 1 ↔ IsCoprime z (↑p : ℤ)

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬norm (E := ℚ_[p]) (↑z : ℚ_[p]) = 1 ↔ ¬IsCoprime z (↑p : ℤ)

Tactic:
simp [Nat.coprime_comm, ← norm_natCast_lt_one_iff, -norm_intCast_lt_one_iff,
    Int.isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, Int.gcd,
    ← hp.out.dvd_iff_not_coprime, norm_natAbs, -cast_natAbs, norm_int_le_one]

Premises used: Int.gcd, Int.isCoprime_iff_gcd_eq_one, Padic.norm_int_le_one, Padic.norm_natCast_lt_one_iff, Nat.cast_natAbs, Nat.Prime.dvd_iff_not_coprime, norm_natAbs, Padic.norm_intCast_lt_one_iff, Nat.coprime_comm, Nat.coprime_iff_gcd_eq_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ norm (E := ℚ_[p]) (↑n : ℚ_[p]) = 1 ↔ p.Coprime n

Tactic:
simpa [p.coprime_comm] using norm_intCast_eq_one_iff (p := p) (z := n)

Premises used: Padic.norm_intCast_eq_one_iff, Nat.coprime_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))

Tactic:
have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : k = k
⊢ Eq (α := ℚ_[p]) (↑k : ℚ_[p]) (↑(↑k : ℚ) : ℚ_[p])

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
rw :
  (↑(padicNorm p (↑k : ℚ)) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ)) ↔
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k
⊢ norm (E := ℚ_[p]) (↑k : ℚ_[p]) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) ↔ HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k

Tactic:
rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]

Premises used: Padic.eq_padicNorm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
norm_cast : padicNorm p (↑k : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) ↔ (↑(p ^ n) : ℤ) ∣ k
⊢ (↑(padicNorm p (↑k : ℚ)) : ℝ) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ)) ↔
    HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ k

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑n : ℤ)) = HPow.hPow (α := ℝ) (β := ℤ) (↑(↑p : ℚ) : ℝ) (-(↑n : ℤ))
rw rw₁ : (↑(p ^ n) : ℤ) ∣ k ↔ (↑(p ^ n) : ℤ) ∣ k
⊢ padicNorm p (↑k : ℚ) ≤ HPow.hPow (α := ℚ) (β := ℤ) (↑p : ℚ) (-(↑n : ℤ)) ↔ (↑(p ^ n) : ℤ) ∣ k

Tactic:
rw [← padicNorm.dvd_iff_norm_le]

Premises used: padicNorm.dvd_iff_norm_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
rw : ‖z2‖ ≤ max ‖z1‖ ‖z2‖
⊢ ‖z2‖ ≤ ‖z1 + z2‖

Tactic:
rw [add_eq_max_of_ne hne]

Premises used: Padic.add_eq_max_of_ne
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z2‖ ≤ max ‖z1‖ ‖z2‖

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
rw : ‖z1‖ ≤ max ‖z1‖ ‖z2‖
⊢ ‖z1‖ ≤ ‖z1 + z2‖

Tactic:
rw [add_eq_max_of_ne hne]

Premises used: Padic.add_eq_max_of_ne
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ max ‖z1‖ ‖z2‖

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
rw : ‖z1‖ = ‖-z2‖
⊢ ‖z1‖ = ‖z2‖

Tactic:
rw [← norm_neg z2]

Premises used: norm_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
h₁ : ‖z1 + -z2‖ < ‖-z2‖
⊢ ‖z1‖ = ‖-z2‖

Tactic:
apply norm_eq_of_norm_add_lt_right

Premises used: Padic.norm_eq_of_norm_add_lt_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z2‖
⊢ ‖z1 + -z2‖ < ‖-z2‖

Tactic:
simp [← sub_eq_add_neg, h]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
rw : ‖z2‖ = ‖z1‖
⊢ ‖z1‖ = ‖z2‖

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
h₁ : ‖z2 - z1‖ < ‖z1‖
⊢ ‖z2‖ = ‖z1‖

Tactic:
apply norm_eq_of_norm_sub_lt_right

Premises used: Padic.norm_eq_of_norm_sub_lt_right
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 - z2‖ < ‖z1‖
⊢ ‖z2 - z1‖ < ‖z1‖

Tactic:
simpa [← norm_neg (z1 - _)] using h

Premises used: HSub.hSub, norm_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
rw : p.Coprime (p - 1)
⊢ norm (E := ℚ_[p]) (↑(p - 1) : ℚ_[p]) = 1

Tactic:
rw [norm_natCast_eq_one_iff]

Premises used: Padic.norm_natCast_eq_one_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ p.Coprime (p - 1)

Tactic:
(coprime_self_sub_right hp.out.one_le).mpr p.coprime_one_right

Premises used: Iff.mpr, Nat.coprime_self_sub_right, Nat.Prime.one_le, Nat.coprime_one_right, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ p.Coprime (p - 1)

Tactic:
exact (coprime_self_sub_right hp.out.one_le).mpr p.coprime_one_right

Premises used: Iff.mpr, Nat.coprime_self_sub_right, Nat.Prime.one_le, Nat.coprime_one_right, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
⊢ ∃ (i : ℕ), ∀ j ≥ i, ‖(↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i‖ < (↑ε : ℝ)

Tactic:
have h := isCauSeq f ε (mod_cast hε)
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
h :
  ∃ (i : ℕ),
    ∀ j ≥ i, LT.lt (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i)) : ℝ) (↑ε : ℝ)
⊢ ∃ (i : ℕ), ∀ j ≥ i, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i) < ε

Tactic:
mod_cast h

Premises used: congrArg, cast, Exists, GE.ge, funext, implies_congr, Eq.refl, Rat.cast_lt._simp_1, forall_congr
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
h :
  ∃ (i : ℕ),
    ∀ j ≥ i, LT.lt (α := ℝ) (↑((padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i)) : ℝ) (↑ε : ℝ)
⊢ ∃ (i : ℕ), ∀ j ≥ i, (padicNormE : (a : ℚ_[p]) → ℚ) ((↑f : ℕ → ℚ_[p]) j - (↑f : ℕ → ℚ_[p]) i) < ε

Tactic:
exact mod_cast h
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
⊢ 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