awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
le_valuation_add hxy

Premises used: Padic.le_valuation_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
exact le_valuation_add hxy

Premises used: Padic.le_valuation_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (if Eq (α := ℚ_[p]) 0 0 then 0 else exp (-valuation (p := p) 0)) = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (if Eq (α := ℚ_[p]) 1 0 then 0 else exp (-valuation (p := p) 1)) = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x * x_1 = 0 → x = 0 → x_1 = 0 → 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg : x * x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 = 0 * exp (-x_1.valuation)
pos₁ : x * x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 = exp (-x.valuation) * 0
neg₁ : x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 = exp (-x.valuation) * exp (-x_1.valuation)
pos₂ : ¬x * x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0
neg₂ : ¬x * x_1 = 0 → x = 0 → ¬x_1 = 0 → exp (-(x * x_1).valuation) = 0 * exp (-x_1.valuation)
pos₃ : ¬x * x_1 = 0 → ¬x = 0 → x_1 = 0 → exp (-(x * x_1).valuation) = exp (-x.valuation) * 0
neg₃ : ¬x * x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → exp (-(x * x_1).valuation) = exp (-x.valuation) * exp (-x_1.valuation)
⊢ (if x * x_1 = 0 then 0 else exp (-(x * x_1).valuation)) =
    (if x = 0 then 0 else exp (-x.valuation)) * if x_1 = 0 then 0 else exp (-x_1.valuation)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x * x_1 = 0
h_1 : x = 0
h_2 : x_1 = 0
⊢ 0 = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x * x_1 = 0
h_1 : x = 0
h_2 : ¬x_1 = 0
⊢ 0 = 0 * exp (-x_1.valuation)

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x * x_1 = 0
h_1 : ¬x = 0
h_2 : x_1 = 0
⊢ 0 = exp (-x.valuation) * 0

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x * x_1 = 0
h_1 : ¬x = 0
h_2 : ¬x_1 = 0
⊢ 0 = exp (-x.valuation) * exp (-x_1.valuation)

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x * x_1 = 0
h_1 : x = 0
h_2 : x_1 = 0
⊢ exp (-(x * x_1).valuation) = HMul.hMul (α := WithZero (Multiplicative ℤ)) 0 0

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x * x_1 = 0
h_1 : x = 0
h_2 : ¬x_1 = 0
⊢ exp (-(x * x_1).valuation) = 0 * exp (-x_1.valuation)

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x * x_1 = 0
h_1 : ¬x = 0
h_2 : x_1 = 0
⊢ exp (-(x * x_1).valuation) = exp (-x.valuation) * 0

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x * x_1 = 0
h_1 : ¬x = 0
h_2 : ¬x_1 = 0
⊢ exp (-(x * x_1).valuation) = exp (-x.valuation) * exp (-x_1.valuation)

Tactic:
simp_all [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
pos : x + x_1 = 0 → x = 0 → x_1 = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + x_1 = 0 → x = 0 → ¬x_1 = 0 → 0 ≤ max 0 (exp (-x_1.valuation))
pos₁ : x + x_1 = 0 → ¬x = 0 → x_1 = 0 → 0 ≤ max (exp (-x.valuation)) 0
neg₁ : x + x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → 0 ≤ max (exp (-x.valuation)) (exp (-x_1.valuation))
pos₂ : ¬x + x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x + x_1).valuation) ≤ max 0 0
neg₂ : ¬x + x_1 = 0 → x = 0 → ¬x_1 = 0 → exp (-(x + x_1).valuation) ≤ max 0 (exp (-x_1.valuation))
pos₃ : ¬x + x_1 = 0 → ¬x = 0 → x_1 = 0 → exp (-(x + x_1).valuation) ≤ max (exp (-x.valuation)) 0
neg₃ : ¬x + x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → exp (-(x + x_1).valuation) ≤ max (exp (-x.valuation)) (exp (-x_1.valuation))
⊢ (if x + x_1 = 0 then 0 else exp (-(x + x_1).valuation)) ≤
    max (if x = 0 then 0 else exp (-x.valuation)) (if x_1 = 0 then 0 else exp (-x_1.valuation))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x + x_1 = 0
