no goals
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)
simpa [hq] using h
no goals
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)
simp [hr]
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)
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 := Rat.num_ne_zero_of_ne_zero hq
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 : ↑q.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
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 : (q.den : ℤ) ≠ 0 := by exact_mod_cast Rat.den_nz _
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
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 : ↑q.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hrn : r.num ≠ 0 := Rat.num_ne_zero_of_ne_zero hr
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hrd : (r.den : ℤ) ≠ 0 := by exact_mod_cast Rat.den_nz _
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
⊢ padicValRat p q ≤ padicValRat p (q + r)
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hqreq : q + r = (q.num * r.den + q.den * r.num) /. (q.den * r.den) := Rat.add_num_den _ _
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
⊢ padicValRat p q ≤ padicValRat p (q + r)
have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p q ≤ padicValRat p (q + r)
conv_lhs => rw [← @Rat.num_den q]
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ padicValRat p (q.num /. ↑q.den) ≤ padicValRat p (q + r)
rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ←
  multiplicity_le_multiplicity_iff, mul_left_comm,
  multiplicity.mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
rw [← @Rat.num_den q, ← @Rat.num_den r, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
  multiplicity_le_multiplicity_iff] at h
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity (↑p) (q.num * ↑r.den * ↑q.den + ↑q.den * r.num * ↑q.den)
calc
  _ ≤
      min (multiplicity (↑p) (q.num * r.den * q.den))
        (multiplicity (↑p) (↑q.den * r.num * ↑q.den)) :=
    le_min
      (by rw [@multiplicity.mul _ _ _ _ (_ * _) _ (Nat.prime_iff_prime_int.1 hp.1), add_comm])
      (by
        rw [mul_assoc,
            @multiplicity.mul _ _ _ _ (q.den : ℤ) (_ * _)
              (Nat.prime_iff_prime_int.1 hp.1)]
        exact add_le_add_left h _)
  _ ≤ _ := min_le_multiplicity_add
no goals
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
⊢ ↑q.den ≠ 0
exact_mod_cast Rat.den_nz _
no goals
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 : ↑q.den ≠ 0
hrn : r.num ≠ 0
⊢ ↑r.den ≠ 0
exact_mod_cast Rat.den_nz _
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (q.num * ↑r.den * ↑q.den)
rw [@multiplicity.mul _ _ _ _ (_ * _) _ (Nat.prime_iff_prime_int.1 hp.1), add_comm]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity ↑p ↑q.den + multiplicity (↑p) (r.num * ↑q.den)
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (↑q.den * r.num * ↑q.den)
rw [mul_assoc,
    @multiplicity.mul _ _ _ _ (q.den : ℤ) (_ * _)
      (Nat.prime_iff_prime_int.1 hp.1)]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h✝ : ∀ (n : ℕ), ↑p ^ n ∣ q.num * ↑r.den → ↑p ^ n ∣ r.num * ↑q.den
h : multiplicity (↑p) (q.num * ↑r.den) ≤ multiplicity (↑p) (r.num * ↑q.den)
hq : ¬q = 0
hr : ¬r = 0
hqn : q.num ≠ 0
hqd : ↑q.den ≠ 0
hrn : r.num ≠ 0
hrd : ↑r.den ≠ 0
hqreq : q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
hqrd : q.num * ↑r.den + ↑q.den * r.num ≠ 0
⊢ multiplicity ↑p ↑q.den + multiplicity (↑p) (q.num * ↑r.den) ≤
    multiplicity ↑p ↑q.den + multiplicity (↑p) (r.num * ↑q.den)
exact add_le_add_left h _