Theorem: pivotTable_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)) [inst : DecidableEq (Row (Schema.fromCHeaders cs))]
    (aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))),
    header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Tactic:
intro t cs inst aggs
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ header (pivotTable t cs aggs) = List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Tactic:
simp only [header, Schema.names, Schema.fromCHeaders,
           Schema.append_eq_List_append, Schema.map_eq_List_map]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ List.map Prod.fst (List.append (List.map Sigma.fst cs) (List.map (fun x => x.fst) aggs)) =
    List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
inst : DecidableEq (Row (Schema.fromCHeaders cs))
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ List.map Prod.fst (List.append (List.map Sigma.fst cs) (List.map (fun x => x.fst) aggs)) =
    List.append (List.map (fun x => x.fst.fst) cs) (List.map (fun x => x.fst.fst) aggs)
Tactic:
exact List.map_map_append cs aggs Prod.fst Sigma.fst Sigma.fst
State after:
no goals