[GOAL]
α : Type u_1
p q : ℚ≥0
h : q ≤ p
⊢ ↑q ≤ ↑p - 0
[PROOFSTEP]
rwa [sub_zero]
[GOAL]
α : Type u_1
p q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
p q : ℚ≥0
n : ℕ
⊢ ↑(toNNRat ↑n) = ↑↑n
[PROOFSTEP]
simp only [Nat.cast_nonneg, Rat.coe_toNNRat]
[GOAL]
α : Type u_1
p q : ℚ≥0
n : ℕ
⊢ ↑n = ↑↑n
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ toNNRat (∑ a in s, f a) = ∑ a in s, toNNRat (f a)
[PROOFSTEP]
rw [← coe_inj, coe_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(toNNRat (f a))
[PROOFSTEP]
exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(toNNRat (f x))
[PROOFSTEP]
rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ toNNRat (∏ a in s, f a) = ∏ a in s, toNNRat (f a)
[PROOFSTEP]
rw [← coe_inj, coe_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∏ i in s, f i = ∏ a in s, ↑(toNNRat (f a))
[PROOFSTEP]
exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(toNNRat (f x))
[PROOFSTEP]
rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
p q : ℚ
⊢ 0 < toNNRat q ↔ 0 < q
[PROOFSTEP]
simp [toNNRat, ← coe_lt_coe]
[GOAL]
p q : ℚ
⊢ toNNRat q = 0 ↔ q ≤ 0
[PROOFSTEP]
simpa [-toNNRat_pos] using (@toNNRat_pos q).not
[GOAL]
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat q ≤ toNNRat p ↔ q ≤ p
[PROOFSTEP]
simp [← coe_le_coe, toNNRat, hp]
[GOAL]
p q : ℚ
⊢ toNNRat q < toNNRat p ↔ q < p ∧ 0 < p
[PROOFSTEP]
simp [← coe_lt_coe, toNNRat, lt_irrefl]
[GOAL]
p q : ℚ
hq : 0 ≤ q
hp : 0 ≤ p
⊢ ↑(toNNRat (q + p)) = ↑(toNNRat q + toNNRat p)
[PROOFSTEP]
simp [toNNRat, hq, hp, add_nonneg]
[GOAL]
p q✝ : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ toNNRat p ↔ ↑q ≤ p
[PROOFSTEP]
rw [← coe_le_coe, Rat.coe_toNNRat p hp]
[GOAL]
p q✝ : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ toNNRat p ↔ ↑q ≤ p
[PROOFSTEP]
simp only [(hp.trans_le q.coe_nonneg).not_le, toNNRat_eq_zero.2 hp.le, hq.not_le]
[GOAL]
p✝ q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ toNNRat q < p ↔ q < ↑p
[PROOFSTEP]
rw [← coe_lt_coe, Rat.coe_toNNRat q hq]
[GOAL]
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
cases' le_total 0 q with hq hq
[GOAL]
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
ext
[GOAL]
case inl.a.num
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (↑(toNNRat (p * q))).num = (↑(toNNRat p * toNNRat q)).num
[PROOFSTEP]
simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]
[GOAL]
case inl.a.den
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (↑(toNNRat (p * q))).den = (↑(toNNRat p * toNNRat q)).den
[PROOFSTEP]
simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]
[GOAL]
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
[GOAL]
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]
[GOAL]
p q✝ q : ℚ
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
obtain hq | hq := le_total q 0
[GOAL]
case inl
p q✝ q : ℚ
hq : q ≤ 0
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
[GOAL]
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
nth_rw 1 [← Rat.coe_toNNRat q hq]
[GOAL]
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat (↑(toNNRat q))⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
rw [← coe_inv, toNNRat_coe]
[GOAL]
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat (p / q) = toNNRat p / toNNRat q
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
[GOAL]
p q : ℚ
hq : 0 ≤ q
⊢ toNNRat (p / q) = toNNRat p / toNNRat q
[PROOFSTEP]
rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
[GOAL]
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ p = q
[PROOFSTEP]
ext
[GOAL]
case a.num
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).num = (↑q).num
[PROOFSTEP]
apply (Int.natAbs_inj_of_nonneg_of_nonneg _ _).1 hn
[GOAL]
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑p).num
p q : ℚ≥0 hn : num p = num q hd : den p = den q ⊢ 0 ≤ (↑q).num
[PROOFSTEP]
exact Rat.num_nonneg_iff_zero_le.2 p.2
[GOAL]
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑q).num
[PROOFSTEP]
exact Rat.num_nonneg_iff_zero_le.2 q.2
[GOAL]
case a.den
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).den = (↑q).den
[PROOFSTEP]
exact hd
[GOAL]
p q : ℚ≥0
⊢ p = q → num p = num q ∧ den p = den q
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℚ≥0
⊢ num p = num p ∧ den p = den p
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
p q✝ q : ℚ≥0
⊢ ↑(num q) / ↑(den q) = q
[PROOFSTEP]
ext1
[GOAL]
case a
p q✝ q : ℚ≥0
⊢ ↑(↑(num q) / ↑(den q)) = ↑q
[PROOFSTEP]
rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_ofNat,
  Int.natAbs_of_nonneg (Rat.num_nonneg_iff_zero_le.2 q.prop)]
[GOAL]
case a
p q✝ q : ℚ≥0
⊢ ↑(↑q).num / ↑(den q) = ↑q
[PROOFSTEP]
exact Rat.num_div_den q
[GOAL]
p q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α q
[PROOFSTEP]
rw [← num_div_den q]
[GOAL]
p q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α (↑(num q) / ↑(den q))
[PROOFSTEP]
apply h
