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

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs)
      { fst := { fst := nm, snd := HasName.hd }.fst,
        snd := hasNameOfFromCHeaders { fst := nm, snd := HasName.hd }.snd } =
    lookupType (fromCHeaders ({ fst := (nm, τ), snd := HasCol.hd } :: cs)) { fst := nm, snd := HasName.hd }
Tactic:
simp only [lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := hasNameOfFromCHeaders HasName.hd } = τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := hasNameOfFromCHeaders HasName.hd } = τ
Tactic:
simp only [hasNameOfFromCHeaders_eq_1]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := colImpliesName HasCol.hd } = τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := colImpliesName HasCol.hd } = τ
Tactic:
rw [@colImpliesName_eq_1 η hs (nm, τ)]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := HasName.hd } = τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := HasName.hd } = τ
Tactic:
simp only [lookupType]
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs)
      { fst := { fst := ch_nm, snd := HasName.hd }.fst,
        snd := hasNameOfFromCHeaders { fst := ch_nm, snd := HasName.hd }.snd } =
    lookupType (fromCHeaders ({ fst := (ch_nm, ch_τ), snd := HasCol.tl h } :: cs)) { fst := ch_nm, snd := HasName.hd }
Tactic:
simp only [lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := hasNameOfFromCHeaders HasName.hd } = ch_τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := hasNameOfFromCHeaders HasName.hd } = ch_τ
Tactic:
simp only [hasNameOfFromCHeaders_eq_1]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := colImpliesName (HasCol.tl h) } = ch_τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := colImpliesName (HasCol.tl h) } = ch_τ
Tactic:
rw [@colImpliesName_eq_2 η hs (nm, τ) (ch_nm, ch_τ) h]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := HasName.tl (colImpliesName h) } = ch_τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := HasName.tl (colImpliesName h) } = ch_τ
Tactic:
simp only [lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType hs { fst := ch_nm, snd := colImpliesName h } = ch_τ

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType hs { fst := ch_nm, snd := colImpliesName h } = ch_τ
Tactic:
apply lookupType_of_colImpliesName
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs)
      { fst := { fst := s_nm, snd := HasName.tl hn }.fst,
        snd := hasNameOfFromCHeaders { fst := s_nm, snd := HasName.tl hn }.snd } =
    lookupType (fromCHeaders ({ fst := fst✝, snd := pf } :: cs)) { fst := s_nm, snd := HasName.tl hn }
Tactic:
simp only [lookupType]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders (HasName.tl hn) } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders (HasName.tl hn) } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }
Tactic:
simp only [hasNameOfFromCHeaders_eq_2]
State after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders hn } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders hn } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }
Tactic:
exact lookupTypeFromCHeadersUnique cs ⟨s_nm, hn⟩
State after:
no goals