Simplifying a match on decidable equality check

Stream: lean4

[Yann Herklotz]

Is there a way to simplify a match based on a decidable equality check? I can't seem to simplify the following without having to manually provide a rewrite for result of the equality check.

structure A where
  a : String
  b : String
deriving DecidableEq

example b : (match ({ a := "", b := "b" } : A) == { a := "", b := "c" } with
             | true => 1
             | false => 2) = b := by
  -- simp
  have : (({ a := "", b := "b" } : A) == { a := "", b := "c" }) = false := by decide
  simp [this]
  sorry

The following seems to work as expected when using if instead of match.

example b : (if ({ a := "", b := "b" } : A) == { a := "", b := "c" }
             then 1
             else 2) = b := by
  simp
  sorry

[Yann Herklotz]

Nevermind, I think I minimised my example too much, in this case the following works fine:

example b : (match ({ a := "", b := "b" } : A) == { a := "", b := "c" } with
             | true => 1
             | false => 2) = b := by
  simp [BEq.beq]
  sorry