-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
theorem le_iff_sub_nonneg (a b : ℚ) : a ≤ b ↔ 0 ≤ b - a :=
  numDenCasesOn'' a fun na da ha hared =>
    numDenCasesOn'' b fun nb db hb hbred => by
      rw [Rat.le_iff, sub_def, normalize_eq, ← num_nonneg, ← Int.sub_nonneg]
      dsimp only
      refine ⟨(Int.ediv_nonneg · (Int.natCast_nonneg _)), fun H ↦ ?_⟩
      contrapose! H
      apply Int.ediv_neg' H
      simp only [Int.natCast_pos, Nat.pos_iff_ne_zero]
      exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha)

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 : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db) / ↑((nb * ↑da - na * ↑db).natAbs.gcd (db * da)) < 0

Tactic:
apply Int.ediv_neg' H

Result:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
H : nb * ↑da - na * ↑db < 0
⊢ 0 < ↑((nb * ↑da - na * ↑db).natAbs.gcd (db * 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
⊢ 0 ≤
      { num := nb, den := db, den_nz := hb, reduced := hbred }.num *
          ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den -
        { num := na, den := da, den_nz := ha, reduced := hared }.num *
          ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den ↔
    0 ≤
      {
          num :=
            ({ num := nb, den := db, den_nz := hb, reduced := hbred }.num *
                  ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den -
                { 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 -
                        { num := na, den := da, den_nz := ha, reduced := hared }.num *
                          ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den).natAbs.gcd
                  ({ num := nb, den := db, den_nz := hb, reduced := hbred }.den *
                    { num := na, den := da, den_nz := ha, reduced := hared }.den)),
          den :=
            { num := nb, den := db, den_nz := hb, reduced := hbred }.den *
                { num := na, den := da, den_nz := ha, reduced := hared }.den /
              ({ num := nb, den := db, den_nz := hb, reduced := hbred }.num *
                        ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den -
                      { num := na, den := da, den_nz := ha, reduced := hared }.num *
                        ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den).natAbs.gcd
                ({ num := nb, den := db, den_nz := hb, reduced := hbred }.den *
                  { num := na, den := da, den_nz := ha, reduced := hared }.den),
          den_nz := ⋯, reduced := ⋯ }.num

Tactic:
dsimp only

Result:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
⊢ 0 ≤ nb * ↑da - na * ↑db ↔ 0 ≤ (nb * ↑da - na * ↑db) / ↑((nb * ↑da - na * ↑db).natAbs.gcd (db * 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
⊢ { num := na, den := da, den_nz := ha, reduced := hared } ≤ { num := nb, den := db, den_nz := hb, reduced := hbred } ↔
    0 ≤
      { num := nb, den := db, den_nz := hb, reduced := hbred } -
        { num := na, den := da, den_nz := ha, reduced := hared }

Tactic:
rw [Rat.le_iff, sub_def, normalize_eq, ← num_nonneg, ← Int.sub_nonneg]

Result:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
⊢ 0 ≤
      { num := nb, den := db, den_nz := hb, reduced := hbred }.num *
          ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den -
        { num := na, den := da, den_nz := ha, reduced := hared }.num *
          ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den ↔
    0 ≤
      {
          num :=
            ({ num := nb, den := db, den_nz := hb, reduced := hbred }.num *
                  ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den -
                { 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 -
                        { num := na, den := da, den_nz := ha, reduced := hared }.num *
                          ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den).natAbs.gcd
                  ({ num := nb, den := db, den_nz := hb, reduced := hbred }.den *
                    { num := na, den := da, den_nz := ha, reduced := hared }.den)),
          den :=
            { num := nb, den := db, den_nz := hb, reduced := hbred }.den *
                { num := na, den := da, den_nz := ha, reduced := hared }.den /
              ({ num := nb, den := db, den_nz := hb, reduced := hbred }.num *
                        ↑{ num := na, den := da, den_nz := ha, reduced := hared }.den -
                      { num := na, den := da, den_nz := ha, reduced := hared }.num *
                        ↑{ num := nb, den := db, den_nz := hb, reduced := hbred }.den).natAbs.gcd
                ({ num := nb, den := db, den_nz := hb, reduced := hbred }.den *
                  { num := na, den := da, den_nz := ha, reduced := hared }.den),
          den_nz := ⋯, reduced := ⋯ }.num

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 : 0 ≤ (nb * ↑da - na * ↑db) / ↑((nb * ↑da - na * ↑db).natAbs.gcd (db * da))
⊢ 0 ≤ nb * ↑da - na * ↑db

Tactic:
contrapose! H

Result:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
H : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db) / ↑((nb * ↑da - na * ↑db).natAbs.gcd (db * da)) < 0

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 : nb * ↑da - na * ↑db < 0
⊢ 0 < ↑((nb * ↑da - na * ↑db).natAbs.gcd (db * da))

Tactic:
simp only [Int.natCast_pos, Nat.pos_iff_ne_zero]

Result:
a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : na.natAbs.Coprime da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : nb.natAbs.Coprime db
H : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db).natAbs.gcd (db * da) ≠ 0

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 : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db).natAbs.gcd (db * da) ≠ 0

Tactic:
exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha)

Result:
no goals