Streamline proofs with unfold

Stream: new members

[Andre Knispel]

I have a proof that just unfolds some definitions in a hypothesis and the goal, and then concludes with rw H, refl. Is there some automation that lets me get rid of those unfolds? For some reason, simp at H reduces H to true, which isn't helpful, and simp at the goal fails.

[Kevin Buzzard]

Maybe simp [H] or simp * at * works but without seeing the details it's difficult to guess. If the rewrite is not too serious you might be able to do it in term mode. simp [first_thing_you_unfold, second_thing_you_unfold, H] at *?

[Andre Knispel]

Passing a list to simp makes it a little easier to read, I only tried that with unfold before. What annoys me in particular is that I need simp [has_mem.mem, set.mem] to reduce x ∈ λ y, t to t[y/x] which I would have expected simp to do.

[Kevin Buzzard]

I'm pretty sure you shouldn't have to do simp [has_mem.mem, set.mem] ever but I am not an expert simper.

[Kevin Buzzard]

But it's very hard to diagnose (for me, at least) unless you post fully working code.

[Andre Knispel]

I'm trying to make a self contained example, but when I replace my isomorphism with a general isomorphism, simp suddenly recognizes it and solves the goal right away, probably because it knows about add_equiv.map_zero

[Andre Knispel]

I remember Coq had a tactic to generalize a term to an arbitrary element of its type, is there such a thing for lean?

[Mario Carneiro]

generalize :)

[Andre Knispel]

Hm, sadly that didn't help in this case...

[Reid Barton]

There's probably some more subtle issue blocking simp from applying the lemma, like instance arguments not agreeing or something