a b c p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔
    (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
a b c p q : ℚ
⊢ p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den
rw [← @num_den q, ← @num_den p]
a b c p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ p.num * ↑q.den ≤ q.num * ↑p.den
a b c p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔
    (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
conv_rhs => simp only [num_den]
no goals
a b c p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ p.num * ↑q.den ≤ q.num * ↑p.den
exact Rat.le_def (by exact_mod_cast p.pos) (by exact_mod_cast q.pos)
no goals
a b c p q : ℚ
⊢ 0 < ↑p.den
exact_mod_cast p.pos
no goals
a b c p q : ℚ
⊢ 0 < ↑q.den
exact_mod_cast q.pos