-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem lt_iff (a b : ℚ) : a < b ↔ a.num * b.den < b.num * a.den :=
  numDenCasesOn'' a fun na da ha hared =>
    numDenCasesOn'' b fun nb db hb hbred => by
      show Rat.blt _ _ = true ↔ _
      suffices
        (na < 0 ∧ 0 ≤ nb ∨ if na = 0 then 0 < nb else (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * da) ↔
        na * db < nb * da by simpa [Rat.blt]
      split_ifs with h
      · suffices 0 < nb ↔ 0 < nb * da by simpa [h]
        refine ⟨(Int.mul_pos · (by omega)), ?_⟩
        contrapose!
        exact (Int.mul_nonpos_of_nonpos_of_nonneg · (by omega))
      · constructor
        · refine (·.elim ?_ And.right)
          rintro ⟨hna, nb0⟩
          apply (Int.mul_neg_of_neg_of_pos hna _).trans_le (Int.mul_nonneg nb0 _) <;> omega
        · intro h
          suffices na < 0 ∧ 0 ≤ nb ∨ na ≤ 0 ∨ 0 < nb by simpa [h]
          contrapose! h
          apply (Int.mul_nonpos_of_nonpos_of_nonneg _ _).trans (Int.mul_nonneg _ _) <;> omega

Proof state:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
⊢ { num := na, den := da, den_nz := ha, reduced := hared }.blt
        { num := nb, den := db, den_nz := hb, reduced := hbred } =
      true ↔
    { num := na, den := da, den_nz := ha, reduced := hared }.num *
        ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den <
      { num := nb, den := db, den_nz := hb, reduced := hbred }.num *
        ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den

Tactic:
suffices
  (na < 0 ∧ 0 ≤ nb ∨ if na = 0 then 0 < nb else (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * da) ↔
  na * db < nb * da by simpa [Rat.blt]

Result:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
⊢ (na < 0 ∧ 0 ≤ nb ∨ if na = 0 then 0 < nb else (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da) ↔ na * ↑db < nb * ↑da

Proof state:
case neg.mp
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
h : ¬na = 0
x✝ : na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da
⊢ na < 0 ∧ 0 ≤ nb → na * ↑db < nb * ↑da

Tactic:
rintro ⟨hna, nb0⟩

Result:
case neg.mp.intro
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
h : ¬na = 0
x✝ : na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da
hna : na < 0
nb0 : 0 ≤ nb
⊢ na * ↑db < nb * ↑da

Proof state:
case pos
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
h : na = 0
⊢ 0 < nb * ↑da → 0 < nb

Tactic:
contrapose!

Result:
case pos
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
h : na = 0
⊢ nb ≤ 0 → nb * ↑da ≤ 0

Proof state:
case neg.mpr
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
h✝ : ¬na = 0
h : na * ↑db < nb * ↑da
⊢ na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da

Tactic:
suffices na < 0 ∧ 0 ≤ nb ∨ na ≤ 0 ∨ 0 < nb by simpa [h]

Result:
case neg.mpr
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
h✝ : ¬na = 0
h : na * ↑db < nb * ↑da
⊢ na < 0 ∧ 0 ≤ nb ∨ na ≤ 0 ∨ 0 < nb