refl power

Stream: general

[Patrick Massot]

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]

Note that you cannot replace by refl with rfl here

[Gabriel Ebner]

It is tagged?

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

[Kenny Lau]

(deleted)

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

I'm about to move that definition out of core

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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