-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiffAt_map_inverse [CompleteSpace E] (e : E ≃L[𝕜] F) :
    ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Tactic:
have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Proof state:
case h.e'_11
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ O₂ ↑e = ↑1

Tactic:
simp [O₂, one_def]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
nontriviality E

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
⊢ ContDiffAt 𝕜 n inverse ↑e

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
let O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp (e.symm : F →L[𝕜] E)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
⊢ ContDiffAt 𝕜 n inverse ↑e

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n Ring.inverse (O₂ ↑e)

Tactic:
convert contDiffAt_ring_inverse 𝕜 (1 : (E →L[𝕜] E)ˣ)

Result:
case h.e'_11
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ O₂ ↑e = ↑1

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
rw [this]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Tactic:
refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n Ring.inverse (O₂ ↑e)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e

Tactic:
have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) ↑e