awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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))
⊢ (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))
have pos₂ : ¬x + x_1 = 0 → x = 0 → x_1 = 0 → exp (-(x + x_1).valuation) ≤ max 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ (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))
have neg₂ : ¬x + x_1 = 0 → x = 0 → ¬x_1 = 0 → exp (-(x + x_1).valuation) ≤ max 0 (exp (-x_1.valuation))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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))
⊢ (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))
have pos₃ : ¬x + x_1 = 0 → ¬x = 0 → x_1 = 0 → exp (-(x + x_1).valuation) ≤ max (exp (-x.valuation)) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ (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))
have neg₃ : ¬x + x_1 = 0 → ¬x = 0 → ¬x_1 = 0 → exp (-(x + x_1).valuation) ≤ max (exp (-x.valuation)) (exp (-x_1.valuation))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)) (exp (-x_1.valuation))
have neg : x.valuation ≤ (x + x_1).valuation ∨ x_1.valuation ≤ (x + x_1).valuation
Tactic: simp_all [inv_le_inv₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valuation.comap (R := ℚ_[p]) (Rat.castHom ℚ_[p]) mulValuation = Rat.padicValuation p
have 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 ℤ))
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valuation.comap (R := ℚ_[p]) (Int.castRingHom ℚ_[p]) mulValuation = Int.padicValuation p
have 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 ℤ))
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
Tactic: have aux (n : ℤ) : 0 < ((p : ℝ) ^ n) := zpow_pos (mod_cast hp.1.pos) _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have pos : ∀ (hx0 : x = 0), ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)
⊢ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have neg : ∀ (hx0 : ¬x = 0), ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)
have neg : HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
  HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
Tactic: rw [norm_eq_zpow_neg_valuation hx0]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < HPow.hPow (α := ℝ) (↑p : ℝ) n
hx0 : ¬x = 0
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have h1p : LT.lt (α := ℝ) 1 (↑p : ℝ)
Tactic: have h1p : 1 < (p : ℝ) := mod_cast hp.1.one_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (hypothesis)
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 : ℝ)
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have H : StrictMono (β := ℝ) fun (n : ℤ) ↦ HPow.hPow (α := ℝ) (↑p : ℝ) n
Tactic: have H := zpow_right_strictMono₀ h1p
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have neg : -x.valuation ≤ 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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)
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have neg₁ : -x.valuation ≤ n ↔ -x.valuation < n + 1
Tactic: rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
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
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) ≤ HPow.hPow (α := ℝ) (↑p : ℝ) n ↔
    HPow.hPow (α := ℝ) (↑p : ℝ) (-x.valuation) < HPow.hPow (α := ℝ) (↑p : ℝ) (n + 1)
have neg₂ : -x.valuation ≤ n ↔ -x.valuation ≤ n
Tactic: rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1)
have rw : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1 + 1)
Tactic: rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
rw : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1 + 1)
⊢ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ ≤ HPow.hPow (α := ℝ) (↑p : ℝ) (n - 1)
have rw₁ : ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n ↔ ‖x‖ < HPow.hPow (α := ℝ) (↑p : ℝ) n
Tactic: rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
have pos : ∀ (hx : x = 0), ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
pos : ∀ (hx : x = 0), ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
have neg : ∀ (hx : ¬x = 0), ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicNumbers (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
have neg : LT.lt (α := ℝ) 1 (↑p : ℝ)
Tactic: rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValInt p z = multiplicity (↑p : ℤ) z
have rw : multiplicity p z.natAbs = multiplicity (↑p : ℤ) z
Tactic: rw [padicValInt, padicValNat_def' hp (Int.natAbs_ne_zero.mpr hz)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
z : ℤ
⊢ padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
have rw : padicValNat p z.natAbs = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
Tactic: rw [padicValInt, padicValNat.eq_zero_iff, Int.natAbs_eq_zero, ← Int.ofNat_dvd_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
z : ℤ
rw : padicValNat p z.natAbs = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
⊢ padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
have rw₁ : p = 1 ∨ z.natAbs = 0 ∨ ¬p ∣ z.natAbs ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
Tactic: rw [padicValInt, padicValNat.eq_zero_iff, Int.natAbs_eq_zero, ← Int.ofNat_dvd_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
have rw₂ : p = 1 ∨ z = 0 ∨ ¬p ∣ z.natAbs ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
Tactic: rw [padicValInt, padicValNat.eq_zero_iff, Int.natAbs_eq_zero, ← Int.ofNat_dvd_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ padicValInt p z = 0 ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
have rw₃ : p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z ↔ p = 1 ∨ z = 0 ∨ ¬(↑p : ℤ) ∣ z
Tactic: rw [padicValInt, padicValNat.eq_zero_iff, Int.natAbs_eq_zero, ← Int.ofNat_dvd_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValRat p (↑z : ℚ) = (↑(multiplicity (↑p : ℤ) z) : ℤ)
have rw : Eq (α := ℤ) (↑(padicValInt p z) : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
Tactic: rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
rw : Eq (α := ℤ) (↑(padicValInt p z) : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
⊢ padicValRat p (↑z : ℚ) = (↑(multiplicity (↑p : ℤ) z) : ℤ)
have rw₁ : Eq (α := ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ) (↑(multiplicity (↑p : ℤ) z) : ℤ)
Tactic: rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)
have rw : HSub.hSub (α := ℤ) (↑(padicValInt p q.num) : ℤ) (↑(padicValNat p q.den) : ℤ) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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) : ℤ)
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)
have rw₁ : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(padicValNat p q.den) : ℤ) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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) : ℤ)
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ)
have rw₂ : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
  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]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ padicValNat p p = 1
