rfl works but "by refl" doesn't

Stream: general

[Kenny Lau]

I have come across a most interesting example where rfl works but by refl doesn't:

import category_theory.opposites

universe u

lemma foo (β γ : Type u) (f : γ ⟶ β) (z : γ) : f.op.unop z = f z := rfl -- works
lemma bar (β γ : Type u) (f : γ ⟶ β) (z : γ) : f.op.unop z = f z := by refl -- fails!
lemma baz (β γ : Type u) (f : γ ⟶ β) (z : γ) : f.op.unop z = f z := by exact rfl -- works!

[Kenny Lau]

@Reid Barton @Bhavik Mehta

[Mario Carneiro]

apply rfl also fails

[Eric Wieser]

irreducible strikes again?

[Eric Wieser]

Oh never mind, those are long hom arrows

[Reid Barton]

opposite is indeed irreducible though