dsimp doesn't use iffs that hold by defeq

Stream: lean4

[Robin Arnez]

Normally, when writing lemmas about how two Props are equal, you use ... ↔ ... instead of ... = .... However, these kinds of theorems don't seem to be considered when using dsimp, which would force you to additionally write an equality theorem. A simple example of this is e.g. gt_iff_lt:

example (x y : Nat) : x > y ↔ y < x := by
  dsimp -- dsimp made no progress

This might be solvable by extending isRflProofCore to allow Iff.refl and Iff.rfl and Iff.symm.

[Ruben Van de Velde]

This is https://github.com/leanprover-community/mathlib4/issues/10675

[Eric Wieser]

Added some more context there

[Marcus Rossel]

https://github.com/leanprover/lean4/issues/2678