isRat_lt_true — Mathlib

Lean4
theorem isRat_lt_true [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] :
    {a b : α} → {na nb : ℤ} → {da db : ℕ} → IsRat a na da → IsRat b nb db → decide (na * db < nb * da) → a < b
  | _, _, _, _, da, db, ⟨_, rfl⟩, ⟨_, rfl⟩, h =>
    by
    have h := Int.cast_strictMono (R := α) <| of_decide_eq_true h
    have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
    have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
    have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
    rw [← mul_assoc, Int.commute_cast] at h
    simp?  at h says simp only [Int.cast_mul, Int.cast_natCast, mul_invOf_cancel_right'] at h
    rwa [Int.commute_cast] at h
Похожие утверждения