Existence of a function as a goal

Stream: new members

[Torger Olson]

I have some goals of the form: there exists a function satisfying some conditions (e.g. commuting with two given functions). I can have u : B → C, and build it how I would on paper, but then Lean forgets the properties of u I baked into the construction.

Are there any resources on/general tips for accomplishing these sorts of goals? Can I def a function in the tactic state?

For context, I'm trying to a formalize an assignment for the course I TA for.

[Alex J. Best]

Use let u := blah (see tactic#let) instead of have