awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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) : ℤ)
⊢ 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]

Premises used: Int.natCast_multiplicity, Rat.den
-- 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 : ℤ)
⊢ 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:
ring
-- 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 : ℤ)
⊢ FiniteMultiplicity (↑p : ℤ) (c * (↑q.den : ℤ))

Tactic:
simpa [finite_int_prime_iff, hc2] using hd

Premises used: padicValRat.finite_int_prime_iff
-- 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 : ℤ)
⊢ FiniteMultiplicity (↑p : ℤ) (c * q.num)

Tactic:
simpa [finite_int_prime_iff, hqz, hc2] using hd

Premises used: padicValRat.finite_int_prime_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
rw₂ rw₃ :
  q.num * r.num /. HMul.hMul (α := ℤ) (↑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 : ℤ)

Tactic:
rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]

Premises used: Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)

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]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
rwa rwa₁ rwa₂ rwa₃ : q ≠ 0
⊢ q.num /. (↑q.den : ℤ) ≠ 0

Tactic:
rwa [Rat.num_divInt_den]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
⊢ q.num /. (↑q.den : ℤ) ≠ 0

Tactic:
have hq' : q.num /. q.den ≠ 0 := by rwa [Rat.num_divInt_den]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rwa rwa₁ rwa₂ rwa₃ : r ≠ 0
⊢ r.num /. (↑r.den : ℤ) ≠ 0

Tactic:
rwa [Rat.num_divInt_den]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ r.num /. (↑r.den : ℤ) ≠ 0

Tactic:
have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_divInt_den]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ _root_.Prime (M := ℤ) (↑p : ℤ)

Tactic:
have hp' : Prime (p : ℤ) := Nat.prime_iff_prime_int.1 hp.1
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 * r.num)) : ℤ)
      (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
    padicValRat p q + padicValRat p r
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Tactic:
rw [padicValRat.defn p (mul_ne_zero hq hr) this]

Premises used: padicValRat.defn, mul_ne_zero
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₃ : ℤ
rw₄ : q.num /. (↑q.den : ℤ) = q.num /. (↑q.den : ℤ)
rw₅ rw₆ : ℤ
| padicValRat p q + padicValRat p r

Tactic:
rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']

Premises used: Rat.num_divInt_den, padicValRat.defn
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
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 : ℤ)) : ℤ)
⊢ HSub.hSub (α := ℤ) (↑(multiplicity (↑p : ℤ) (q.num * r.num)) : ℤ)
      (↑(multiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))) : ℤ) =
    padicValRat p q + padicValRat p r

Tactic:
conv_rhs =>
    rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']

Premises used: Rat.num_divInt_den, padicValRat.defn
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ))
rw₂ : FiniteMultiplicity (↑p : ℤ) (q.num * r.num)
⊢ 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:
rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]

Premises used: Nat.cast_add, multiplicity_mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
⊢ 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:
ring
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
⊢ FiniteMultiplicity (↑p : ℤ) (HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ))

Tactic:
simp [finite_int_prime_iff]

Premises used: padicValRat.finite_int_prime_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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 : ℤ)
⊢ FiniteMultiplicity (↑p : ℤ) (q.num * r.num)

Tactic:
simp [finite_int_prime_iff, hq, hr]

Premises used: padicValRat.finite_int_prime_iff
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
k : ℕ
zero : padicValRat p (HPow.hPow (β := ℕ) q 0) = (↑0 : ℤ) * padicValRat p q
succ :
  ∀ (n : ℕ),
    padicValRat p (q ^ n) = (↑n : ℤ) * padicValRat p q → padicValRat p (q ^ (n + 1)) = (↑(n + 1) : ℤ) * padicValRat p q
⊢ padicValRat p (q ^ k) = (↑k : ℤ) * padicValRat p q

Tactic:
induction k
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
⊢ padicValRat p (HPow.hPow (β := ℕ) q 0) = (↑0 : ℤ) * padicValRat p q

Tactic:
simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ', add_mul, add_comm]

Premises used: add_mul, pow_ne_zero, add_comm, pow_succ', padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
n : ℕ
h : padicValRat p (q ^ n) = (↑n : ℤ) * padicValRat p q
⊢ padicValRat p (q ^ (n + 1)) = (↑(n + 1) : ℤ) * padicValRat p q

Tactic:
simp [*, padicValRat.mul hq (pow_ne_zero _ hq), _root_.pow_succ', add_mul, add_comm]

Premises used: add_mul, pow_ne_zero, add_comm, pow_succ', padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
pos : ∀ (hq : q = 0), padicValRat p q⁻¹ = -padicValRat p q
neg : ∀ (hq : ¬q = 0), padicValRat p q⁻¹ = -padicValRat p q
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
by_cases hq : q = 0
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
simp [hq]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
neg₃ neg₄ : Eq (α := ℤ) 0 0
⊢ padicValRat p q⁻¹ = -padicValRat p q

Tactic:
rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq,
      padicValRat.one]

Premises used: padicValRat.one, inv_ne_zero, eq_neg_iff_add_eq_zero, inv_mul_cancel₀, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
rw₃ rw₄ : padicValRat p q + -padicValRat p r = padicValRat p q + -padicValRat p r
⊢ 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]

