Eq.rec with a constant does nothing: h ▸ c = c

Stream: Is there code for X?

[Snir Broshi]

docs#eq_rec_constant solves the simple case:

import Mathlib
theorem eq_rec_constant' {α β : Sort*} {x y : α} (h : x = y) (c : β) : h.rec c = c :=
  eq_rec_constant c h

The motive (fun _ _ ↦ β) takes a value of type α, a proof that x is equal to it, and returns a some constant type β that doesn't depend on those two values.

[Snir Broshi]

But what about cases where the motive is more complicated?

theorem eq_rec_constant₂ {α β : Sort*} {P : α → Sort*} {x y : α} (p : P y) (h : x = y) (c : β) :
    h.rec (fun _ ↦ c) p = c := by
  cases h
  rfl

Here the motive has another argument p for a term of type P _ (I'm not sure what the motive is exactly, but something like that).

[Snir Broshi]

theorem eq_rec_constant₃ {α β : Sort*} {P : α → Sort*} {Q : (a : α) → P a → Sort*} {x y : α}
    (p : P y) (q : Q y p) (h : x = y) (c : β) : h.rec (fun _ _ ↦ c) p q = c := by
  cases h
  rfl

Now there's a q that depends on the values before it, including p. And we can keep going like this.
I think we can even add a term whose type depends on the equality h and not just y, which further complicates matters.

[Snir Broshi]

Is there an easy way to solve this, perhaps with a tactic? Or should we add the versions with more params to Mathlib?
This came up when working with Sym2 (and Sym2.rec which uses Eq.rec), but I'm not able to inline the proof for eq_rec_constant₂ in this:

theorem Sym2.eq_rec_constant₂ {α : Type*} {β : Sort*} {P : Sym2 α → Sort*} {a b : α} (p : P s(b, a))
    (c : β) : (Sym2.sound (Sym2.Rel.swap a b)).rec (fun _ ↦ c) p = c := by
  cases Sym2.sound (Sym2.Rel.swap a b) -- error
  rfl

Also I was surprised that just rfl doesn't work here (without cases)

[Aaron Liu]

import Mathlib

theorem Sym2.eq_rec_constant₂ {α : Type*} {β : Sort*} {P : Sym2 α → Sort*} {a b : α} (p : P s(b, a))
    (c : β) : (Sym2.sound (Sym2.Rel.swap a b)).rec (fun _ ↦ c) p = c := by
  rw! [Sym2.sound (Sym2.Rel.swap a b)]
  rfl

[Snir Broshi]

Thanks! and thank you for creating rw! :)
Is there a way without it though? why doesn't simp [Sym2.sound (Sym2.Rel.swap a b)] work here?

[Aaron Liu]

that's because it's in a dependent position

[Snir Broshi]

yeah but simp usually magically works
I'm just a bit worried about how being one of the first users of a tactic might affect my PR getting approved