autoBoundImplicits3.lean:9:29-9:34: error(lean.unknownIdentifier): Unknown identifier `size₂`

Note: It is not possible to treat `size₂` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.
autoBoundImplicits3.lean:13:24-13:26: error(lean.unknownIdentifier): Unknown identifier `α₃`

Note: It is not possible to treat `α₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
autoBoundImplicits3.lean:13:33-13:38: error(lean.unknownIdentifier): Unknown identifier `size₃`

Note: It is not possible to treat `size₃` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
autoBoundImplicits3.lean:17:30-17:32: error(lean.unknownIdentifier): Unknown identifier `α₄`

Note: It is not possible to treat `α₄` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
autoBoundImplicits3.lean:17:39-17:44: error(lean.unknownIdentifier): Unknown identifier `size₄`

Note: It is not possible to treat `size₄` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.