Theorem: Schema.sieve_eq_List_sieve (Table/SchemaFunctions.lean)

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
τ : Type u_1
bs : List Bool
xs✝ xs : List τ
⊢ sieve [] xs = List.sieve [] xs
Tactic:
simp only [sieve, List.sieve]
State after:
no goals

State before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
τ : Type u_1
bs : List Bool
xs : List τ
head✝ : Bool
tail✝ : List Bool
⊢ sieve (head✝ :: tail✝) [] = List.sieve (head✝ :: tail✝) []
Tactic:
simp only [sieve, List.sieve]
State after:
no goals