-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ContDiff.lean
theorem to_localInverse (hf : ContDiffAt 𝕂 n f a)
    (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
    ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

Proof state:
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
⊢ ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

Tactic:
have := hf.localInverse_apply_image hf' hn

Result:
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

Proof state:
case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toPartialHomeomorph f hf hf' hn)) (↑(toPartialHomeomorph f hf hf' hn).symm (f a))

Tactic:
convert hf

Result:
no goals

Proof state:
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

Tactic:
apply (hf.toPartialHomeomorph f hf' hn).contDiffAt_symm
  (image_mem_toPartialHomeomorph_target hf hf' hn)

Result:
case hf₀'
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt (↑(toPartialHomeomorph f hf hf' hn)) (↑?m.42318) (↑(toPartialHomeomorph f hf hf' hn).symm (f a))

case hf
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ ContDiffAt 𝕂 n (↑(toPartialHomeomorph f hf hf' hn)) (↑(toPartialHomeomorph f hf hf' hn).symm (f a))

𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ E ≃L[𝕂] F

Proof state:
case hf₀'
𝕂 : Type u_1
inst✝⁵ : RCLike 𝕂
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
f' : E ≃L[𝕂] F
a : E
n : WithTop ℕ∞
hf : ContDiffAt 𝕂 n f a
hf' : HasFDerivAt f (↑f') a
hn : 1 ≤ n
this : hf.localInverse hf' hn (f a) = a
⊢ HasFDerivAt (↑(toPartialHomeomorph f hf hf' hn)) (↑?m.42318) (↑(toPartialHomeomorph f hf hf' hn).symm (f a))

Tactic:
convert hf'

Result:
no goals