aesop で bad simp lemma が導入されて証明ができなくなる例

[Seasawher]

aesop はデフォルトでローカルコンテキストにある補題を使って simp をするので、期せずしてよくない simp 補題を導入してしまって証明ができなくなることがある。（これは仕様）

Zulip: aesop with a "bad simp hypothesis" in the context

import Aesop

example (h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp

  -- aesopで証明できない
  fail_if_success aesop

  trivial

[Seasawher]

simp_all と simp at * の違いに関連している