CanLift.prf

theorem CanLift.prf : ∀ {α : Sort u_1} {β : Sort u_2} {coe : outParam (β → α)} {cond : outParam (α → Prop)} [self : CanLift α β coe cond] (x : α), cond x → ∃ y, coe y = x

This theorem states that for any types `α` and `β`, given a function `coe` that maps elements from `β` to `α`, and a predicate `cond` that applies to elements of `α`, assuming that we can lift `α` to `β` via `coe` under the condition `cond`, for any element `x` in `α` that satisfies `cond`, there exists an element `y` in `β` such that `coe y` is equal to `x`. In other words, any element of `α` satisfying `cond` can be seen as an image of some element in `β` under the function `coe`.

More concisely: Given functions `coe : β -> α` and predicate `cond : α -> Prop`, if for all `x : α` with `cond x`, there exists `y : β` such that `coe y = x`, then `cond` has a lifting to a predicate on `β` via `coe`.