Theorem: pivotLonger_spec1 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ header (pivotLonger t cs c1 c2) = Schema.names (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
simp only [header, Schema.names]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (Schema.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (Schema.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
rw [Schema.append_eq_List_append]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
have := List.map_append Prod.fst (sch.removeTypedNames cs) [(c1, η), (c2, τ)]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (Schema.removeTypedNames sch cs ++ [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ List.map Prod.fst [(c1, η), (c2, τ)]
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (Schema.removeTypedNames sch cs ++ [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ List.map Prod.fst [(c1, η), (c2, τ)]
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
simp only [HAppend.hAppend, Append.append] at this
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
rw [this]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
τ : Type u_η
t : Table sch
cs : ActionList (Schema.removeTypedName τ) sch
c1 c2 : η
this :
  List.map Prod.fst (List.append (Schema.removeTypedNames sch cs) [(c1, η), (c2, τ)]) =
    List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)])
⊢ List.append (List.map Prod.fst (Schema.removeTypedNames sch cs)) (List.map Prod.fst [(c1, η), (c2, τ)]) =
    List.map Prod.fst (Schema.removeTypedNames sch cs) ++ [c1, c2]
Tactic:
rfl
State after:
no goals