simp? doesn't propagate "at h"

Stream: general

[Yakov Pechersky]

Try simp? at h in the proof below -- the "Try this" doesn't keep the "at h" part.

import data.nat.cast

open nat

lemma div2_add_two_of_not_bodd (n : ℕ) (h : n.bodd = ff) : div2 (n + 2) = div2 n + 1 :=
begin
  induction n with n hn,
  { simp },
  { -- simp? at h, -- does not say "Try this"
    simp only [bnot_eq_ff_eq_eq_tt, nat.bodd_succ] at h,
    simp [h] }
end

[Yakov Pechersky]

I know that this isn't the best tactic proof to prove this, just an example.

[Johan Commelin]

@Yakov Pechersky Yes, this is a known issue. I hacked on simp to get simp? working. But I am horrible at C++ and meta code. So I hope that someone else can port all the squeeze_simp goodies to simp?.