generalize_proofs failed

Stream: general

[Patrick Johnson]

It doesn't make new hypothesis h in this example:

import tactic

noncomputable theory
open_locale classical

def a : ℕ := if h : ∃ (k : ℕ), k = 1 then h.some else 0

example : a = 1 :=
begin
  rw [a, dif_pos], swap, { exact ⟨1, rfl⟩ },
  generalize_proofs h,
  sorry
end

[Mario Carneiro]

#13025