Theorem: selectColumns2_spec3 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ {sch : Schema} (t : Table sch) (ns : List (Fin (ncols t))) (c : CertifiedName (schema (selectColumns2 t ns))),
    Schema.lookupType (schema (selectColumns2 t ns)) c =
      Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Tactic:
intro sch t ns c
State after:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (schema (selectColumns2 t ns))
⊢ Schema.lookupType (schema (selectColumns2 t ns)) c =
    Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }

State before:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (schema (selectColumns2 t ns))
⊢ Schema.lookupType (schema (selectColumns2 t ns)) c =
    Schema.lookupType (schema t) { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Tactic:
unfold schema at *
State after:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (Schema.nths sch ns)
⊢ Schema.lookupType (Schema.nths sch ns) c =
    Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }

State before:
η : Type u_η
dec_η : DecidableEq η
sch✝ : Schema
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
c : CertifiedName (Schema.nths sch ns)
⊢ Schema.lookupType (Schema.nths sch ns) c =
    Schema.lookupType sch { fst := c.fst, snd := Schema.hasNameOfNthsHasName c.snd }
Tactic:
apply Schema.lookupType_nths_eq_lookupType
State after:
no goals