∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : CommSemiring R] [inst_3 : Semiring Z] [inst_4 : Algebra R Z] (e : X ≃ₜ Y) (g : LocallyConstant Y Z) (a : X),
  ((LocallyConstant.congrLeftₐ R e).symm g) a = g (e a)