∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : TopologicalSpace M₁] [inst_1 : TopologicalSpace M₂]
  [inst_2 : AddCommMonoid M₁] {f : M₁ → M₂} (motive : IsCompactOperator f → Prop) (hf : IsCompactOperator f),
  (∀ (w : Set M₂) (hK : IsCompact w) (hKf : f ⁻¹' w ∈ nhds 0), motive ⋯) → motive hf