-- 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:
𝕜 : 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
hf : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ∃ 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:
classical
rcases hf with ⟨M, hM⟩
let U := {y | ∃ (N : E ≃L[𝕜] F), N = fderivWithin 𝕜 f s y}
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
let N : E → (E ≃L[𝕜] F) := fun x ↦ if h : x ∈ U then h.choose else M
have eN : (fun y ↦ (N y : E →L[𝕜] F)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y := by
  filter_upwards [hU] with y hy
  simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec hy
have e'N : N x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx eN
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
have hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x := by
  have : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ (fun y ↦ (N y : E →L[𝕜] F))) s x :=
    (contDiffAt_map_inverse (N x)).comp_contDiffWithinAt x hN
  convert this with y
  simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]
refine ⟨N, hN, hN', eN, fun v ↦ ?_⟩
have A' y : ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F) ((N y).symm : F →L[𝕜] E)
    = ContinuousLinearMap.id 𝕜 F := by ext; simp
have : fderivWithin 𝕜 (fun y ↦ ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F)
    ((N y).symm : F →L[𝕜] E)) s x v = 0 := by
  simp [A', fderivWithin_const_apply, hs x hx]
have I : (N x : E →L[𝕜] F) ∘L (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v) =
    - (fderivWithin 𝕜 (fun y ↦ (N y : E →L[𝕜] F)) s x v) ∘L ((N x).symm : F →L[𝕜] E) := by
  rw [ContinuousLinearMap.fderivWithin_of_bilinear _ (hN.differentiableWithinAt le_rfl)
    (hN'.differentiableWithinAt le_rfl) (hs x hx)] at this
  simpa [eq_neg_iff_add_eq_zero] using this
have B (M : F →L[𝕜] E) : M = ((N x).symm : F →L[𝕜] E) ∘L ((N x) ∘L M) := by
  ext; simp
rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), I]
simp only [ContinuousLinearMap.comp_neg, neg_inj, eN.fderivWithin_eq e'N]

Result:
no goals

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 : E
A' : ∀ (y : E), ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm = ContinuousLinearMap.id 𝕜 F
this : (fderivWithin 𝕜 (fun y => ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm) s x) v = 0
I :
  (↑(N x)).comp ((fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v) =
    -((fderivWithin 𝕜 (fun y => ↑(N y)) s x) v).comp ↑(N x).symm
M : F →L[𝕜] E
⊢ M = (↑(N x).symm).comp ((↑(N x)).comp M)

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 : E
A' : ∀ (y : E), ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm = ContinuousLinearMap.id 𝕜 F
this : (fderivWithin 𝕜 (fun y => ((ContinuousLinearMap.compL 𝕜 F E F) ↑(N y)) ↑(N y).symm) s x) v = 0
I :
  (↑(N x)).comp ((fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v) =
    -((fderivWithin 𝕜 (fun y => ↑(N y)) s x) v).comp ↑(N x).symm
M : F →L[𝕜] E
x✝ : F
⊢ M x✝ = ((↑(N x).symm).comp ((↑(N x)).comp M)) x✝

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,
    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:
let N : E → (E ≃L[𝕜] F) := fun x ↦ if h : x ∈ U then h.choose else M

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
⊢ ∃ 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)