no goals
X : TopCat
T✝ T : ↑X → Type v
P : PrelocalPredicate T
U : Opens ↑X
f : (x : { x // x ∈ U }) → T ↑x
h : pred P f
x : { x // x ∈ U }
⊢ pred P fun x => f ((fun x => { val := ↑x, property := (_ : ↑x ∈ ↑U) }) x)
convert h