Unique

lemma unique    {X : Type*} [NormedAddCommGroup X] [InnerProductSpace ℝ X]    [MeasureSpace X] [OpensMeasurableSpace X]    {Y : Type*} [NormedAddCommGroup Y] [InnerProductSpace ℝ Y]    [FiniteDimensional ℝ Y] [MeasureSpace Y]    {F : (X → U) → (Y → V)} {F' G' : (Y → V) → (X → U)}    [IsFiniteMeasureOnCompacts (@volume X _)] [(@volume X _).IsOpenPosMeasure]    (hF : HasVarAdjoint F F') (hG : HasVarAdjoint F G') :    ∀ f, ContDiff ℝ ∞ f → F' f = G' f := by   intro f hf; funext x   obtain ⟨K, cK, hK⟩ := hF.ext' {x} (isCompact_singleton)  obtain ⟨L, cL, hL⟩ := hG.ext' {x} (isCompact_singleton)  have hnonempty : Set.Nonempty ({0} ∪ (K ∪ L)) := by simp   -- prepare test function that is one on `K ∪ L`  let r := sSup ((fun x => ‖x‖) '' ({0} ∪ (K ∪ L)))  obtain ⟨y₀, -, hr, hsup⟩ := IsCompact.exists_sSup_image_eq_and_ge (s := {0} ∪ (K ∪ L))    (IsCompact.union (by simp) (IsCompact.union cK cL)) hnonempty    (f := fun x => ‖x‖) (by fun_prop)  have hr0 : 0 ≤ r := le_of_le_of_eq (norm_nonneg y₀) hr.symm   let φ : ContDiffBump (0 : Y) := {    rIn := r + 1,    rOut := r + 2,    rIn_pos := by linarith,    rIn_lt_rOut := by linarith}   -- few properties about `φ`  have hφ : IsTestFunction (fun x : Y => φ x) :=    ⟨ContDiffBump.contDiff φ, ContDiffBump.hasCompactSupport φ⟩  have hφ' : ∀ x, x ∈ K ∪ L → x ∈ Metric.closedBall 0 φ.rIn := by    intro x hx    simp only [φ, Metric.mem_closedBall, dist_zero_right]    have hxr : ‖x‖ ≤ r := le_of_le_of_eq (hsup x (by simp [hx])) hr.symm    linarith   let ψ := fun x => φ x • f x  have hψ : IsTestFunction (fun x : Y => ψ x) := by fun_prop  have hψeq : ∀ x ∈ K ∪ L, f x = ψ x := fun x hx => by    rw [show ψ x = φ x • f x from rfl, ContDiffBump.one_of_mem_closedBall φ (hφ' x hx), one_smul]  simp only [hK f ψ (fun z hz => hψeq z (by simp [hz])) x rfl,    hL f ψ (fun z hz => hψeq z (by simp [hz])) x rfl,    unique_on_test_functions hF hG ψ hψ]