Theorem: selectColumns3_spec1 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (cs : List (CertifiedHeader sch)), header (selectColumns3 t cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
intros t cs
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ header (selectColumns3 t cs) = List.map (Prod.fst ∘ Sigma.fst) cs

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ header (selectColumns3 t cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
simp only [header, selectColumns3, Schema.names]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
cs : List (CertifiedHeader sch)
⊢ List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
induction cs with
| nil => simp only [Schema.pick, List.map]
| cons c cs ih =>
  simp only [Schema.pick, List.map, List.cons.injEq]
  apply And.intro
  . simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
  . exact ih
State after:
no goals

State before:
case nil
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
⊢ List.map Prod.fst (Schema.fromCHeaders []) = List.map (Prod.fst ∘ Sigma.fst) []
Tactic:
simp only [Schema.pick, List.map]
State after:
no goals

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.fromCHeaders (c :: cs)) = List.map (Prod.fst ∘ Sigma.fst) (c :: cs)
Tactic:
simp only [Schema.pick, List.map, List.cons.injEq]
State after:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c ∧
    List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs

State before:
case cons
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c ∧
    List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
apply And.intro
State after:
case cons.left
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c

case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs

State before:
case cons.left
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c

case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
. simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
State after:
case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs

State before:
case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
. exact ih
State after:
no goals

State before:
case cons.left
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ c.fst.fst = (Prod.fst ∘ Sigma.fst) c
Tactic:
simp only [Function.comp, Schema.lookup_fst_eq_nm, CertifiedName.val]
State after:
no goals

State before:
case cons.right
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
c : CertifiedHeader sch
cs : List (CertifiedHeader sch)
ih : List.map Prod.fst (Schema.fromCHeaders cs) = List.map (Prod.fst ∘ Sigma.fst) cs
⊢ List.map Prod.fst (Schema.map Sigma.fst cs) = List.map (Prod.fst ∘ Sigma.fst) cs
Tactic:
exact ih
State after:
no goals