Theorem: vcat_spec2 (Table/Proofs.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
⊢ ∀ (t1 t2 : Table sch), nrows (vcat t1 t2) = nrows t1 + nrows t2
Tactic:
intro t1 t2
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ nrows (vcat t1 t2) = nrows t1 + nrows t2

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ nrows (vcat t1 t2) = nrows t1 + nrows t2
Tactic:
simp only [nrows, Schema.length_eq_List_length]
State after:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ List.length (vcat t1 t2).rows = List.length t1.rows + List.length t2.rows

State before:
η : Type u_η
dec_η : DecidableEq η
sch : Schema
t1 t2 : Table sch
⊢ List.length (vcat t1 t2).rows = List.length t1.rows + List.length t2.rows
Tactic:
exact List.length_append t1.rows t2.rows
State after:
no goals