Dist update

theorem dist_update [ProperSpace Y] {K : Set X} (hK : IsCompact K) {P : Type*} [MetricSpace P]    {KP : Set P} (hKP : IsCompact KP) (f : P → M → N) (hf : Continuous ↿f)    (hf' : ∀ p, f p '' range φ ⊆ range ψ) {ε : M → ℝ} (hε : ∀ m, 0 < ε m) (hε' : Continuous ε) :    ∃ η > (0 : ℝ), ∀ g : P → X → Y, ∀ p ∈ KP, ∀ p' ∈ KP, ∀ x ∈ K,      dist (g p' x) (ψ.invFun (f p (φ x))) < η →        dist (update φ ψ (f p') (g p') <| φ x) (f p <| φ x) < ε (φ x) := by  let F : P × X → Y := fun q ↦ (ψ.invFun ∘ f q.1 ∘ φ) q.2  let K₁ := Metric.cthickening 1 (F '' KP.prod K)  have hK₁ : IsCompact K₁ := by    refine Metric.isCompact_of_isClosed_isBounded Metric.isClosed_cthickening        (Bornology.IsBounded.cthickening <| IsCompact.isBounded <| ?_)    apply (hKP.prod hK).image    exact ψ.contMDiffOn_inv.continuousOn.comp_continuous      (hf.comp <| continuous_fst.prodMk <| φ.continuous.comp continuous_snd) fun q ↦      hf' q.1 ⟨φ q.2, mem_range_self _, rfl⟩  have h₁ : UniformContinuousOn ψ K₁ :=    hK₁.uniformContinuousOn_of_continuous ψ.continuous.continuousOn  have hεφ : ∀ x ∈ K, 0 < (ε ∘ φ) x := fun x _hx ↦ hε _  obtain ⟨ε₀, hε₀, hε₀'⟩ := hK.exists_forall_le' (hε'.comp φ.continuous).continuousOn hεφ  obtain ⟨τ, hτ : 0 < τ, hτ'⟩ := Metric.uniformContinuousOn_iff.mp h₁ ε₀ hε₀  refine ⟨min τ 1, by simp [hτ], fun g p hp p' _hp' x hx hη ↦ ?_⟩  obtain ⟨H, H'⟩ := lt_min_iff.mp hη  apply lt_of_lt_of_le _ (hε₀' x hx); clear hε₀'  simp only [update_apply_embedding]  have h₁ : g p' x ∈ K₁ :=    Metric.mem_cthickening_of_dist_le (g p' x) (F (p, x)) 1 _ ⟨(p, x), ⟨hp, hx⟩, rfl⟩ H'.le  have h₂ : f p (φ x) ∈ range ψ := hf' p ⟨φ x, mem_range_self _, rfl⟩  rw [← ψ.right_inv h₂]  exact hτ' _ h₁ _ (Metric.self_subset_cthickening _ ⟨(p, x), ⟨hp, hx⟩, rfl⟩) H