p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ p ≠ 1 ∧ 0 < q.den
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ (multiplicity p q.den).Dom
rw [← finite_iff_dom, finite_nat_iff]
no goals
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ p ≠ 1 ∧ 0 < q.den
exact ⟨hp, q.pos⟩
case hc
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ p ≠ 1 ∧ 0 < q.den

p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ q.num ≠ 0

p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ q.num ≠ 0

p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ q.num ≠ 0
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ padicValRat p q =
    ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) -
      ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom))
rw [padicValRat, padicValInt.of_ne_one_ne_zero hp, padicValNat, dif_pos]
no goals
case hc
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ p ≠ 1 ∧ 0 < q.den
exact ⟨hp, q.pos⟩
no goals
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ q.num ≠ 0
exact Rat.num_ne_zero_of_ne_zero hq