fix: dsimp should reduce kernel projections (#3607)

closes #3395
leanprover · Mar 5, 2024 · 436d7be · 436d7be
1 parent 414f0eb
commit 436d7be
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -159,6 +159,9 @@ private def reduceStep (e : Expr) : SimpM Expr := do
       return f.betaRev e.getAppRevArgs
   -- TODO: eta reduction
   if cfg.proj then
+    match (← reduceProj? e) with
+    | some e => return e
+    | none =>
     match (← reduceProjFn? e) with
     | some e => return e
     | none   => pure ()

diff --git a/tests/lean/run/3395.lean b/tests/lean/run/3395.lean
@@ -0,0 +1,8 @@
+structure S where
+  f : Nat → Nat
+
+example (h : g 1 = x) : { f := g : S }.f 1 = x := by
+  unfold S.f
+  dsimp
+  guard_target =ₛ g 1 = x
+  assumption