-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem mul {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) :
    padicValRat p (q * r) = padicValRat p q + padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

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]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
⊢ r.num /. ↑r.den ≠ 0

Tactic:
rwa [Rat.num_divInt_den]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) (q.num * r.num)) - ↑(multiplicity (↑p) (↑q.den * ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

Tactic:
rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) q.num) + ↑(multiplicity (↑p) r.num) - (↑(multiplicity ↑p ↑q.den) + ↑(multiplicity ↑p ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (↑q.den * ↑r.den)

p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
⊢ q.num /. ↑q.den ≠ 0

Tactic:
rwa [Rat.num_divInt_den]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) (q.num * r.num)) - ↑(multiplicity (↑p) (↑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']

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) (q.num * r.num)) - ↑(multiplicity (↑p) (↑q.den * ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

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

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) (q.num * r.num)) - ↑(multiplicity (↑p) (↑q.den * ↑r.den)) = padicValRat p q + padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
⊢ q * r = q.num * r.num /. (↑q.den * ↑r.den)

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

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Tactic:
have hq' : q.num /. q.den ≠ 0 := by rwa [Rat.num_divInt_den]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Tactic:
have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_divInt_den]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑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

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (↑q.den * ↑r.den)

Tactic:
simp [finite_int_prime_iff]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ ↑(multiplicity (↑p) q.num) + ↑(multiplicity (↑p) r.num) - (↑(multiplicity ↑p ↑q.den) + ↑(multiplicity ↑p ↑r.den)) =
    ↑(multiplicity (↑p) q.num) - ↑(multiplicity ↑p ↑q.den) + (↑(multiplicity (↑p) r.num) - ↑(multiplicity ↑p ↑r.den))

Tactic:
ring

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑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

Tactic:
have hp' : Prime (p : ℤ) := Nat.prime_iff_prime_int.1 hp.1

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ padicValRat p (q * r) = padicValRat p q + padicValRat p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q ≠ 0
hr : r ≠ 0
this : q * r = q.num * r.num /. (↑q.den * ↑r.den)
hq' : q.num /. ↑q.den ≠ 0
hr' : r.num /. ↑r.den ≠ 0
hp' : _root_.Prime ↑p
⊢ FiniteMultiplicity (↑p) (q.num * r.num)

Tactic:
simp [finite_int_prime_iff, hq, hr]

Result:
no goals