h_1 : x = 0
h_2 : x_1 = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x + x_1 = 0
h_1 : x = 0
h_2 : ¬x_1 = 0
⊢ 0 ≤ max 0 (exp (-x_1.valuation))

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x + x_1 = 0
h_1 : ¬x = 0
h_2 : x_1 = 0
⊢ 0 ≤ max (exp (-x.valuation)) 0

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : x + x_1 = 0
h_1 : ¬x = 0
h_2 : ¬x_1 = 0
⊢ 0 ≤ max (exp (-x.valuation)) (exp (-x_1.valuation))

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x + x_1 = 0
h_1 : x = 0
h_2 : x_1 = 0
⊢ exp (-(x + x_1).valuation) ≤ max 0 0

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x + x_1 = 0
h_1 : x = 0
h_2 : ¬x_1 = 0
⊢ exp (-(x + x_1).valuation) ≤ max 0 (exp (-x_1.valuation))

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x + x_1 = 0
h_1 : ¬x = 0
h_2 : x_1 = 0
⊢ exp (-(x + x_1).valuation) ≤ max (exp (-x.valuation)) 0

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x + x_1 = 0
h_1 : ¬x = 0
h_2 : ¬x_1 = 0
neg : x.valuation ≤ (x + x_1).valuation ∨ x_1.valuation ≤ (x + x_1).valuation
⊢ exp (-(x + x_1).valuation) ≤ max (exp (-x.valuation)) (exp (-x_1.valuation))

Tactic:
simp_all [inv_le_inv₀]

Premises used: inv_le_inv₀
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x x_1 : ℚ_[p]
h : ¬x + x_1 = 0
h_1 : ¬x = 0
h_2 : ¬x_1 = 0
⊢ x.valuation ≤ (x + x_1).valuation ∨ x_1.valuation ≤ (x + x_1).valuation

Tactic:
simpa using le_valuation_add ‹_›

Premises used: Padic.le_valuation_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h :
  ∀ (r : ℚ),
    Eq (α := WithZero (Multiplicative ℤ))
      ((Valuation.comap (R := ℚ_[p]) (Rat.castHom ℚ_[p]) mulValuation : (a : ℚ) → WithZero (Multiplicative ℤ)) r :
        WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
⊢ Valuation.comap (R := ℚ_[p]) (Rat.castHom ℚ_[p]) mulValuation = Rat.padicValuation p

Tactic:
ext
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℚ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((Valuation.comap (R := ℚ_[p]) (Rat.castHom ℚ_[p]) mulValuation : (a : ℚ) → WithZero (Multiplicative ℤ)) r :
      WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))

Tactic:
simp [Rat.padicValuation]

Premises used: Rat.padicValuation
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
h :
  ∀ (r : ℤ),
    Eq (α := WithZero (Multiplicative ℤ))
      ((Valuation.comap (R := ℚ_[p]) (Int.castRingHom ℚ_[p]) mulValuation : (a : ℤ) → WithZero (Multiplicative ℤ)) r :
        WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))
⊢ Valuation.comap (R := ℚ_[p]) (Int.castRingHom ℚ_[p]) mulValuation = Int.padicValuation p

Tactic:
ext
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℤ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((Valuation.comap (R := ℚ_[p]) (Int.castRingHom ℚ_[p]) mulValuation : (a : ℤ) → WithZero (Multiplicative ℤ)) r :
      WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) r : WithZero (Multiplicative ℤ))

Tactic:
simp [← Rat.padicValuation_cast, ← comap_mulValuation_eq_padicValuation]

Premises used: Rat.padicValuation_cast, Padic.comap_mulValuation_eq_padicValuation
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ ‖x‖ =
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (WithZero.log ((mulValuation : (a : ℚ_[p]) → WithZero (Multiplicative ℤ)) x))

Tactic:
simp [norm_eq_zpow_neg_valuation, hx]

Premises used: Padic.norm_eq_zpow_neg_valuation
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ (addValuation : (a : ℚ_[p]) → WithTop ℤ) x = (↑x.valuation : WithTop ℤ)

Tactic:
simp only [Padic.addValuation, AddValuation.of_apply, addValuationDef, if_neg hx]

Premises used: Padic.addValuationDef, AddValuation.of_apply, Padic.addValuation, if_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n

Tactic:
have aux (n : ℤ) : 0 < ((p : ℝ) ^ n) := zpow_pos (mod_cast hp.1.pos) _
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
pos : ∀ (hx0 : x = 0), ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
neg : ∀ (hx0 : ¬x = 0), ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
hx0 : x = 0
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)

Tactic:
simp [hx0, norm_zero, aux, le_of_lt (aux _)]

Premises used: norm_zero, le_of_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
hx0 : ¬x = 0
neg :
  HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)

Tactic:
rw [norm_eq_zpow_neg_valuation hx0]

Premises used: Padic.norm_eq_zpow_neg_valuation
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
hx0 : ¬x = 0
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
have h1p : 1 < (p : ℝ) := mod_cast hp.1.one_lt
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
hx0 : ¬x = 0
h1p : LT.lt (α := ℝ) 1 (↑p : ℝ)
⊢ StrictMono (β := ℝ) fun (n : ℤ) ↦ HPow.hPow (α := ℝ) (↑p : ℝ) n

