behaviour of simpa changed

Stream: general

[Chris Hughes]

A few of my proofs have broken since the recent changes to simpa. For example this one.

lemma zero_pow {α : Type*} [semiring α] {n : ℕ} (hn : 0 < n) : (0 : α) ^ n = 0 :=
by cases n; simpa [_root_.pow_succ, lt_irrefl] using hn

It fails if it solves the goal without using hn

[Mario Carneiro]

You should just use by cases n; simp [_root_.pow_succ, lt_irrefl, hn] here. simpa is not supposed to be a replacement for simp