a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b < ↑c / ↑d ↔ a * d < c * b
simp only [lt_iff_le_not_le]
case h₁
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

case h₂
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d
apply and_congr
no goals
case h₁
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b
simp [div_num_den, Rat.le_def b_pos d_pos]
case h₂.h
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑c / ↑d ≤ ↑a / ↑b ↔ c * b ≤ a * d
case h₂
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
apply not_congr
no goals
case h₂.h
a✝ b✝ c✝ : ℚ
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑c / ↑d ≤ ↑a / ↑b ↔ c * b ≤ a * d
simp [div_num_den, Rat.le_def d_pos b_pos]