Theorem: addColumn_spec3 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
⊢ ∀ (t : Table sch) (c : η) (vs : List (Option τ)),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead sch c τ []) } =
      τ
Tactic:
intros t c vs
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
t : Table sch
c : η
vs : List (Option τ)
⊢ Schema.lookupType (schema (addColumn t c vs))
      { 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 : η
vs : List (Option τ)
⊢ Schema.lookupType (schema (addColumn t c vs))
      { 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 (dropColumn t _)
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u
inst✝ : DecidableEq τ
c : η
vs : List (Option τ)
t : Table []
⊢ Schema.lookupType (schema (addColumn t c vs))
      { 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 : η
vs : List (Option τ)
s : Header
ss : List Header
ih :
  ∀ (t : Table ss),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
⊢ Schema.lookupType (schema (addColumn t c vs))
      { 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 : η
vs : List (Option τ)
s : Header
ss : List Header
ih :
  ∀ (t : Table ss),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
⊢ 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 : η
vs : List (Option τ)
s : Header
ss : List Header
ih :
  ∀ (t : Table ss),
    Schema.lookupType (schema (addColumn t c vs))
        { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
      τ
t : Table (s :: ss)
⊢ Schema.lookupType (Schema.append ss [(c, τ)])
      { fst := c, snd := Schema.colImpliesName (Schema.hasAppendedHead ss c τ []) } =
    τ
Tactic:
apply ih (dropColumn t _)
State after:
no goals