# Zulip Chat Archive

## Stream: general

### Topic: subset refl weirdness

#### Reid Barton (May 04 2018 at 18:47):

Is this a bug?

set_option pp.all true example {α : Type} (s : set α) : s ⊆ s := by refl /- error: invalid apply tactic, failed to unify @has_subset.subset.{0} (set.{0} α) (@set.has_subset.{0} α) s s with @has_subset.subset.{?l_1} (list.{?l_1} ?m_2) (@list.has_subset.{?l_1} ?m_2) ?m_3 ?m_3 state: α : Type, s : set.{0} α ⊢ @has_subset.subset.{0} (set.{0} α) (@set.has_subset.{0} α) s s -/

#### Reid Barton (May 04 2018 at 18:52):

I guess this actually does not exist anywhere...?

@[refl] lemma set.subset.refl {α : Type u} (s : set α) : s ⊆ s := λ x, id

#### Simon Hudon (May 04 2018 at 18:53):

You're probably right. You can try:

local attribute [refl] set.subset.refl -- if that's the name of the appropriate lemma

#### Simon Hudon (May 04 2018 at 18:53):

Then your proof will work

#### Reid Barton (May 04 2018 at 18:58):

Ah, the lemma does exist in mathlib, but without `@[refl]`

#### Kevin Buzzard (May 04 2018 at 22:01):

The proof of a refl lemma is often `rfl`

, and conversely any proof which is proved with `rfl`

is I think automatically tagged `@[refl]`

, but because the proof wasn't rfl here the tag is needed.

#### Simon Hudon (May 04 2018 at 22:03):

`rfl`

is only for reflexivity of equality and the tag comes from the fact that `rfl`

implies that the two terms are definitionally equal. But if we're talking of reflexivity of other relations than equality, it doesn't imply anything with regards to definitional equality

#### Kevin Buzzard (May 04 2018 at 22:10):

I just tried my theory and the lemma I proved with rfl was tagged `@[_refl_lemma]`

not `@[refl]`

#### Chris Hughes (May 05 2018 at 19:59):

`@[refl]`

means it's a proof that a relation is reflexive and is for the `refl`

tactic. `@[_refl_lemma]`

means it's a proof of equality proved using `rfl`

for the `dsimp`

tactic.

Last updated: May 14 2021 at 04:22 UTC