-- 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
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}
⊢ range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (fderivWithin 𝕜 f s x)

Tactic:
rw [← hM]

Result:
𝕜 : 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}
⊢ range ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 ↑M

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 :
  (((ContinuousLinearMap.precompR E (ContinuousLinearMap.compL 𝕜 F E F)) ↑(N x))
          (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) +
        ((ContinuousLinearMap.precompL E (ContinuousLinearMap.compL 𝕜 F E F)) (fderivWithin 𝕜 (fun y => ↑(N y)) s x))
          ↑(N x).symm)
      v =
    0
⊢ (↑(N x)).comp ((fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v) =
    -((fderivWithin 𝕜 (fun y => ↑(N y)) s x) v).comp ↑(N x).symm

Tactic:
simpa [eq_neg_iff_add_eq_zero] using this

Result:
no goals

Proof state:
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

Tactic:
simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]

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
this : ContDiffWithinAt 𝕜 1 (fun y => fderivWithin 𝕜 f s y) s x
⊢ ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x

Tactic:
apply this.congr_of_eventuallyEq eN e'N

Result:
no goals

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

Tactic:
rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), 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 : 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)
⊢ (↑(N x).symm).comp (-((fderivWithin 𝕜 (fun y => ↑(N y)) s x) v).comp ↑(N x).symm) =
    -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v).comp ↑(N x).symm)