set type

Stream: new members

[vxctyxeha]

h32 : {1 - √2, 3 + √7, 1 + √2, 5} ⊆ p.roots
⊢ {1 - √2, 3 + √7, 1 + √2, 5} ≤ p.roots How to change symbols ⊆ to ≤

[Matt Diamond]

do you need to? did you try exact h32?

[Ruben Van de Velde]

That's a bad habit though. Does SetLike.le_def work?

[Weiyi Wang]

roots is a Multiset, right? I don't think you can do this change for Multiset because LE and subset are different for Multiset

[Weiyi Wang]

oh

[Weiyi Wang]

one direction is true,

[Weiyi Wang]

but it is not your direction :( https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Multiset/Defs.html#Multiset.subset_of_le