chore: ensure that the rfl tactic tries Iff.rfl (#5359)

Revert the removal of the macro containing `Iff.rfl` in #5329; it was
causing errors in leanprover-community/mathlib4#16839.

src/Init/Core.lean

@@ -823,6 +823,8 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
+
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=

tests/lean/run/5359.lean

@@ -0,0 +1,19 @@
+/-!
+Test that `Iff.rfl` is tried by the `rfl` tactic.
+-/
+universe u v w
+
+class L (F : Sort u) (α : outParam (Sort v)) (β : outParam (α → Sort w)) where
+  coe : F → ∀ a : α, β a
+
+instance {F : Sort u} {α : Sort v} {β : α → Sort w} [L F α β] :
+    CoeFun F (fun _ ↦ ∀ a : α, β a) where coe := @L.coe _ _ β _
+
+instance {π : Nat → Type u} [∀ i, LE (π i)] : LE (∀ i, π i) where le x y := ∀ i, x i ≤ y i
+
+structure S (α : Nat → Type u) where
+variable {α : Nat → Type u} [∀ i, LE (α i)]
+instance : L (S α) Nat α := sorry
+instance : LE (S α) := ⟨fun f g ↦ ∀ i, f i ≤ g i⟩
+
+example : ∀ {a b : S α}, L.coe a ≤ L.coe b ↔ a ≤ b := by rfl