diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 389010b828..f96e371c50 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1490,6 +1490,11 @@ have been simplified by using the modifier `↓`. Here is an example
 @[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
 ```
 
+You can instruct the simplifier to rewrite the lemma from right-to-left:
+```lean
+attribute @[simp ←] and_assoc
+```
+
 When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
 The equational theorems of function are applied at very low priority (100 and below).
 If there are several with the same priority, it is uses the "most recent one". Example:
@@ -1501,7 +1506,7 @@ If there are several with the same priority, it is uses the "most recent one". E
   cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
 /--
 Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.
diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean
index 88f19a6ada..71a84b7f58 100644
--- a/src/Lean/Meta/Tactic/Simp/Attr.lean
+++ b/src/Lean/Meta/Tactic/Simp/Attr.lean
@@ -26,10 +26,13 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
         let go : MetaM Unit := do
           let info ← getConstInfo declName
           let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-          let prio ← getAttrParamOptPrio stx[2]
+          let inv := !stx[2].isNone
+          let prio ← getAttrParamOptPrio stx[3]
           if (← isProp info.type) then
-            addSimpTheorem ext declName post (inv := false) attrKind prio
+            addSimpTheorem ext declName post (inv := inv) attrKind prio
           else if info.hasValue then
+            if inv then
+              throwError "invalid '←' modifier, '{declName}' is a declaration name to be unfolded"
             if (← SimpTheorems.ignoreEquations declName) then
               ext.add (SimpEntry.toUnfold declName) attrKind
             else if let some eqns ← getEqnsFor? declName then
diff --git a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
index dadbb4846d..eb26a525c5 100644
--- a/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
+++ b/src/Lean/Meta/Tactic/Simp/RegisterCommand.lean
@@ -21,7 +21,7 @@ macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
   let procDescr := quote s!"simproc set for {procId.getId.toString}"
   -- TODO: better docDomment for simprocs
   `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (prio)? : attr
     /-- Simplification procedure -/
     initialize extProc : SimprocExtension ← registerSimprocAttr $(quote procId.getId) $procDescr none $(quote procId.getId)
     /-- Simplification procedure -/
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index e846f721c5..cc56e30f26 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -49,6 +49,11 @@ def Origin.key : Origin → Name
   | .stx id _ => id
   | .other name => name
 
+/-- The origin corresponding to the converse direction (`← thm` vs. `thm`) -/
+def Origin.converse : Origin → Option Origin
+  | .decl declName phase inv => some (.decl declName phase (not inv))
+  | _ => none
+
 instance : BEq Origin where
   beq a b := match a, b with
     | .decl declName₁ _ inv₁, .decl declName₂ _ inv₂ =>
@@ -225,9 +230,10 @@ If `e` is a backwards theorem `← thm`, we must ensure the forward theorem is e
 from `d`. See issue #4290
 -/
 private def eraseFwdIfBwd (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems :=
-  match e.origin with
-  | .decl declName post true => eraseIfExists d (.decl declName post false)
-  | _ => d
+  if let some converseOrigin := e.origin.converse then
+    eraseIfExists d converseOrigin
+  else
+    d
 
 def addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems :=
   let d := eraseFwdIfBwd d e
@@ -262,13 +268,20 @@ def SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (
 
 def SimpTheorems.erase [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
-  unless d.isLemma thmId ||
+  if d.isLemma thmId ||
     match thmId with
     | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
-  do
-    logWarning m!"'{thmId.key}' does not have [simp] attribute"
-  return d.eraseCore thmId
+  then
+    return d.eraseCore thmId
+
+  -- `attribute [-simp] foo` should also undo `attribute [simp ←] foo`.
+  if let some thmId' := thmId.converse then
+    if d.isLemma thmId' then
+      return d.eraseCore thmId'
+
+  logWarning m!"'{thmId.key}' does not have [simp] attribute"
+  return d
 
 private partial def isPerm : Expr → Expr → MetaM Bool
   | .app f₁ a₁, .app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba4..cb8a954a4d 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
diff --git a/tests/lean/run/issue5828.lean b/tests/lean/run/issue5828.lean
new file mode 100644
index 0000000000..5a5a990d0c
--- /dev/null
+++ b/tests/lean/run/issue5828.lean
@@ -0,0 +1,97 @@
+axiom a : Nat
+axiom b : Nat
+axiom a_eq_b : a = b
+
+axiom P : Nat → Nat → Prop
+
+-- Warm-up: rewriting in the forward direction
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+attribute [simp] a_eq_b
+
+/--
+error: unsolved goals
+⊢ P b b
+-/
+#guard_msgs in example : P a b := by simp
+
+attribute [-simp] a_eq_b
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+-- Re-adding an attribute after [-simp] does not work, see
+-- https://github.com/leanprover/lean4/issues/5868
+
+attribute [simp] a_eq_b
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+-- so this test use new copies of `a_eq_b` for now
+
+axiom a_eq_b_2 : a = b
+
+attribute [simp ←] a_eq_b_2
+
+/--
+error: unsolved goals
+⊢ P a a
+-/
+#guard_msgs in example : P a b := by simp
+
+-- Removing the attribute works, no matter the direction
+
+attribute [-simp] a_eq_b_2
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+-- Setting one should erase the other
+
+axiom a_eq_b_3 : a = b
+
+attribute [simp ←] a_eq_b_3
+attribute [simp] a_eq_b_3
+
+/--
+error: unsolved goals
+⊢ P b b
+-/
+#guard_msgs in example : P a b := by simp
+
+
+-- The erasure is sticky:
+attribute [simp ←] a_eq_b_3
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+axiom a_eq_b_4 : a = b
+
+attribute [simp] a_eq_b_4
+attribute [simp ←] a_eq_b_4
+
+/--
+error: unsolved goals
+⊢ P a a
+-/
+#guard_msgs in example : P a b := by simp
+
+
+-- Some more error conditions
+
+axiom P_a : P a a
+
+/-- error: invalid '←' modifier in rewrite rule to 'True' -/
+#guard_msgs in
+attribute [simp ←] P_a
+
+/-- error: invalid 'simp', it is not a proposition nor a definition (to unfold) -/
+#guard_msgs in
+attribute [simp ←] P
+
+/-- error: invalid '←' modifier, 'id' is a declaration name to be unfolded -/
+#guard_msgs in
+attribute [simp ←] id