Theorem: selectColumns2_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t : Table sch) (ns : List (Fin (ncols t))) (i : Nat) (hi : i < List.length ns),
    List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
      List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Tactic:
intro t ns i hi
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (header (selectColumns2 t ns)) { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (header t) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Tactic:
simp only [header]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch) (finHeaderLengthOfFinNcols t (List.get ns { val := i, isLt := hi }))
Tactic:
simp only [finHeaderLengthOfFinNcols]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch)
      { val := (List.get ns { val := i, isLt := hi }).val,
        isLt := (_ : (List.get ns { val := i, isLt := hi }).val < List.length (header t)) }

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t : Table sch
ns : List (Fin (ncols t))
i : Nat
hi : i < List.length ns
⊢ List.get (Schema.names (Schema.nths sch ns))
      { val := i, isLt := (_ : i < List.length (header (selectColumns2 t ns))) } =
    List.get (Schema.names sch)
      { val := (List.get ns { val := i, isLt := hi }).val,
        isLt := (_ : (List.get ns { val := i, isLt := hi }).val < List.length (header t)) }
Tactic:
apply Schema.get_map_nths_eq_get_get
State after:
no goals