simp only [nrows, groupBy, Schema.length_eq_List_length]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ nrows (groupBy t key proj agg) = List.length (List.unique (List.map key t.rows))
η : Type u_η
dec_η : DecidableEq η
sch : Schema
η' : Type u_1
inst✝¹ : DecidableEq η'
sch' : Schema
κ : Type u_3
ν : Type u_4
inst✝ : DecidableEq κ
t : Table sch
key : Row sch → κ
proj : Row sch → ν
agg : κ → List ν → Row sch'
⊢ List.length
      (List.map (fun klv => agg klv.fst klv.snd) (List.groupByKey (List.map (fun r => (key r, proj r)) t.rows))) =
    List.length (List.unique (List.map key t.rows))