simp only [nrows, orderBy, Schema.length_eq_List_length]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ nrows (orderBy t cmps✝) = nrows t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cmps✝ : List ((κ : Type u) × (Row sch → κ) × (κ → κ → Bool))
⊢ List.length
      (List.mergeSortWith
        (fun r₁ r₂ =>
          match List.find? (fun x => !Prod.snd x.2 (Prod.fst x.2 r₁) (Prod.fst x.2 r₂)) cmps✝ with
          | none => Ordering.lt
          | x => Ordering.gt)
        t.rows) =
    List.length t.rows