-- Mathlib/Analysis/Calculus/VectorField.lean
/-- If a `C^2` map has an invertible derivative within a set at a point, then nearby derivatives
can be written as continuous linear equivs, which depend in a `C^1` way on the point, as well as
their inverse, and moreover one can compute the derivative of the inverse. -/
lemma _root_.exists_continuousLinearEquiv_fderivWithin_symm_eq
    {f : E → F} {s : Set E} {x : E} (h'f : ContDiffWithinAt 𝕜 2 f s x)
    (hf : (fderivWithin 𝕜 f s x).IsInvertible) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ∃ N : E → (E ≃L[𝕜] F), ContDiffWithinAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) s x
    ∧ ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x
    ∧ (∀ᶠ y in 𝓝[s] x, N y = fderivWithin 𝕜 f s y)
    ∧ ∀ v, fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v
      = - (N x).symm  ∘L ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x v)) ∘L (N x).symm

Proof state:
case intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v =
              -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v).comp ↑(N x).symm)

Tactic:
have hU : U ∈ 𝓝[s] x := by
  have I : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (fderivWithin 𝕜 f s x) := by
    rw [← hM]
    exact M.nhds
  have : ContinuousWithinAt (fderivWithin 𝕜 f s) s x :=
    (h'f.fderivWithin_right (m := 1) hs le_rfl hx).continuousWithinAt
  exact this I

Result:
case intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v =
              -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v).comp ↑(N x).symm)

Proof state:
case intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x => if h : x ∈ U then Exists.choose h else M
eN : (fun y => ↑(N y)) =ᶠ[𝓝[s] x] fun y => fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v =
              -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v).comp ↑(N x).symm)

Tactic:
have hN : ContDiffWithinAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) s x := by
  have : ContDiffWithinAt 𝕜 1 (fun y ↦ fderivWithin 𝕜 f s y) s x :=
    h'f.fderivWithin_right (m := 1) hs le_rfl hx
  apply this.congr_of_eventuallyEq eN e'N

Result:
case intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x => if h : x ∈ U then Exists.choose h else M
eN : (fun y => ↑(N y)) =ᶠ[𝓝[s] x] fun y => fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v =
              -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v).comp ↑(N x).symm)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x => if h : x ∈ U then Exists.choose h else M
eN : (fun y => ↑(N y)) =ᶠ[𝓝[s] x] fun y => fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x
hN' : ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x
v y : E
⊢ ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm = ContinuousLinearMap.id 𝕜 F

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
M : E ≃L[𝕜] F
hM : ↑M = fderivWithin 𝕜 f s x
U : Set E := {y | ∃ N, ↑N = fderivWithin 𝕜 f s y}
hU : U ∈ 𝓝[s] x
N : E → E ≃L[𝕜] F := fun x => if h : x ∈ U then Exists.choose h else M
eN : (fun y => ↑(N y)) =ᶠ[𝓝[s] x] fun y => fderivWithin 𝕜 f s y
e'N : ↑(N x) = fderivWithin 𝕜 f s x
hN : ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x
hN' : ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x
v y : E
x✝ : F
⊢ (((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm) x✝ = (ContinuousLinearMap.id 𝕜 F) x✝