Mathlib 由来の警告があるので、警告があったらエラーにするのを一時的にやめる

Mathlib 由来の警告があるので、警告があったらエラーにするのを一時的にやめる #1022