simp only [Function.comp, getValue]
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => getValue r "key") ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
      (List.groupByKey (List.map (fun r => (getValue r c, r)) t.rows)))
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_1
inst : DecidableEq τ
t : Table sch
c : η
hc : Schema.HasCol (c, τ) sch
⊢ List.NoDuplicates
    (List.map
      ((fun r => Cell.toOption (Row.getCell r Schema.HasCol.hd)) ∘ fun klv =>
        Row.cons (Cell.fromOption (Option.map ULift.up klv.fst)) (Row.cons (Cell.val { rows := klv.snd }) Row.nil))
      (List.groupByKey (List.map (fun r => (Cell.toOption (Row.getCell r hc), r)) t.rows)))