fix: dsimp should reduce kernel projections

closes #3395

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 ()

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