Theorem: Schema.lookup_of_colImpliesName (Table/Schema.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
ss : List Header
⊢ lookup ((nm, τ) :: ss) { fst := nm, snd := colImpliesName HasCol.hd } = (nm, τ)
Tactic:
rw [colImpliesName_eq_1 (sch' := ss) (hdr := (nm, τ)),
    lookup_eq_1]
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup (head✝ :: ss) { fst := nm, snd := colImpliesName (HasCol.tl h) } = (nm, τ)
Tactic:
rw [colImpliesName_eq_2, lookup_eq_2]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup ss { fst := nm, snd := colImpliesName h } = (nm, τ)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
head✝ : Header
ss : List Header
h : HasCol (nm, τ) ss
⊢ lookup ss { fst := nm, snd := colImpliesName h } = (nm, τ)
Tactic:
apply lookup_of_colImpliesName
State after:
no goals