Type mismatch although having the "correct" set membership

Stream: new members

[Michael Novak]

In the following example Lean complains that x should be of type I. Why is that? And how would you deal with this? I know that we can switch the membership sign ∈ to a type judgement sign : to get a dependent function type, but first I don't understand why do we get an error already in the theorem statement - what's the problem exactly and secondly, this is not exactly my real problem - in the real proof I'm working on I have to assume the set membership information to show that some condition holds in order to use a certain theorem from mathlib.

import Mathlib
example (S : Set ℝ) (hc : Convex ℝ S) (x₀ : S) (x : ℝ) : x ∈ S → (Set.uIcc x₀ x) ⊆ S := sorry

[Weiyi Wang]

(deleted)

[Weiyi Wang]

Because x₀ is now of type ↥S, not of type ℝ, Set.uIcc x₀ _ is inferred as of type Set ↥S (not Set ℝ), so it wants _ := x of type ↥S as well, which is wrong. You can write Set.uIcc x₀.val x where x₀.val is of type ℝ, so the whole thing is inferred as of type Set ℝ. We want to avoid using Set as a type because of this trouble.

[Weiyi Wang]

You can write

example (S : Set ℝ) (hc : Convex ℝ S) (x₀ x : ℝ)  (h1 : x₀∈ S) (h2 : x ∈ S) : Set.uIcc x₀ x ⊆ S := sorry

(This is also more symmetrical than your original statement)

[Michael Novak]

Thank you very much! So would you say that in general when writing a theorem in which I want to have an assumption of a variable x which should be in some subset s : Set α , where α is some type, instead of making the assumption (x : s) I should make two assumptions : (x : α) (x ∈ s) ?

[Weiyi Wang]

Yep, that's usually the best way to write it