Theorem: selectColumns3_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)) (c : CertifiedName (schema (selectColumns3 t cs))),
    Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
      Schema.lookupType (schema (selectColumns3 t cs)) c
Tactic:
intro t cs c
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (schema (selectColumns3 t cs)) c

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (schema (selectColumns3 t cs)) c
Tactic:
unfold schema
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.fromCHeaders cs) c

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.fromCHeaders cs) c
Tactic:
unfold Schema.fromCHeaders
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (schema (selectColumns3 t cs))
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c
Tactic:
simp only [schema] at c
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (Schema.fromCHeaders cs)
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
c : CertifiedName (Schema.fromCHeaders cs)
⊢ Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfFromCHeaders c.snd } =
    Schema.lookupType (Schema.map Sigma.fst cs) c
Tactic:
apply Schema.lookupTypeFromCHeadersUnique
State after:
no goals