lean - 快速简化表达式 'ite ("a"="b") x y'

Question

当留下一个ite ("a"="b") x y涉及两个不同字符串文字之间可判定相等的形式的表达式时，似乎simp它本身不允许我将此表达式简化为y. ite ("a"="a") x y这与简化为xwith的情况相反simp。所以我发现自己在做一个案例分析cases decidable.em ("a"="b") with H H，然后使用exfalsoand处理一个案例dec_trivial，另一个使用simp [H]. 所以我能够继续前进，但我想知道是否有更惯用和更短的方法来实现相同的结果。

Answer 1

要么 要么rw [if_neg (show "a" ≠ "b", from dec_trivial)]是simp [if_neg (show "a" ≠ "b", from dec_trivial)]我知道的最简单的方法。