AddEquiv.arrowCongr is a homeomorphism?

Stream: Is there code for X?

[Jz Pan]

Do we have homeomorphism version of docs#AddEquiv.arrowCongr ?

We have docs#AddEquiv.arrowCongr and docs#Homeomorph.piCongrLeft which gives add equiv and homeomorphism respectively, but seems that as functions they are not definitionally equal...

[Jz Pan]

import Mathlib

theorem Equiv.arrowCongr_eq_piCongrLeft {M N P : Type*} (f : M ≃ N) :
    f.arrowCongr (.refl P) = f.piCongrLeft fun _ ↦ P := by
  ext g n
  simp [Equiv.piCongrLeft_apply_eq_cast]

[Jz Pan]

Should I PR this?