# What is the difference between refl and rfl in Lean 3?

I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? I've read that refl is "more powerful", but I never knew beforehand if one would definitely work where the other may not. Bonus points for by exact rfl explanations. I also wonder if there are significant changes to these between different versions of Lean 3...

• I changed the reflexivity tag to equality. Presumably there is no point in splitting equality into reflexivity, symmetry, transitivity, etc. Feb 14, 2022 at 13:14
• I can't seem to edit it. I can only edit some tags but not others. Or maybe I don't know how to use the internet. Feb 14, 2022 at 22:11

So you are correct that refl is a tactic, and rfl is a term, so for example:

example : 1 = 1 := rfl
example : nat = nat := by refl -- equivalent to putting rfl


But refl is more powerful, as it can also apply other lemmas that have the @[refl] attribute on them (like rfl) :

example : true ↔ true := rfl -- error!
example : true ↔ true := by refl -- fine! makes term iff.rfl
example : 0 ≤ 0 := by refl -- fine!


There are other similar tactics for symmetry (also symmetry' which is slightly better) and transitivity, both with their related attributes.

by exact rfl is a hack used to deal with the elaborator, which sometimes can infer what you mean wrong, but putting it into a tactic state forces it to realise what's going on. A similar hack is show _, from ... (although it seems this isn't commonly used with rfl)

• In the first line, rfl and refl seem like they should be swapped Feb 12, 2022 at 19:23
• It might be worth mentioning that refl is able to prove equalities because eq.refl has the [refl] attribute (i.e., equality isn't a special case). It's also part of a suite of three tactics for applying lemmas for relations: refl, symmetry, and transitivity. Feb 12, 2022 at 19:31

Separately from the rfl (term) vs refl (tactic) distinction, there is also the distinction between rfl and refl in lemma names:

#check @eq.refl  -- ∀ {α : Sort u_2} (a : α), a = a
#check @rfl      -- ∀ {α : Sort u_2} {a : α}, a = a

#check @iff.refl -- ∀ (a : Prop), a ↔ a
#check @iff.rfl  -- ∀ {a : Prop}, a ↔ a

#check @le_refl  -- ∀ {α : Type u_2} [_inst_1 : preorder α] (a : α), a ≤ a
#check @le_rfl   -- ∀ {α : Type u_2} [_inst_1 : preorder α] {a : α}, a ≤ a


The difference here is that that rfl uses an implicit {} binder for a, while refl uses a explicit () binder. So iff.rfl is shorthand for iff.refl _, le_rfl is shorthand for le_refl _, etc.