Cont MDiff update

theorem contMDiff_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M} {K : Set X}    (hK : IsClosed (φ '' K)) (hf : CMDiff ∞ (uncurry f))    (hg : CMDiff ∞ (uncurry g)) (hk : CMDiff ∞ k)    (hg' : ∀ y x, x ∉ K → f y (φ x) = ψ (g y x)) :    CMDiff ∞ fun x ↦ update φ ψ (f x) (g x) (k x) := by  have hK' : ∀ x, k x ∉ φ '' K → update φ ψ (f x) (g x) (k x) = f x (k x) := fun x hx ↦    nice_update_of_eq_outside_compact_aux φ ψ (f x) (g x) (hg' x) hx  refine contMDiff_of_locally_contMDiffOn fun x ↦ ?_  let U := range φ  let V := (φ '' K)ᶜ  have h₂ : IsOpen (k ⁻¹' V) := hK.isOpen_compl.preimage hk.continuous  have h₃ : V ∪ U = univ := by    rw [← compl_subset_iff_union, compl_compl]    exact image_subset_range φ K  have h₄ (x) : k x ∈ U → update φ ψ (f x) (g x) (k x) = (ψ ∘ g x ∘ φ.invFun) (k x) :=    fun hm ↦ if_pos hm  by_cases hx : k x ∈ U  · exact ⟨k ⁻¹' U, φ.isOpen_range.preimage hk.continuous, hx,      (contMDiffOn_congr h₄).mpr <| ψ.contMDiff_to.comp_contMDiffOn <| hg.comp_contMDiffOn        (contMDiffOn_id.prodMk <| φ.contMDiffOn_inv.comp hk.contMDiffOn Subset.rfl)⟩  · refine ⟨k ⁻¹' V, h₂, ?_, (contMDiffOn_congr hK').mpr      (hf.comp ((contMDiff_id (n := ∞)).prodMk hk)).contMDiffOn⟩    exact ((Set.ext_iff.mp h₃ (k x)).mpr trivial).resolve_right hx