Theorem: flatten_spec1 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : ActionList Schema.flattenList sch), header (flatten t cs) = header t
Tactic:
intros t cs
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ header (flatten t cs) = header t

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ header (flatten t cs) = header t
Tactic:
simp only [flatten, header, Schema.names]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ List.map Prod.fst (Schema.flattenLists sch cs) = List.map Prod.fst sch

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : ActionList Schema.flattenList sch
⊢ List.map Prod.fst (Schema.flattenLists sch cs) = List.map Prod.fst sch
Tactic:
induction cs with
| nil => rfl
| cons c cs ih =>
  rw [ih]
  simp only [Schema.flattenList]
  apply Schema.retypeColumn_preserves_names
  exact Table.mk []
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenLists schema✝ ActionList.nil) = List.map Prod.fst schema✝
Tactic:
rfl
State after:
no goals

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenLists schema✝ (ActionList.cons c cs)) = List.map Prod.fst schema✝
Tactic:
rw [ih]
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenList schema✝ c) = List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.flattenList schema✝ c) = List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Tactic:
simp only [Schema.flattenList]
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.retypeColumn schema✝ (Schema.colImpliesName c.snd.snd) c.snd.fst) =
    List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ List.map Prod.fst (Schema.retypeColumn schema✝ (Schema.colImpliesName c.snd.snd) c.snd.fst) =
    List.map Prod.fst schema✝

case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Tactic:
apply Schema.retypeColumn_preserves_names
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch schema✝ : Schema
c : (c : η) × (τ : Type u_1) × Schema.HasCol (c, List τ) schema✝
cs : ActionList Schema.flattenList (Schema.flattenList schema✝ c)
ih :
  Table (Schema.flattenList schema✝ c) →
    List.map Prod.fst (Schema.flattenLists (Schema.flattenList schema✝ c) cs) =
      List.map Prod.fst (Schema.flattenList schema✝ c)
t : Table schema✝
⊢ Table (Schema.flattenList schema✝ c)
Tactic:
exact Table.mk []
State after:
no goals