simp, tauto

Stream: general

[Sean Leather]

So close and yet so far:

error: done tactic failed, there are unsolved goals
state:
...
a : b₁ = b₂
⊢ b₂ = b₁

[Kevin Buzzard]

eq.symm is not a good simp lemma :-)

[Simon Hudon]

What is the goal before you call tauto?

[Reid Barton]

I made a version of tauto that calls cc (which is how I discovered that cc bug I mentioned here a while ago)

[Reid Barton]

instead of done

[Sean Leather]

The goal is rather complicated (but seems like it should be automatically solvable), and I don't have it around anymore. The proof doesn't involve eq.symm. But I've noticed this same pattern a few times when trying tauto. Here's another example that I just tried. It seems that tauto can't solve this (which is just or.inr)?

⊢ s ∈ tl → s = hd ∨ s ∈ tl