-- 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
h : na = 0
x✝ : 0 < nb
⊢ 0 < ↑da

Tactic:
omega

Result:
no goals

Proof state:
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

Tactic:
apply (Int.mul_neg_of_neg_of_pos hna _).trans_le (Int.mul_nonneg nb0 _) <;> omega

Result:
no goals

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
⊢ na * ↑db < nb * ↑da → na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da

Tactic:
intro 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) ∧ na * ↑db < nb * ↑da

Proof state:
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
this : 0 < nb ↔ 0 < nb * ↑da
⊢ na < 0 ∧ 0 ≤ nb ∨ 0 < nb ↔ na * ↑db < nb * ↑da

Tactic:
simpa [h]

Result:
no goals

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

Tactic:
contrapose! 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 < 0 → nb < 0) ∧ 0 < na ∧ nb ≤ 0
⊢ nb * ↑da ≤ na * ↑db

Proof state:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
this : (na < 0 ∧ 0 ≤ nb ∨ if na = 0 then 0 < nb else (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da) ↔ na * ↑db < nb * ↑da
⊢ { 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:
simpa [Rat.blt]

Result:
no goals

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 } < { num := nb, den := db, den_nz := hb, reduced := hbred } ↔
    { 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:
show Rat.blt _ _ = true ↔ _

Result:
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

Proof state:
case neg
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
⊢ na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da ↔ na * ↑db < nb * ↑da

Tactic:
constructor

Result:
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
⊢ na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da → na * ↑db < nb * ↑da

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
⊢ na * ↑db < nb * ↑da → na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da

Proof state:
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

Tactic:
split_ifs with h

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
⊢ na < 0 ∧ 0 ≤ nb ∨ 0 < nb ↔ na * ↑db < nb * ↑da

case neg
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
⊢ na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da ↔ na * ↑db < nb * ↑da

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 < 0 → nb < 0) ∧ 0 < na ∧ nb ≤ 0
⊢ nb * ↑da ≤ na * ↑db

Tactic:
apply (Int.mul_nonpos_of_nonpos_of_nonneg _ _).trans (Int.mul_nonneg _ _) <;> omega

Result:
no goals

Proof state:
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
this : na < 0 ∧ 0 ≤ nb ∨ na ≤ 0 ∨ 0 < nb
⊢ na < 0 ∧ 0 ≤ nb ∨ (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * ↑da

Tactic:
simpa [h]

Result:
no goals

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
⊢ na < 0 ∧ 0 ≤ nb ∨ 0 < nb ↔ na * ↑db < nb * ↑da

Tactic:
suffices 0 < nb ↔ 0 < nb * da by simpa [h]

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
⊢ 0 < nb ↔ 0 < nb * ↑da

Proof state:
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✝ : nb ≤ 0
⊢ 0 ≤ ↑da

Tactic:
omega

Result:
no goals