Theorem: update_spec4 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (subsch : RetypedSubschema sch) (t : Table sch) (f : Row sch → Row (RetypedSubschema.toSchema subsch)),
    nrows (update subsch t f) = nrows t
Tactic:
intros
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ nrows (update subsch✝ t✝ f✝) = nrows t✝

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ nrows (update subsch✝ t✝ f✝) = nrows t✝
Tactic:
simp only [nrows, update, Schema.length_eq_List_length]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ List.length (List.map (fun r => update.updateCells r (f✝ r)) t✝.rows) = List.length t✝.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
subsch✝ : RetypedSubschema sch
t✝ : Table sch
f✝ : Row sch → Row (RetypedSubschema.toSchema subsch✝)
⊢ List.length (List.map (fun r => update.updateCells r (f✝ r)) t✝.rows) = List.length t✝.rows
Tactic:
apply List.length_map
State after:
no goals