Localisation stability

theorem localisation_stability {f : M → M'} (ld : LocalisationData I I' f) :    ∃ (ε : M → ℝ) (_hε : ∀ m, 0 < ε m) (_hε' : Continuous ε),      ∀ (g : M → M') (_hg : ∀ m, dist (g m) (f m) < ε m) (i),        range (g ∘ ld.φ i) ⊆ range (ld.ψj i) := by  let K : ld.ι' → Set M' := fun i ↦ ld.ψ i '' closedBall 0 1  let U : ld.ι' → Set M' := fun i ↦ range <| ld.ψ i  have hK : ∀ i, IsClosed (K i) := fun i ↦    IsCompact.isClosed (IsCompact.image (isCompact_closedBall 0 1) (ld.ψ i).continuous)  have hK' : LocallyFinite K := ld.h₄.subset fun i ↦ image_subset_range (ld.ψ i) (closedBall 0 1)  have hU : ∀ i, IsOpen (U i) := fun i ↦ (ld.ψ i).isOpen_range  have hKU : ∀ i, K i ⊆ U i := fun i ↦ image_subset_range _ _  obtain ⟨δ, hδ₀, hδ₁⟩ := exists_continuous_real_forall_closedBall_subset hK hU hKU hK'  have := ld.cont  refine ⟨δ ∘ f, fun m ↦ hδ₀ (f m), by fun_prop, fun g hg i ↦ ?_⟩  rintro - ⟨e, rfl⟩  have hi : f (ld.φ i e) ∈ K (ld.j i) :=    image_mono ball_subset_closedBall (ld.h₃ i (mem_range_self e))  exact hδ₁ (ld.j i) (f <| ld.φ i e) hi (le_of_lt (hg _))