# Lean4: How to construct an HEq between dependent functions?

I have an extremely simple goal to prove:

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

The reason the match happens is because the type of px is (PEmpty ⊕ t) and dir is a variable whose type depends on the value of px. So this is a heterogeneous equality between a dependent function that matches on its first argument but doesn't use it - it does so only to teach the compiler, and a non-dependent function (basically const).

I'm in tactic mode but cannot use funext here, because it seems to only apply to nondependent functions. I basically want to do a substitution, but don't know how.

### Some more context

The biggest issue for me here is that I cannot even extract this goal to the top level in any way. The most reduced version of this problem I could manage to extract is this:

def hmm (k : Type) (b : (Empty ⊕ k) → Type) : HEq
(fun (px : Empty ⊕ k) (rd : b px) => match px with | Sum.inr ahh => rd )
fun (x : Empty ⊕ k) (a : b x) => a :=
by
_

And this gives me a red squiggly line at the definition, which says this:

stuck at solving universe constraint
imax 1 1 ?u.106314 =?= 1
while trying to unify
(x : Empty ⊕ k) → b x → b x : Type
with
(x : Empty ⊕ k) → b x → b x : Type

The problem arises from the match expression, which must somehow be introducing that ?u.106314 metavariable (if that is what it is). If I change this to:

def hmm (k : Type) (b : (Empty ⊕ k) → Type) : HEq
(fun (px : Empty ⊕ k) (rd : b px) => rd)
fun (x : Empty ⊕ k) (a : b x) => a :=
by
_

The error disappears (and the proof is trivial). When this goal first appeared in my code, it had an explicit motive := ... with a huge thing in the ... given to the match - that's why I think match is doing some universe shenanigans. So before I can prove the goal above, I need to make the statement of this heterogeneous equality type check, but can't even figure that out.

Here's a gist with all the code needed to recreate this goal: https://gist.github.com/amuricys/e6ad118dd28873c11779b64edf0268f9

• Can you please edit your question with a MWE that we can paste into Lean? (Turn your above goal into an example or theorem with a sorry for the proof. Make sure it type checks.) Thanks! Commented Mar 26 at 23:03
• Hi Jason, sorry, I just added a lot more context and turned the goal into something you should be able to copy paste (what do you mean by MWE?). One problem before actually proving what I need though is that I can't even get this to type check, I'm stuck on some universe issue. Thanks for asking for more details. Commented Mar 28 at 19:46
• To get things started I posted the answer I had earlier written. I think it matches your current code close enough, but maybe not your original use case. Commented Mar 28 at 20:31

Someone in the leanprover zulip managed to close this goal:

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

I followed up a bit:

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) =

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?

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.

(Wrote this before you updated your question.) I'm not sure where that goal came up, either in a real situation or just something you want to prove, but here is my best approximation to your situation:

def foo : (Sum Empty Nat) -> Nat
| Sum.inl e => e.elim
| Sum.inr n => n

def bar : (px : Sum Empty Nat) -> Fin (foo px) -> Fin (foo px)
| Sum.inl e, _ => e.elim
| Sum.inr _, dir => dir

def baz (x : Sum Empty Nat) : Fin (foo x) -> Fin (foo x) := id

example : bar = baz := by
funext x n
cases x with
| inl e => exact e.elim
| inr n => rfl

Notice that unlike your question, bar and baz are equal, not just Heq. Moreover, I can't think of an interpretation where Heq is the right approach. Heq x y are for when x and y have different-but-equal types, but in this case bar and baz have the same type (x : Sum Empty Nat) -> Fin (foo x) -> Fin (foo x). If baz instead had type (x : Nat) -> Fin (foo x) -> Fin (foo x) then these wouldn't be equal or Heq, since it is independent whether Nat = Sum Empty Nat in Lean, so you can't prove it.

• This goal, with the HEq, is generated by a bunch of successive applications of the unfold -> simp tactics, a strategy I've found great success with elsewhere (I've only been doing Lean for about a week). I agree that with Eq the proof is quite simple and I'm not sure why this HEq is introduced. I'm sure the types of the arguments to the functions being equalized are different but it's hard to check because I can't extract the goal to the top level without it giving the type error above. I added all the code necessary for generating this error to the answer :) Commented Mar 28 at 22:25