## Stream: general

### Topic: refl power

#### Patrick Massot (May 13 2020 at 13:43):

At https://github.com/leanprover-community/tutorials/issues/11, @Dan Stanescu asks why rw is so powerful. I know that part of the answer is it calls refl, by I don't understand why refl works when the relevant lemma doesn't seem to be tagged.

import data.nat.basic

open nat

-- The following lemma is not tagged refl
#check @dvd_refl
/- dvd_refl : ∀ {α : Type*} [comm_semiring α] (a : α), a ∣ a -/

example (n : ℕ) : n ∣ n := by refl


#### Patrick Massot (May 13 2020 at 13:45):

Note that you cannot replace by refl with rfl here

#### Gabriel Ebner (May 13 2020 at 13:50):

It is tagged?

-- #print dvd_refl
@[refl, simp, priority 100]
theorem dvd_refl : ∀ {α : Type u} [_inst_1 : comm_semiring α] (a : α), a ∣ a :=


(deleted)

#### Patrick Massot (May 13 2020 at 13:53):

Ok, so someone added this attribute far away from the lemma itself (presumably in mathlib)

#### Patrick Massot (May 13 2020 at 13:53):

I should have used #print instead of "Go to definition"

#### Johan Commelin (May 13 2020 at 13:53):

I'm about to move that definition out of core

#### Patrick Massot (May 13 2020 at 13:54):

It even sounds familiar. I think this is not the first time I meet this issue actually.

#### Johan Commelin (May 13 2020 at 13:54):

And when I say "I", of course I mean "Johan, with an enormous amount of help from Gabriel"

#### Patrick Massot (May 13 2020 at 13:55):

https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ring.lean#L156

Last updated: May 08 2021 at 03:17 UTC