awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
rw₁ : 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 /. HMul.hMul (α := ℤ) (↑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 (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
have this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
Tactic: have : q * r = (q.num * r.num) /. (q.den * r.den) := by
    rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
have hq' : q.num /. (↑q.den : ℤ) ≠ 0
Tactic: have hq' : q.num /. q.den ≠ 0 := by rwa [Rat.num_divInt_den]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
have hr' : r.num /. (↑r.den : ℤ) ≠ 0
Tactic: have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_divInt_den]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
have hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
Tactic: have hp' : Prime (p : ℤ) := 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 r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r
have rw : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
    (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
  padicValRat p q + padicValRat p r
Tactic: rw [padicValRat.defn p (mul_ne_zero hq hr) this]
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
| padicValRat p q + padicValRat p r
have rw : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
Tactic: rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
rw :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
| padicValRat p q + padicValRat p r
have rw₁ : r.num /. (↑r.den : ℤ) = r.num /. (↑r.den : ℤ)
Tactic: rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
rw :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
rw₁ : r.num /. (↑r.den : ℤ) = r.num /. (↑r.den : ℤ)
| padicValRat p q + padicValRat p r
have rw₂ : ℤ
Tactic: rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
rw :
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
rw₁ : r.num /. (↑r.den : ℤ) = r.num /. (↑r.den : ℤ)
rw₂ rw₃ : ℤ
| padicValRat p q + padicValRat p r
have rw₄ : q.num /. (↑q.den : ℤ) = q.num /. (↑q.den : ℤ)
Tactic: rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
      (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
    padicValRat p q + padicValRat p r
have conv_rhs : HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
    (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
Tactic: conv_rhs =>
    rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
      (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
      HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
have rw : HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) -
    HAdd.hAdd (α := ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ)
      (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ) =
  HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
Tactic: rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
rw :
  HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) -
      HAdd.hAdd (α := ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ)
        (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
      HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
      (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
      HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
have rw₁ : FiniteMultiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))
Tactic: rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]
-- 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
this : q * r = q.num * r.num /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hq' : q.num /. (↑q.den : ℤ) ≠ 0
hr' : r.num /. (↑r.den : ℤ) ≠ 0
hp' : _root_.Prime (M := ℤ) (↑p : ℤ)
rw :
  HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) -
      HAdd.hAdd (α := ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ)
        (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
      HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
rw₁ : FiniteMultiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
      (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
    HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) q.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ)) : ℤ) +
      HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) r.num) : ℤ) (↑(multiplicity (α := ℤ) (↑p : ℤ) (↑r.den : ℤ)) : ℤ)
have rw₂ : FiniteMultiplicity (↑p : ℤ) (q.num * r.num)
Tactic: rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
k : ℕ
⊢ padicValRat p (q ^ k) = (↑k : ℤ) * padicValRat p q
have zero : padicValRat p (HPow.hPow (β := ℕ) q 0) = (↑0 : ℤ) * padicValRat p q
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
k : ℕ
zero : padicValRat p (HPow.hPow (β := ℕ) q 0) = (↑0 : ℤ) * padicValRat p q
⊢ padicValRat p (q ^ k) = (↑k : ℤ) * padicValRat p q
have succ : ∀ (n : ℕ),
  padicValRat p (q ^ n) = (↑n : ℤ) * padicValRat p q → padicValRat p (q ^ (n + 1)) = (↑(n + 1) : ℤ) * padicValRat p q
Tactic: induction k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ padicValRat p q⁻¹ = -padicValRat p q
have pos : ∀ (hq : q = 0), padicValRat p q⁻¹ = -padicValRat p q
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
pos : ∀ (hq : q = 0), padicValRat p q⁻¹ = -padicValRat p q
⊢ padicValRat p q⁻¹ = -padicValRat p q
have neg : ∀ (hq : ¬q = 0), padicValRat p q⁻¹ = -padicValRat p q
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
have neg : padicValRat p q⁻¹ + padicValRat p q = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
      padicValRat.one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
neg : padicValRat p q⁻¹ + padicValRat p q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
have neg₁ : padicValRat p (q⁻¹ * q) = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
      padicValRat.one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
neg : padicValRat p q⁻¹ + padicValRat p q = 0
neg₁ : padicValRat p (q⁻¹ * q) = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
have neg₂ : padicValRat p 1 = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
      padicValRat.one]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
