∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (R : Type u_6) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] (a : LocallyConstant X Y) (a_1 : X),
  (LocallyConstant.coeFnₗ R) a a_1 = a a_1