a b c p q : ℚ
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q ↔ p.num * ↑q.den < q.num * ↑p.den
a b c p q : ℚ
⊢ p < q ↔ p.num * ↑q.den < q.num * ↑p.den
rw [lt_iff_le_and_ne, Rat.le_def']
no goals
a b c p q : ℚ
⊢ p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
exact not_iff_not.mpr eq_iff_mul_eq_mul
case mp
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
⊢ p.num * ↑q.den < q.num * ↑p.den

case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den < q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q ↔ p.num * ↑q.den < q.num * ↑p.den
constructor <;> intro h
no goals
case mp
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
⊢ p.num * ↑q.den < q.num * ↑p.den
exact lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩
case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den < q.num * ↑p.den
tmp : p.num * ↑q.den ≤ q.num * ↑p.den ∧ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den < q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
have tmp := lt_iff_le_and_ne.mp h
no goals
case mpr
a b c p q : ℚ
this : p ≠ q ↔ p.num * ↑q.den ≠ q.num * ↑p.den
h : p.num * ↑q.den < q.num * ↑p.den
tmp : p.num * ↑q.den ≤ q.num * ↑p.den ∧ p.num * ↑q.den ≠ q.num * ↑p.den
⊢ p.num * ↑q.den ≤ q.num * ↑p.den ∧ p ≠ q
exact ⟨tmp.left, this.mpr tmp.right⟩