isNNRat_lt_true — Mathlib

Lean4
theorem isNNRat_lt_true [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Nontrivial α] :
    {a b : α} → {na nb : ℕ} → {da db : ℕ} → IsNNRat a na da → IsNNRat b nb db → decide (na * db < nb * da) → a < b
  | _, _, _, _, da, db, ⟨_, rfl⟩, ⟨_, rfl⟩, h =>
    by
    have h := (Nat.cast_lt (α := α)).mpr <| 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, Nat.commute_cast] at h
    simp?  at h says simp only [Nat.cast_mul, mul_invOf_cancel_right'] at h
    rwa [Nat.commute_cast] at h
Похожие утверждения