F : Type ?u.54964
ι : Type ?u.54967
α : Type ?u.54970
β : Type ?u.54973
K : Type u_1
inst✝ : LinearOrderedField K
r : ℚ
hr : 0 < r
⊢ 0 < ↑r.num / ↑r.den
F : Type ?u.54964
ι : Type ?u.54967
α : Type ?u.54970
β : Type ?u.54973
K : Type u_1
inst✝ : LinearOrderedField K
r : ℚ
hr : 0 < r
⊢ 0 < ↑r
rw [Rat.cast_def]
no goals
F : Type ?u.54964
ι : Type ?u.54967
α : Type ?u.54970
β : Type ?u.54973
K : Type u_1
inst✝ : LinearOrderedField K
r : ℚ
hr : 0 < r
⊢ 0 < ↑r.num / ↑r.den
exact div_pos (Int.cast_pos.2 <| num_pos_iff_pos.2 hr) (Nat.cast_pos.2 r.pos)