Theorem: buildColumn_spec4 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (f : Row sch → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
      τ
Tactic:
intros t c f
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
f : Row sch → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
    τ

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
f : Row sch → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
    τ
Tactic:
induction sch with
| nil =>
  simp only [Schema.lookupType]
| cons s ss ih =>
  simp only [Schema.lookupType]
  apply ih
  . exact (dropColumn t _)
  . exact f ∘ (Row.cons Cell.emp)
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
t : Table []
f : Row [] → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead [] c τ []) } =
    τ
Tactic:
simp only [Schema.lookupType]
State after:
no goals

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (schema (buildColumn t c f))
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead (s :: ss) c τ []) } =
    τ
Tactic:
simp only [Schema.lookupType]
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
Tactic:
apply ih
State after:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ

State before:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss

case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
. exact (dropColumn t _)
State after:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ

State before:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
. exact f ∘ (Row.cons Cell.emp)
State after:
no goals

State before:
case cons.t
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Table ss
Tactic:
exact (dropColumn t _)
State after:
no goals

State before:
case cons.f
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
s : Header
ss : List Header
ih :
  ∀ (t : Table ss) (f : Row ss → Option τ),
    Schema.lookupType (schema (buildColumn t c f))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
f : Row (s :: ss) → Option τ
⊢ Row ss → Option τ
Tactic:
exact f ∘ (Row.cons Cell.emp)
State after:
no goals