Enlarge the codomain of a function

Stream: Is there code for X?

[Pedro Sánchez Terraf]

Really basic question: I have S U : set α, h : S ⊆ U, and f : X → ↥S. Is there a coextension function such that coextension f h U : X → ↥U is f with codomain U?

I tried to do

#find Π x y, (x ⊆ y) → (_ → x) → (_ → y)

but found nothing (other searches, like #find (_ → _) → (_ ⊆ _) → (_ → _) resulted in “excessive memory consumption”).
Meta question: How do I look for things like this without bothering you??

[Sky Wilshaw]

You could try something like inclusion h \circ f.

[Sky Wilshaw]

docs#set.inclusion

[Sky Wilshaw]

At least in my opinion Lean is a hard language to learn, and asking questions should be encouraged - it certainly helped me a lot when I was learning!

[Sky Wilshaw]

One way to find functions that you might not know about is library_search. If you write a (precise enough) function signature, lean can try to search for a function that it knows about to basically fill in that function in any way it knows. For example:

example {α β : Type*} (S U : set α) (h : S ⊆ U) (f : β → S) (b : β) : U := by library_search

gives

Try this: refine set.inclusion h (f b)

You might have seen this in the context of writing proofs, where library_search gives a proof that's already in mathlib, but there's no real difference between proofs and other terms in Lean, so library_search can help you with both. Of course, it doesn't know what you're actually trying to do, so library_search won't always give you the correct answer:

def add_one (n : ℕ) : ℕ := by library_search
-- Try this: exact n