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

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
cn : CertifiedName s
⊢ lookupType s cn = (lookup s cn).snd
Tactic:
cases cn with | mk nm pf =>
induction pf with
| hd =>
  simp only [lookupType]
  rw [lookup_eq_1]
| tl h ih =>
  simp only [lookupType]
  rw [lookup_eq_2]
  apply ih
State after:
no goals

State before:
case mk
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
pf : HasName nm s
⊢ lookupType s { fst := nm, snd := pf } = (lookup s { fst := nm, snd := pf }).snd
Tactic:
induction pf with
| hd =>
  simp only [lookupType]
  rw [lookup_eq_1]
| tl h ih =>
  simp only [lookupType]
  rw [lookup_eq_2]
  apply ih
State after:
no goals

State before:
case mk.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookupType ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    (lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd }).snd
Tactic:
simp only [lookupType]
State after:
case mk.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ τ✝ = (lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd }).snd

State before:
case mk.hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ τ✝ = (lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd }).snd
Tactic:
rw [lookup_eq_1]
State after:
no goals

State before:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h } =
    (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd
Tactic:
simp only [lookupType]
State after:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd

State before:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h }).snd
Tactic:
rw [lookup_eq_2]
State after:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd

State before:
case mk.tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
h : HasName c✝ rs✝
ih : lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
⊢ lookupType rs✝ { fst := c✝, snd := h } = (lookup rs✝ { fst := c✝, snd := h }).snd
Tactic:
apply ih
State after:
no goals