Extracting a proof from a dependent function call

Stream: lean4

[Jeremy Salwen]

Is there a way to refer to a proof which is embedded in a dependent type? Here is a MWE:

import Std.Data.List.Basic
import Mathlib.Tactic.applyFun
import Mathlib.Data.List.Basic

open Lean

lemma List.getLast?_some {α} {l: List α} {a:α} (h:List.getLast? l = some a):
  List.getLast l (by have h₂:= congr_arg Option.isSome h; simp at h₂; simp [h₂]) = a := by sorry

lemma examp  (h: List.getLast? l = some e): l ≠ [] := by
  have h₂ := List.getLast?_some h
  exact h₂.what

At the bottom, I have h₂: List.getLast l (_ : ¬l = []) = e as a hypothesis, and I'd like to just refer to the anonymous proof which is the second argument to getLast, but I can't figure out how.

[Yakov Pechersky]

in mathlib3, we have tactic#generalize_hyps for extracting that out

[Mario Carneiro]

you mean generalize_proofs?

[Jeremy Salwen]

I just tried generalize_proofs h₂ but it seems to have no effect.

[Eric Wieser]

generalize_proofs at h₂ I think is the correct spelling, but it fails mysteriously

[Jeremy Salwen]

I get the error unknown free variable '_uniq.334'

[Eric Wieser]

  revert h₂
  generalize_proofs h'
  intro h₂

works

[Eric Wieser]

That failure looks like a bug in docs4#Mathlib.Tactic.GeneralizeProofs.generalizeProofs to me

[Arien Malec]

This is the same issue I was seeing in mathlib4#1179

[Arien Malec]

And the revert/intro trick works there.

[Arien Malec]

Ah, in one place, but not the other.