fix: dsimp missing theorems for literals (#4467)

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -430,7 +430,10 @@ private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fu
     if (← readThe Simp.Context).isDeclToUnfold declName then
       return .continue e
     else
-      return .done e
+      -- Users may have added a `[simp]` rfl theorem for the literal
+      match (← (← getMethods).dpost e) with
+      | .continue none => return .done e
+      | r => return r
   else
     return .continue e
 

src/Lean/Meta/Transform.lean

@@ -21,7 +21,7 @@ inductive TransformStep where
   For `pre`, this means visiting the children of the expression.
   For `post`, this is equivalent to returning `done`. -/
   | continue (e? : Option Expr := none)
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 namespace Core
 

tests/lean/run/dsimpNatLitIssue.lean

@@ -0,0 +1,43 @@
+variable {R M : Type}
+
+class Zero (α : Type) where
+  zero : α
+
+instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
+  ofNat := ‹Zero α›.1
+
+/-- Typeclass for the `⊥` (`\bot`) notation -/
+class Bot (α : Type) where
+  /-- The bot (`⊥`, `\bot`) element -/
+  bot : α
+
+/-- The bot (`⊥`, `\bot`) element -/
+notation "⊥" => Bot.bot
+
+/-- Typeclass for types with a scalar multiplication operation, denoted `•` (`\bu`) -/
+class SMul (M α : Type) where
+  smul : M → α → α
+
+infixr:73 " • " => SMul.smul
+
+structure Submodule (R : Type) (M : Type) [Zero M] [SMul R M] where
+  carrier : M → Prop
+  zero_mem : carrier (0 : M)
+
+variable [Zero M] [SMul R M]
+
+instance : Bot (Submodule R M) where
+  bot := ⟨(· = 0), rfl⟩
+
+instance : Zero (Submodule R M) where
+  zero := ⊥
+
+@[simp]
+theorem zero_eq_bot : (0 : Submodule R M) = ⊥ :=
+  rfl
+
+theorem ohai : (0 : Submodule R M) = ⊥ := by
+  simp -- works
+
+theorem oops : (0 : Submodule R M) = ⊥ := by
+  dsimp -- should work