neg : padicValRat p q⁻¹ + padicValRat p q = 0
neg₁ : padicValRat p (q⁻¹ * q) = 0
neg₂ : padicValRat p 1 = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q
have neg₃ : Eq (α := ℤ) 0 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
      padicValRat.one]
-- 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
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r
have rw : padicValRat p (q * r⁻¹) = padicValRat p q - padicValRat p r
Tactic: rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]
-- 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 : padicValRat p (q * r⁻¹) = padicValRat p q - padicValRat p r
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r
have rw₁ : padicValRat p q + padicValRat p r⁻¹ = padicValRat p q - padicValRat p r
Tactic: rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]
-- 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 : padicValRat p (q * r⁻¹) = padicValRat p q - padicValRat p r
rw₁ : padicValRat p q + padicValRat p r⁻¹ = padicValRat p q - padicValRat p r
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r
have rw₂ : padicValRat p q + -padicValRat p r = padicValRat p q - padicValRat p r
Tactic: rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]
-- 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 : padicValRat p (q * r⁻¹) = padicValRat p q - padicValRat p r
rw₁ : padicValRat p q + padicValRat p r⁻¹ = padicValRat p q - padicValRat p r
rw₂ : padicValRat p q + -padicValRat p r = padicValRat p q - padicValRat p r
⊢ padicValRat p (q / r) = padicValRat p q - padicValRat p r
have rw₃ : padicValRat p q + -padicValRat p r = padicValRat p q + -padicValRat p r
Tactic: rw [div_eq_mul_inv, padicValRat.mul hq (inv_ne_zero hr), padicValRat.inv r, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
have hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
Tactic: have hf1 : FiniteMultiplicity (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
have hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
Tactic: have hf2 : FiniteMultiplicity (p : ℤ) (n₂ * d₁) := finite_int_prime_iff.2 (mul_ne_zero hn₂ hd₁)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
have lhs : padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂)
Tactic: lhs
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂)
have rw : HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) n₁) : ℤ) (↑(multiplicity (↑p : ℤ) d₂) : ℤ) ≤
  HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) d₁) : ℤ) (↑(multiplicity (↑p : ℤ) n₂) : ℤ)
Tactic: rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
      padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ←
      add_sub_assoc, le_sub_iff_add_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
| HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) n₁) : ℤ) (↑(multiplicity (↑p : ℤ) d₂) : ℤ) ≤
    HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) d₁) : ℤ) (↑(multiplicity (↑p : ℤ) n₂) : ℤ)
have norm_cast : multiplicity (↑p : ℤ) n₁ + multiplicity (↑p : ℤ) d₂ ≤ multiplicity (↑p : ℤ) d₁ + multiplicity (↑p : ℤ) n₂
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
| multiplicity (↑p : ℤ) n₁ + multiplicity (↑p : ℤ) d₂ ≤ multiplicity (↑p : ℤ) d₁ + multiplicity (↑p : ℤ) n₂
have rw : ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
Tactic: rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
        ← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,
        hf1.multiplicity_le_multiplicity_iff hf2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
have rw : ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
Tactic: lhs
    rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
      padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ←
      add_sub_assoc, le_sub_iff_add_le]
    norm_cast
    rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
        ← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,
        hf1.multiplicity_le_multiplicity_iff hf2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
have conv : padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
  ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
Tactic: conv =>
    lhs
    rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
      padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ←
      add_sub_assoc, le_sub_iff_add_le]
    norm_cast
    rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
        ← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,
        hf1.multiplicity_le_multiplicity_iff hf2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hf1 : FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)
hf2 : FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)
conv :
  padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
⊢ padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
have conv₁ : (∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁) ↔
  ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
Tactic: conv =>
    lhs
    rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
      padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ←
      add_sub_assoc, le_sub_iff_add_le]
    norm_cast
    rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm,
        ← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2,
        hf1.multiplicity_le_multiplicity_iff hf2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hqn : q.num ≠ 0
Tactic: have hqn : q.num ≠ 0 := Rat.num_ne_zero.2 hq
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
Tactic: have hqd : (q.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hrn : r.num ≠ 0
Tactic: have hrn : r.num ≠ 0 := Rat.num_ne_zero.2 hr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.PadicVal.Basic (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : Ne (α := ℤ) (↑q.den : ℤ) 0
hrn : r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
Tactic: have hrd : (r.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _