-- 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}
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
⊢ (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 B (M : F →L[𝕜] E) : M = ((N x).symm : F →L[𝕜] E) ∘L ((N x) ∘L M) := by
  ext; simp

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
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
B : ∀ (M : F →L[𝕜] E), M = (↑(N x).symm).comp ((↑(N x)).comp M)
⊢ (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}
I : range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (fderivWithin 𝕜 f s x)
this : ContinuousWithinAt (fderivWithin 𝕜 f s) s x
⊢ U ∈ 𝓝[s] x

Tactic:
exact this I

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
⊢ (fun y => ↑(N y)) =ᶠ[𝓝[s] x] fun y => fderivWithin 𝕜 f s y

Tactic:
filter_upwards [hU] with y hy

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
y : E
hy : y ∈ U
⊢ ↑(N y) = fderivWithin 𝕜 f s y

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
this : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ fun y => ↑(N y)) s x
⊢ ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x

Tactic:
convert this with y

Result:
case h.e'_10.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
this : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ fun y => ↑(N y)) s x
y : E
⊢ ↑(N y).symm = (ContinuousLinearMap.inverse ∘ fun y => ↑(N y)) y