Tactic:
have H := zpow_right_strictMono₀ h1p
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
hx0 : ¬x = 0
h1p : LT.lt (α := ℝ) 1 (↑p : ℝ)
H : StrictMono (β := ℝ) fun (n : ℤ) ↦ HPow.hPow (α := ℝ) (↑p : ℝ) n
neg : -x.valuation ≤ n ↔ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
neg₁ : -x.valuation ≤ n ↔ -x.valuation < n + 1
neg₂ neg₃ : -x.valuation ≤ n ↔ -x.valuation ≤ n
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)

Tactic:
rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]

Premises used: StrictMono.lt_iff_lt, StrictMono.le_iff_le, Int.lt_add_one_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
rw : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1 + 1)
rw₁ rw₂ : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n
⊢ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1)

Tactic:
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

Premises used: Padic.norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
pos : ∀ (hx : x = 0), ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
neg : ∀ (hx : ¬x = 0), ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]

Premises used: le_refl, norm_zero, Padic.valuation_zero, zero_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
neg : LT.lt (α := ℝ) 1 (↑p : ℝ)
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos]

Premises used: zpow_zero, zpow_le_zpow_iff_right₀, neg_nonpos, Padic.norm_eq_zpow_neg_valuation, Nat.cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

Premises used: Iff.mpr, Nat.one_lt_cast, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

Premises used: Iff.mpr, Nat.one_lt_cast, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
h : ¬p ∣ n
⊢ padicValNat p n = 0

Tactic:
eq_zero_iff.2 <| Or.inr <| Or.inr h

Premises used: Iff.mpr, padicValNat.eq_zero_iff, Or.inr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
rw : multiplicity p z.natAbs = multiplicity (↑p : ℤ) z
⊢ padicValInt p z = multiplicity (↑p : ℤ) z

Tactic:
rw [padicValInt, padicValNat_def' hp (Int.natAbs_ne_zero.mpr hz)]

Premises used: Iff.mpr, padicValInt, padicValNat_def', Int.natAbs_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ multiplicity p z.natAbs = multiplicity (↑p : ℤ) z

Tactic:
apply Int.multiplicity_natAbs

Premises used: Int.multiplicity_natAbs
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
⊢ padicValInt p 0 = 0

Tactic:
simp [padicValInt]

Premises used: padicValInt
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
⊢ padicValInt p 1 = 0

Tactic:
simp [padicValInt]

Premises used: padicValInt
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
⊢ padicValInt p (↑n : ℤ) = padicValNat p n

Tactic:
simp [padicValInt]

Premises used: padicValInt
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : 1 < p
⊢ padicValInt p (↑p : ℤ) = 1

Tactic:
simp [padicValNat.self hp]

Premises used: padicValNat.self
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
z : ℤ
rw : padicValNat p z.natAbs = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
rw₁ : p = 1 ∨ z.natAbs = 0 ∨ ¬p ∣ z.natAbs ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
rw₂ : p = 1 ∨ z = 0 ∨ ¬p ∣ z.natAbs ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
rw₃ rw₄ : p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
⊢ padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z

Tactic:
rw [padicValInt, padicValNat.eq_zero_iff, Int.natAbs_eq_zero, ← Int.ofNat_dvd_left]

Premises used: padicValNat.eq_zero_iff, padicValInt, Int.ofNat_dvd_left, Int.natAbs_eq_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
z : ℤ
h : ¬(↑p : ℤ) ∣ z
⊢ padicValInt p z = 0

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
q : ℚ
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(padicValInt p q.num) : ℤ) (↑(padicValNat p q.den) : ℤ)

Tactic:
rfl

Premises used: padicValRat, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
q : ℚ
⊢ padicValRat p (-q) = padicValRat p q

Tactic:
simp [padicValRat, padicValInt]

Premises used: padicValInt, padicValRat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
⊢ padicValRat p 0 = 0

Tactic:
simp [padicValRat]

Premises used: padicValRat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
⊢ padicValRat p 1 = 0

Tactic:
simp [padicValRat]

Premises used: padicValRat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
z : ℤ
⊢ padicValRat p (↑z : ℚ) = (↑(padicValInt p z) : ℤ)

Tactic:
simp [padicValRat]

