626a.lean:3:42: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly)
626a.lean:8:42: error: failed to synthesize placeholder, type is a unknown (i.e., it is a metavariable) (solution: provide type explicitly)