∀ {X : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] {C₀ C₁ C₂ : Set X} (f₁ : LocallyConstant (↑C₁) Z)
  (f₂ : LocallyConstant (↑C₂) Z),
  (∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩) →
    ∀ (x : ↑C₀) (hx : x ∈ Subtype.val ⁻¹' C₁ ∩ Subtype.val ⁻¹' C₂),
      (LocallyConstant.comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, ⋯⟩ =
        (LocallyConstant.comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, ⋯⟩