heq_congr?

Stream: Is there code for X?

[Rish Vaishnav]

I was somewhat surprised that I couldn't find this:

def heq_congr {A B C : Type*} (hAB : A = B) {f : A → C} {g : B → C} (hfg : f == g)
  {a : A} {b : B} (hab : a == b) : f a = g b :=
by revert a b f g; rw hAB; intros; exact congr (eq_of_heq hfg) (eq_of_heq hab)

(can also be proved by finish). Is there something obvious I'm missing?

[Yaël Dillies]

Why are you using heq? It's very rarely needed.

[Rish Vaishnav]

Not an MWE, but it's for this proof... I could technically do without it here, but I think that would involve copying much of the proof just above it (and the sorrys should be easy).

[Rish Vaishnav]

The short of it is that I'm dealing with subtypes, and the fact that a subtype on a set unioned with the empty set is the subtype on that same set, but this is not definitionally true.

[Kyle Miller]

@Rish Vaishnav That sort of lemma's not necessary because you can turn each heq into an eq step-by-step. There's a tactic for this, too, which is nice:

def heq_congr {A B C : Type*} (hAB : A = B) {f : A → C} {g : B → C} (hfg : f == g)
  {a : A} {b : B} (hab : a == b) : f a = g b :=
begin
  unify_equations hAB hfg hab,
  refl,
end