Theorem: select_spec4 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
⊢ ∀ (t : Table sch) (f : Row sch → Fin (nrows t) → Row sch'), nrows (select t f) = nrows t
Tactic:
intros
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ nrows (select t✝ f✝) = nrows t✝

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ nrows (select t✝ f✝) = nrows t✝
Tactic:
simp only [nrows, select, Schema.length_eq_List_length]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ List.length
      (List.map (fun x => f✝ x.snd ((_ : List.length t✝.rows = nrows t✝) ▸ x.fst)) (List.verifiedEnum t✝.rows)) =
    List.length t✝.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
sch' : Schema
t✝ : Table sch
f✝ : Row sch → Fin (nrows t✝) → Row sch'
⊢ List.length
      (List.map (fun x => f✝ x.snd ((_ : List.length t✝.rows = nrows t✝) ▸ x.fst)) (List.verifiedEnum t✝.rows)) =
    List.length t✝.rows
Tactic:
exact Eq.trans (List.length_map _ _) (List.length_verifiedEnum _)
State after:
no goals