have rw : multiplicity p p = 1
Tactic: rw [padicValNat_def (@Fact.out p.Prime).ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
⊢ 1 ≤ padicValNat p n
have rwa : (↑1 : WithTop ℕ) ≤ (↑(padicValNat p n) : WithTop ℕ)
Tactic: rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn,
    ← pow_dvd_iff_le_emultiplicity, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
div : p ∣ n
rwa : (↑1 : WithTop ℕ) ≤ (↑(padicValNat p n) : WithTop ℕ)
⊢ 1 ≤ padicValNat p n
have rwa₁ : LE.le (α := WithTop ℕ) (↑1 : WithTop ℕ) (↑(padicValNat p n) : WithTop ℕ)
Tactic: rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn,
    ← pow_dvd_iff_le_emultiplicity, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 ℕ)
⊢ 1 ≤ padicValNat p n
have rwa₂ : (↑1 : WithTop ℕ) ≤ emultiplicity p n
Tactic: rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn,
    ← pow_dvd_iff_le_emultiplicity, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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
⊢ 1 ≤ padicValNat p n
have rwa₃ : HPow.hPow (β := ℕ) p 1 ∣ n
Tactic: rwa [← WithTop.coe_le_coe, ENat.some_eq_coe, padicValNat_eq_emultiplicity hn,
    ← pow_dvd_iff_le_emultiplicity, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
have hd : d ≠ 0
Tactic: have hd : d ≠ 0 := Rat.mk_denom_ne_zero_of_ne_zero hqz qdf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
n d : ℤ
hqz : q ≠ 0
qdf : q = n /. d
hd : d ≠ 0
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
have let : ∀ (c : ℤ) (hc1 : n = c * q.num) (hc2 : d = c * (↑q.den : ℤ)),
  padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
Tactic: let ⟨c, hc1, hc2⟩ := Rat.num_den_mk hd qdf
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 : ℤ)
⊢ padicValRat p q = HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
have rw : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
Tactic: rw [padicValRat.multiplicity_sub_multiplicity hp.1.ne_one hqz]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) n) : ℤ) (↑(multiplicity (↑p : ℤ) d) : ℤ)
have simp : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (c * q.num)) : ℤ) (↑(multiplicity (↑p : ℤ) (c * (↑q.den : ℤ))) : ℤ)
Tactic: simp only [hc1, hc2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (c * q.num)) : ℤ) (↑(multiplicity (↑p : ℤ) (c * (↑q.den : ℤ))) : ℤ)
have 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 : ℤ)) : ℤ)
Tactic: rw [multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1),
    multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 : ℤ)) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (c * q.num)) : ℤ) (↑(multiplicity (↑p : ℤ) (c * (↑q.den : ℤ))) : ℤ)
have rw₁ : FiniteMultiplicity (↑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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 : ℤ))
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (c * q.num)) : ℤ) (↑(multiplicity (↑p : ℤ) (c * (↑q.den : ℤ))) : ℤ)
have rw₂ : FiniteMultiplicity (↑p : ℤ) (c * q.num)
Tactic: rw [multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1),
    multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
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 : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) c) : ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) -
      HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) c) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ)
have simp_rw : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity p q.den) : ℤ) =
  HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) c) : ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) -
    HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) c) : ℤ) (↑(multiplicity p q.den) : ℤ)
Tactic: simp_rw [Int.natCast_multiplicity p q.den]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
have rw : mkRat (q.num * r.num) (q.den * r.den) = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
rw : mkRat (q.num * r.num) (q.den * r.den) = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
have rw₁ : q.num * r.num /. (↑(q.den * r.den) : ℤ) = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]