failed to instantiate goal with subtypes

Stream: new members

[Nir Paz]

This code produces a "failed to instantiate goal" error:

example : ∃ (f : {x : ℝ | true} → {x : ℝ | true}), true :=
begin
  use λ x, ⟨if (∃ (n : ℕ), n > 0) then 0 else 0, sorry⟩,
end

But when I change ∃ (n : ℕ), n > 0 to something simpler, like 0 = 0, then it works. Obviously I'm working on something a bit different than this (this is the minimalistiest example I found), but I need to define a function with "if" for it, and then because of this problem I can't even try to fill the sorry.
I think maybe I'm just misunderstanding something basic about subtypes or defining functions this way, so any clarification is welcome (:

[Eric Wieser]

This is just use being annoying

[Kyle Miller]

I haven't tested your example, but one thing that seems possible is that since if requires a decidable instances (and there's not immediately one here), use fails, and use can be unfriendly like that. Maybe try using the classical tactic first? This adds the classical decidable instances.

[Eric Wieser]

Use refine instead of use and you'll get a better error message

[Kevin Buzzard]

By the way, functions go from types to types and the domain and codomain of your f are terms (because they're subsets), so they're being coerced into types which causes a bit of obfuscation. You can use {x : \R // true} to make the subtype directly.

[Nir Paz]

using classical worked, thanks!