Premises used: sub_eq_add_neg, div_eq_mul_inv, inv_ne_zero, padicValRat.inv, padicValRat.mul
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n₁ n₂ d₁ d₂ : ℤ
hn₁ : n₁ ≠ 0
hn₂ : n₂ ≠ 0
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
⊢ FiniteMultiplicity (↑p : ℤ) (n₁ * d₂)

Tactic:
have hf1 : FiniteMultiplicity (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₂)
⊢ FiniteMultiplicity (↑p : ℤ) (n₂ * d₁)

Tactic:
have hf2 : FiniteMultiplicity (p : ℤ) (n₂ * d₁) := finite_int_prime_iff.2 (mul_ne_zero hn₂ hd₁)
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₁)
lhs : padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔
    ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁

Tactic:
lhs
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₁)
rw :
  HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) n₁) : ℤ) (↑(multiplicity (↑p : ℤ) d₂) : ℤ) ≤
    HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) d₁) : ℤ) (↑(multiplicity (↑p : ℤ) n₂) : ℤ)
| padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂)

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]

Premises used: add_sub_assoc, sub_le_iff_le_add', Rat.divInt_ne_zero_of_ne_zero, padicValRat.defn, le_sub_iff_add_le, rfl
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₁)
norm_cast : multiplicity (↑p : ℤ) n₁ + multiplicity (↑p : ℤ) d₂ ≤ multiplicity (↑p : ℤ) d₁ + multiplicity (↑p : ℤ) n₂
| HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) n₁) : ℤ) (↑(multiplicity (↑p : ℤ) d₂) : ℤ) ≤
    HAdd.hAdd (α := ℤ) (↑(multiplicity (↑p : ℤ) d₁) : ℤ) (↑(multiplicity (↑p : ℤ) n₂) : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₁)
rw : ∀ (n : ℕ), HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₁ * d₂ → HPow.hPow (α := ℤ) (↑p : ℤ) n ∣ n₂ * d₁
| multiplicity (↑p : ℤ) n₁ + multiplicity (↑p : ℤ) d₂ ≤ multiplicity (↑p : ℤ) d₁ + multiplicity (↑p : ℤ) n₂

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]

Premises used: Nat.prime_iff_prime_int, add_comm, multiplicity_mul, Iff.mp, FiniteMultiplicity.multiplicity_le_multiplicity_iff, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₁)
rw : ∀ (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₁

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]

Premises used: add_sub_assoc, Nat.prime_iff_prime_int, add_comm, sub_le_iff_le_add', multiplicity_mul, Rat.divInt_ne_zero_of_ne_zero, Iff.mp, padicValRat.defn, le_sub_iff_add_le, FiniteMultiplicity.multiplicity_le_multiplicity_iff, rfl, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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₁
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₁
⊢ 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]

Premises used: add_sub_assoc, Nat.prime_iff_prime_int, add_comm, sub_le_iff_le_add', multiplicity_mul, Rat.divInt_ne_zero_of_ne_zero, Iff.mp, padicValRat.defn, le_sub_iff_add_le, FiniteMultiplicity.multiplicity_le_multiplicity_iff, rfl, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p q ≤ padicValRat p r
hq : q = 0
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
simpa [hq] using h
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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)

Tactic:
simp [hr]
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ q.num ≠ 0

Tactic:
have hqn : q.num ≠ 0 := Rat.num_ne_zero.2 hq
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
have hqd : (q.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ r.num ≠ 0

Tactic:
have hrn : r.num ≠ 0 := Rat.num_ne_zero.2 hr
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
⊢ Ne (α := ℤ) (↑r.den : ℤ) 0

Tactic:
have hrd : (r.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
⊢ q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)

Tactic:
have hqreq : q + r = (q.num * r.den + q.den * r.num) /. (q.den * r.den) := Rat.add_num_den _ _
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
⊢ q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0

Tactic:
have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
rw : padicValRat p (q.num /. (↑q.den : ℤ))
| padicValRat p q

Tactic:
rw [← q.num_divInt_den]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
conv_lhs : padicValRat p (q.num /. (↑q.den : ℤ)) ≤ padicValRat p (q + r)
⊢ padicValRat p q ≤ padicValRat p (q + r)

Tactic:
conv_lhs => rw [← q.num_divInt_den]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.NumberTheory.Padics.PadicVal.Basic
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
hrd : Ne (α := ℤ) (↑r.den : ℤ) 0
hqreq : q + r = (q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) (↑r.den : ℤ)
hqrd : q.num * (↑r.den : ℤ) + (↑q.den : ℤ) * r.num ≠ 0
rw :
  emultiplicity (α := ℤ) (↑p : ℤ) (↑q.den : ℤ) + emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ)) ≤
    emultiplicity (↑p : ℤ) (q.num * (↑r.den : ℤ) * (↑q.den : ℤ) + (↑q.den : ℤ) * r.num * (↑q.den : ℤ))
⊢ padicValRat p (q.num /. (↑q.den : ℤ)) ≤ padicValRat p (q + r)

Tactic:
rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ←
        emultiplicity_le_emultiplicity_iff, mul_left_comm,
        emultiplicity_mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]

Premises used: add_mul, padicValRat.padicValRat_le_padicValRat_iff, Nat.prime_iff_prime_int, emultiplicity_le_emultiplicity_iff, mul_left_comm, Iff.mp, mul_ne_zero, Fact.out, emultiplicity_mul