Specializing universal quantifier at elements of a subset

Stream: maths

[Panagiotis Angelinos]

Hello! I believe I have some type-theoretic confusions and lack of syntactical knowledge which is stopping me from proving some basic things. Here is, for example, a part of my tactics state:

X: Type u_1
inst✝¹: TopologicalSpace X
S: Set X
u v: ↑S
h1: Inseparable ↑u ↑v → ↑u = ↑v
huv: Inseparable u v
⊢ u = v

I would like to apply h1 here, but it does not work. The goal is an equality in S, whereas ↑u = ↑v is an equality in X. If you are wondering how I got h1, it is because I specialized

h1: ∀ (x y : X), Inseparable x y → x = y

at u and v, which might be the real problem. Is it allowed to specialize a quantifier like ∀ (x y : X) at points u v: ↑S where S : Set X?

[Filippo A. E. Nuccio]

You should try to create a #mwe so that one can easily copy-paste your code, rather than your state, in VSCode, and reproduce what goes on.

[Yaël Dillies]

No need for the MWE here, the problem is pretty clear

[Yaël Dillies]

That's because h1 is about equality in S while your goal is about equality in X

[Yaël Dillies]

docs#Subtype.coe_inj is the glue you're missing to go from one to the other

[Patrick Massot]

Filippo is still right to train people to provide mwes.

[Panagiotis Angelinos]

Thanks for the help. I'm sorry I didn't provide an MWE.

[Filippo A. E. Nuccio]

No reason to be sorry, it is just a good habit to develop in order to let people help you more easily. We all tried something like this at the beginning :smile: