no goals
𝕜 : Type u_2
inst✝¹⁵ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹⁴ : NormedAddCommGroup D
inst✝¹³ : NormedSpace 𝕜 D
E : Type uE
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type uF
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
G : Type uG
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace 𝕜 G
X : Type ?u.2636312
inst✝⁶ : NormedAddCommGroup X
inst✝⁵ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
R : Type ?u.2639790
inst✝⁴ : NormedRing R
inst✝³ : NormedAlgebra 𝕜 R
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : CompleteSpace 𝕜'
x : 𝕜'
hx : x ≠ 0
n : ℕ∞
⊢ ContDiffAt 𝕜 n Inv.inv x
simpa only [Ring.inverse_eq_inv'] using contDiffAt_ring_inverse 𝕜 (Units.mk0 x hx)