Basic Finset question

Stream: new members

[David Landsberg]

Having trouble restating the above example you gave, but as a lemma. This is what I have (and it works fine if i replace the line stating the lemma with "example (s1 t1 : u) : {s1, t1} = {t1, s1} :=" ):

variable u : Type
variables s t : set u

lemma l4: {u} (s1 t1 : u) : {s1, t1} = {t1, s1} :=
begin
apply set.ext,
intro x,
rw set.mem_insert_iff,
rw set.mem_insert_iff,
rw set.mem_singleton_iff,
rw set.mem_singleton_iff,
exact or.comm
end

[Notification Bot]

David Landsberg has marked this topic as unresolved.