Theorem: Schema.hasNameOfFromCHeaders_eq_2 (Table/SchemaFunctions.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
hdr : Header
hpf : HasCol hdr sch
cs : List (CertifiedHeader sch)
nm : η
h : HasName nm (map Sigma.fst cs)
⊢ hasNameOfFromCHeaders (HasName.tl h) = hasNameOfFromCHeaders h
Tactic:
cases sch with
| nil => contradiction
| cons s ss => simp [hasNameOfFromCHeaders]
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
hdr : Header
nm : η
hpf : HasCol hdr []
cs : List (CertifiedHeader [])
h : HasName nm (map Sigma.fst cs)
⊢ hasNameOfFromCHeaders (HasName.tl h) = hasNameOfFromCHeaders h
Tactic:
contradiction
State after:
no goals

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
hdr : Header
nm : η
s : Header
ss : List Header
hpf : HasCol hdr (s :: ss)
cs : List (CertifiedHeader (s :: ss))
h : HasName nm (map Sigma.fst cs)
⊢ hasNameOfFromCHeaders (HasName.tl h) = hasNameOfFromCHeaders h
Tactic:
simp [hasNameOfFromCHeaders]
State after:
no goals