Self help during proofs

Stream: new members

[Trevor Fancher]

During a proof, one of my hypothesis has a ⟨R, hR⟩.val term. I don't know what that means or how to work with it. While specific help on this would be nice, I am looking for more general help on how I could find out during a proof (in tactic mode) on how I could figure out what such things mean and how to deal with them. Some tips along the lines of how to do "printf style debugging" when in tactic mode is what I'm after. Thanks in advance.

[Ruben Van de Velde]

You can click on the term in the widget

[Johan Commelin]

@Trevor Fancher Are you using VScode? Because you can click on things in the goal view to explore them.

[Eric Rodriguez]

fwiw, usually try dsimp first if you don't get the tactic state. that simplifies things up to definitional equality, and so will actually turn that into just R.

[Trevor Fancher]

I am using VSCode. I didn't realize clicking on things let me dig around like that. Thats really neat!

[Trevor Fancher]

That certainly will change how I explore during proofs :)

[Kevin Buzzard]

Your pointy bracket R, hR term will surely be an insurance of a structure with two fields, one called val (which will presumably be R) and one called something else (which will be hR). As Eric says, you can probably use dsimp to tidy up, but note that sometimes you can then finish the proof and delete the dsimp because all it does is changes things to definitionally equal but easier-to-read things