Theorem: pivotTable_spec3_aux (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.fromCHeaders ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := { fst := nm, snd := Schema.HasName.hd }.fst,
        snd := Schema.hasNameOfAppend { fst := nm, snd := Schema.HasName.hd }.snd } =
    Schema.lookup sch
      { fst := { fst := nm, snd := Schema.HasName.hd }.fst,
        snd := Schema.hasNameOfFromCHeaders { fst := nm, snd := Schema.HasName.hd }.snd }
Tactic:
simp only [Schema.fromCHeaders, List.map, List.append, Schema.hasNameOfAppend]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.hd } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders Schema.HasName.hd }

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
nm : η
τ : Type u_1
snd✝ : Schema.HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := (nm, τ), snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.hd } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders Schema.HasName.hd }
Tactic:
rw [Schema.lookup_eq_1,
    Schema.hasNameOfFromCHeaders_eq_1,
    Schema.lookup_of_colImpliesName]
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup
      (Schema.append (Schema.fromCHeaders ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := { fst := nm, snd := Schema.HasName.tl a✝ }.fst,
        snd := Schema.hasNameOfAppend { fst := nm, snd := Schema.HasName.tl a✝ }.snd } =
    Schema.lookup sch
      { fst := { fst := nm, snd := Schema.HasName.tl a✝ }.fst,
        snd := Schema.hasNameOfFromCHeaders { fst := nm, snd := Schema.HasName.tl a✝ }.snd }
Tactic:
simp only [Schema.fromCHeaders, List.map, List.append, Schema.hasNameOfAppend]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.tl (Schema.hasNameOfAppend a✝) } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders (Schema.HasName.tl a✝) }

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup
      (Schema.append (Schema.map Sigma.fst ({ fst := fst✝, snd := snd✝ } :: cs)) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.HasName.tl (Schema.hasNameOfAppend a✝) } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders (Schema.HasName.tl a✝) }
Tactic:
rw [Schema.lookup_eq_2,
    Schema.hasNameOfFromCHeaders_eq_2]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup (Schema.append (Schema.map Sigma.fst cs) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.hasNameOfAppend a✝ } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders a✝ }

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
fst✝ : Header
snd✝ : Schema.HasCol fst✝ sch
cs : List (CertifiedHeader sch)
aggs : List ((c' : Header) × (c : CertifiedHeader sch) × (List (Option c.fst.snd) → Option c'.snd))
nm : η
a✝ : Schema.HasName nm (Schema.map Sigma.fst cs)
⊢ Schema.lookup (Schema.append (Schema.map Sigma.fst cs) (Schema.map (fun x => x.fst) aggs))
      { fst := nm, snd := Schema.hasNameOfAppend a✝ } =
    Schema.lookup sch { fst := nm, snd := Schema.hasNameOfFromCHeaders a✝ }
Tactic:
apply pivotTable_spec3_aux cs aggs ⟨nm, _⟩
State after:
no goals