Reduction of goal

Stream: general

[Jasmin Blanchette]

Suppose I have a goal like ((Ss_fst, Ss_snd).fst, (Ss_fst, Ss_snd).snd) ⇒ ((Ss'_fst, Ss'_snd).fst, (Ss'_fst, Ss'_snd).snd) and I just want to automatically reduce it, i.e., beta-delta-etc.-reduce it. I have the impression that Lean (and Coq) discourage that, preferring a lazy approach, but sometimes it seems useful, and in a teaching context I can see many uses for that. Going outside the goal, writing

#reduce (∀Ss_fst Ss_snd Ss'_fst Ss'_snd, ((Ss_fst, Ss_snd).fst, (Ss_fst, Ss_snd).snd) ⇒ ((Ss'_fst, Ss'_snd).fst, (Ss'_fst, Ss'_snd).snd))

and then doing a show with the result seems like a roundabout solution. Is there a more direct approach? If not, why not?

[Johan Commelin]

dsimp

[Jasmin Blanchette]

Ah!! That's what dsimp is for! I think the simp part mislead me there. Thanks a lot. :)

[Kevin Buzzard]

Maybe simp only [] would work too