∀ {α : Type u} {β : Type v} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β}
  [inst_2 : TopologicalSpace δ] {g : δ → α} {b : δ}, IsLocalExtr f (g b) → ContinuousAt g b → IsLocalExtr (f ∘ g) b