| /-- | |
| trace: x y : Nat | |
| h : y = 0 | |
| ⊢ id (2 * x + y) = id (2 * x) | |
| -/ | |
| #guard_msgs in | |
| example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by | |
| simp +arith only | |
| /- | |
| This is a test for a `simp` cache issue where the following incorrect goal was being | |
| produced. | |
| ``` | |
| ... |- id (2*x + y) = id (x + x) | |
| ``` | |
| instead of | |
| ``` | |
| ... |- id (2*x + y) = id (2*x) | |
| ``` | |
| -/ | |
| trace_state | |
| simp [h] | |
| example (x y : Nat) (h : y = 0) : id (x + x) = id ((x + x) + y) := by | |
| simp +arith only | |
| simp [h] |