RFC: `generalize` should utilize proof-irrelevance to auto-generalize proofs

Proposal

In certain situations involving indexed type families, the generalize tactic fails to proceed because generalization breaks some proof term that depends on the generalized term. However, it seems that one can always proceed by proof-irrelevance: there is no way that anything else could depend on the proof term having a specific value, so it is always possible to generalize the proof term first. I suggest that generalize should do this automatically.

axiom foo : (n m : Nat) → Type
axiom mk : (n : Nat) → n = n → foo n n
axiom f : Nat → Nat

set_option pp.proofs true in
example (n m : Nat) (h : f n = f m) :
    HEq (mk (f n) (congrArg f rfl)) (mk (f m) rfl) := by
  /- tactic 'generalize' failed, result is not type correct
    ∀ (x : ℕ), x = f m → HEq (mk x (congrArg f rfl)) (mk (f m) rfl) -/
  -- Specifically, `congrArg f rfl : f n = f n`, but should have type `x = x`. -/
  generalize f n = x at h

example (n m : Nat) (h : f n = f m) :
    HEq (mk (f n) (congrArg f rfl)) (mk (f m) rfl) := by
  generalize congrArg f rfl = pf -- works
  generalize f n = x at h pf -- works
  cases h -- now we can finish the proof
  rfl

UPDATE: I learned that in mathlib, proof generalization is supported by generalize_proofs, so generalize congrArg f rfl = pf can become generalize_proofs pf. Since mathlib supports that, this addition would probably only make sense in core if the functionality is more broadly useful.

• User Experience: It would eliminate a paper-cut when working with dependent types.

• Beneficiaries: In practice, this kind of situation comes up in mathlib's category theory library. Users working with or on category theory may benefit.

• Maintainability: The generalize code may become more complicated.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the core generalize tactic implementation and compare it with mathlib's generalize_proofs behavior described in the issue. Determine whether proof-irrelevance should be supported in core, then validate the proposal against the provided dependent-type examples and confirm the existing behavior remains correct.