diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index d75bba4e0d..96654601a4 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -666,6 +666,8 @@ theorem Iff.refl (a : Prop) : a ↔ a :=
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
+
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
   Iff.intro
     (fun ha => Iff.mp h₂ (Iff.mp h₁ ha))
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 98755ee815..4a2c27d989 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -323,9 +323,14 @@ syntax (name := eqRefl) "eq_refl" : tactic
 `rfl` tries to close the current goal using reflexivity.
 This is supposed to be an extensible tactic and users can add their own support
 for new reflexive relations.
+
+Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
+reflexivity theorems (e.g., `Iff.rfl`).
 -/
 macro "rfl" : tactic => `(tactic| eq_refl)
 
+macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
+
 /--
 `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
 theorems included (relevant for declarations defined by well-founded recursion).
@@ -432,13 +437,17 @@ syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
 /--
 `rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
 -/
-macro (name := rwSeq) "rw" c:(config)? s:rwRuleSeq l:(location)? : tactic =>
+macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
   match s with
   | `(rwRuleSeq| [$rs,*]%$rbrak) =>
     -- We show the `rfl` state on `]`
     `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
+/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
+macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
+  `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))
+
 /--
 The `injection` tactic is based on the fact that constructors of inductive data
 types are injections.
diff --git a/tests/lean/run/1842.lean b/tests/lean/run/1842.lean
index b101bd2d82..c896679e11 100644
--- a/tests/lean/run/1842.lean
+++ b/tests/lean/run/1842.lean
@@ -9,7 +9,6 @@ theorem and_assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
 
 theorem and_left_comm : a ∧ (b ∧ c) ↔ b ∧ (a ∧ c) := by
   rw [← and_assoc, ← and_assoc, @And.comm a b]
-  exact Iff.rfl
 
 theorem pairwise_append {l₁ l₂ : List α} :
     (l₁ ++ l₂).Pairwise R ↔ l₁.Pairwise R ∧ l₂.Pairwise R ∧ ∀ {a} (_ : a ∈ l₁), ∀ {b} (_ : b ∈ l₂), R a b := by
diff --git a/tests/lean/run/deq.lean b/tests/lean/run/deq.lean
index 65f61fe2d6..9c6cb54d27 100644
--- a/tests/lean/run/deq.lean
+++ b/tests/lean/run/deq.lean
@@ -27,8 +27,8 @@ theorem deq_correct_2 (Q : LazyList τ)
   : deq Q = none ↔ Q.force = none
   := by
     cases h' : Q.force with
-    | none => unfold deq; rw [h']; simp
-    | some => unfold deq; rw [h']; simp
+    | none => unfold deq; rw [h']
+    | some => unfold deq; rw [h']
 
 theorem deq_correct_3 (Q : LazyList τ)
   : deq Q = none ↔ Q.force = none
diff --git a/tests/lean/run/rw_inst_mvars.lean b/tests/lean/run/rw_inst_mvars.lean
index eff45a55f5..93a5c7393b 100644
--- a/tests/lean/run/rw_inst_mvars.lean
+++ b/tests/lean/run/rw_inst_mvars.lean
@@ -1,6 +1,4 @@
 example  (p : Nat → Prop) (h : ∀ n, p (n+1) = p n) : (p m ↔ p 0) := by
   induction m
-  case succ ih =>
-    rw [h, ih]
-    exact Iff.rfl
+  case succ ih => rw [h, ih]
   case zero => exact Iff.rfl
diff --git a/tests/lean/runTacticMustCatchExceptions.lean.expected.out b/tests/lean/runTacticMustCatchExceptions.lean.expected.out
index ece6163a71..6c0381b827 100644
--- a/tests/lean/runTacticMustCatchExceptions.lean.expected.out
+++ b/tests/lean/runTacticMustCatchExceptions.lean.expected.out
@@ -1,27 +1,36 @@
-runTacticMustCatchExceptions.lean:2:25-2:28: error: tactic 'rfl' failed, equality expected
-  Nat.le 1 (a + b)
-a b : Nat
-⊢ 1 ≤ a + b
-runTacticMustCatchExceptions.lean:3:25-3:28: error: tactic 'rfl' failed, equality expected
-  Nat.le (a + b) b
-a b : Nat
-this : 1 ≤ a + b
-⊢ a + b ≤ b
-runTacticMustCatchExceptions.lean:4:25-4:28: error: tactic 'rfl' failed, equality expected
-  Nat.le b 2
-a b : Nat
-this✝ : 1 ≤ a + b
-this : a + b ≤ b
-⊢ b ≤ 2
-runTacticMustCatchExceptions.lean:9:18-9:21: error: tactic 'rfl' failed, equality expected
-  Nat.le 1 (a + b)
-a b : Nat
-⊢ 1 ≤ a + b
-runTacticMustCatchExceptions.lean:10:14-10:17: error: tactic 'rfl' failed, equality expected
-  Nat.le (a + b) b
-a b : Nat
-⊢ a + b ≤ b
-runTacticMustCatchExceptions.lean:11:14-11:17: error: tactic 'rfl' failed, equality expected
-  Nat.le b 2
-a b : Nat
-⊢ b ≤ 2
+runTacticMustCatchExceptions.lean:2:25-2:28: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  1 ≤ a + b : Prop
+runTacticMustCatchExceptions.lean:3:25-3:28: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  a + b ≤ b : Prop
+runTacticMustCatchExceptions.lean:4:25-4:28: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  b ≤ 2 : Prop
+runTacticMustCatchExceptions.lean:9:18-9:21: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  1 ≤ a + b : Prop
+runTacticMustCatchExceptions.lean:10:14-10:17: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  a + b ≤ b : Prop
+runTacticMustCatchExceptions.lean:11:14-11:17: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  b ≤ 2 : Prop