How to prove HEq between dependent functions?

Stream: lean4

[André Muricy Santos]

I'm trying to understand how the goal in this gist: https://gist.github.com/amuricys/e6ad118dd28873c11779b64edf0268f9.
After a bunch of simplifications, the goal is simply a heterogeneous equality between two functions that ignore their first argument, except the first one pattern matches on it:

HEq
  (fun px rd =>
    match px, rd with
    | Sum.inr _ppos, dir => dir)
  fun x a => a

I've tried extracting a simple version of this to the top level as a lemma but can't even get it to type check.
In the goal I'm trying all sorts of tricks, including going into conversion mode so that I can get rid of that HEq. When I do this:

def hmm {pos : Type} {dir : pos → Type} (px : 𝟬.pos ⊕ pos) (rd : dir (match px with | Sum.inr ppos => ppos) ) :
  (match px, rd with
    | Sum.inr _ppos, dir => dir)
  =
  rd
  := by
    cases px
    . contradiction
    . rfl
-- ...
conv =>
        lhs -- this is: fun px rd => match px, rd with | Sum.inr _ppos, dir => dir
        intro px rd
        rw [hmm px rd] -- trying to rewrite with the non-heterogeneous equality lemma
      _

I get the most incredible type error at the application of hmm:

application type mismatch
  hmm px rd
argument
  rd
has type
  dir✝
    (match px with
    | Sum.inr ppos => ppos) : Type
but is expected to have type
  dir✝
    (match px with
    | Sum.inr ppos => ppos) : Type

This type is not equal to itself (?????). I'm very lost on how to proceed with this. I feel like there should be a subst somewhere, but I can't figure out where.

[André Muricy Santos]

(this is cross posted from stack exchange: https://proofassistants.stackexchange.com/questions/3856/lean4-how-to-construct-an-heq-between-dependent-functions?noredirect=1#comment7498_3856)

[Kyle Miller]

I didn't think about the underlying problems, and I just plowed forward trying to close the goal using congr! and split, which was able to work.

theorem coproduct.leftUnitor.hom_inv_id (p : Poly) :
    composemap (leftUnitor.hom p) (leftUnitor.inv p) = polyid (𝟬 + p) := by
  ext d
  . cases d
    . contradiction
    . rfl
  . cases p
    . unfold composemap
      simp
      unfold inv
      simp
      unfold hom
      simp
      unfold polyid
      simp
      unfold id
      conv =>
        lhs
        intro x a
        simp
      congr!
      · split
        assumption
      rename_i a1 a2 a3 a4
      cases a1
      split
      assumption

[Kyle Miller]

Cleaned up:

theorem coproduct.leftUnitor.hom_inv_id (p : Poly) :
    composemap (leftUnitor.hom p) (leftUnitor.inv p) = polyid (𝟬 + p) := by
  ext d
  . cases d
    . contradiction
    . rfl
  . cases p
    simp only [hom, inv, composemap, polyid, Function.comp_apply, id_eq]
    congr!
    · split
      assumption
    · split
      assumption

[André Muricy Santos]

Wow, thank you! Could you explain to me what led you to apply congr!? I see that the goal it creates is

Sum.inr
    (match a✝ with
    | Sum.inr ppos => ppos) =
  a'✝

Which you're able to split on; this is exactly what I would have gotten if I'd applied funext to a _homogeneous_ equality right?

Also, why does using simp only help here at all? I thought that made the tactic less powerful since it ignores so many things it _could_ use. You also give it a lot of things that are not lemmas! In that case it just unfolds the definition?

[André Muricy Santos]

(the rename tactic is also gold, I'd been looking for a way to introduce hidden variable names forever)

[Edward van de Meent]

a good reason to use simp only [...] over simp is making the proof less sensitive to changes to what is and isn't a @[simp] lemma. furthermore, using just a bare line of simp only (or simp only []) allows you to reduce simple lambdas in goals, for example it reduces something like {fst := foo; snd := bar}.fst to foo

[Kyle Miller]

congr! is a tactic that tries to prove that the two sides of something that has two sides are equal, and it has different tricks to split things up. If there's a nasty HEq, sometimes congr! can make progress. (It also can do funext to show that two functions are equal.)

[Kyle Miller]

To get that simp only I used simp?. It's good practice for "non-terminal simps" for the reason Edward mentioned.

[André Muricy Santos]

awesome. thank you guys!