Premises used: padicValRat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
rw : Eq (α := ℤ) (↑(padicValInt p z) : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
rw₁ rw₂ : Eq (α := ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
⊢ padicValRat p (↑z : ℚ) = (↑(multiplicity (↑p : ℤ) z) : ℤ)

Tactic:
rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]

Premises used: padicValRat.of_int, padicValInt.of_ne_one_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
rw :
  HSub.hSub (α := ℤ) (↑(padicValInt p q.num) : ℤ) (↑(padicValNat p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)
rw₁ :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(padicValNat p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)
rw₂ rw₃ :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)

Tactic:
rw [padicValRat, padicValInt.of_ne_one_ne_zero hp (Rat.num_ne_zero.2 hq),
    padicValNat_def' hp q.den_ne_zero]

Premises used: Iff.mpr, Rat.num_ne_zero, Rat.den_ne_zero, padicValRat, padicValNat_def', padicValInt.of_ne_one_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
⊢ padicValRat p (↑n : ℚ) = (↑(padicValNat p n) : ℤ)

Tactic:
simp [padicValRat]

Premises used: padicValRat
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : 1 < p
⊢ padicValRat p (↑p : ℚ) = 1

Tactic:
simp [hp]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
⊢ 0 ≤ padicValRat p (↑n : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
⊢ (↑(padicValNat p n) : ℤ) = padicValRat p (↑n : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : multiplicity p p = 1
⊢ padicValNat p p = 1

Tactic:
rw [padicValNat_def (@Fact.out p.Prime).ne_zero]

Premises used: padicValNat_def, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ multiplicity p p = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
rwa : (↑1 : WithTop ℕ) ≤ (↑(padicValNat p n) : WithTop ℕ)
rwa₁ : LE.le (α := WithTop ℕ) (↑1 : WithTop ℕ) (↑(padicValNat p n) : WithTop ℕ)
rwa₂ : (↑1 : WithTop ℕ) ≤ emultiplicity p n
rwa₃ : HPow.hPow (β := ℕ) p 1 ∣ n
rwa₄ rwa₅ rwa₆ rwa₇ : p ∣ n
⊢ 1 ≤ padicValNat p n

Tactic:
rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn,
    ← pow_dvd_iff_le_emultiplicity, pow_one]

Premises used: ENat.some_eq_coe, pow_dvd_iff_le_emultiplicity, pow_one, WithTop.coe_le_coe, padicValNat_eq_emultiplicity
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p n : ℕ
inst : Fact (Nat.Prime p)
hn0 : n ≠ 0
⊢ p ∣ n ↔ padicValNat p n ≠ 0

Tactic:
⟨fun h => one_le_iff_ne_zero.mp (one_le_padicValNat_of_dvd hn0 h), fun h =>
    Classical.not_not.1 (mt padicValNat.eq_zero_of_not_dvd h)⟩

Premises used: Classical.not_not, one_le_padicValNat_of_dvd, mt, Iff.intro, Iff.mp, Nat.one_le_iff_ne_zero, padicValNat.eq_zero_of_not_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ FiniteMultiplicity (↑p : ℤ) a ↔ a ≠ 0

Tactic:
simp [Int.finiteMultiplicity_iff, hp.1.ne_one]

Premises used: Int.finiteMultiplicity_iff, Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
⊢ d ≠ 0

Tactic:
have hd : d ≠ 0 := Rat.mk_denom_ne_zero_of_ne_zero hqz qdf
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
let :
  ∀ (c : ℤ) (hc1 : n = c * q.num) (hc2 : d = c * (↑q.den : ℤ)),
    padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)

Tactic:
let ⟨c, hc1, hc2⟩ := Rat.num_den_mk hd qdf
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * (↑q.den : ℤ)
rw :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)

Tactic:
rw [padicValRat.multiplicity_sub_multiplicity hp.1.ne_one hqz]

Premises used: Nat.Prime.ne_one, padicValRat.multiplicity_sub_multiplicity, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * (↑q.den : ℤ)
simp :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (c * q.num)) : ℤ) (↑(multiplicity (↑p : ℤ) (c * (↑q.den : ℤ))) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)

Tactic:
simp only [hc1, hc2]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
c : ℤ
hc1 : n = c * q.num
hc2 : d = c * (↑q.den : ℤ)
rw :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) c + multiplicity (↑p : ℤ) q.num) : ℤ)
      (↑(multiplicity (↑p : ℤ) c + multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ)
rw₁ : FiniteMultiplicity (↑p : ℤ) (c * (↑q.den : ℤ))
rw₂ : FiniteMultiplicity (↑p : ℤ) (c * q.num)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (c * q.num)) : ℤ) (↑(multiplicity (↑p : ℤ) (c * (↑q.den : ℤ))) : ℤ)

Tactic:
rw [multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1),
    multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1)]

Premises used: Nat.prime_iff_prime_int, multiplicity_mul, Iff.mp, Fact.out