apply congrArg
η : 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.map (Prod.fst ∘ fun r => (key r, proj r)) = List.map key
case h
η : 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'
⊢ (Prod.fst ∘ fun r => (key r, proj r)) = key