convert HasFDerivAt.comp _ this hX
case intro
ι : Type ?u.34796
R : Type u_3
A : Type u_2
m : Type u_1
n : Type ?u.34808
p : Type ?u.34811
q : Type ?u.34814
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : NontriviallyNormedField R
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra R A
inst✝ : CompleteSpace A
X : R → Matrix m m A
X' : Matrix m m A
r : R
hX : HasFDerivAt X (ContinuousLinearMap.smulRight 1 X') r
u : (Matrix m m A)ˣ
hu : ↑u = X r
this :
  HasFDerivAt Ring.inverse
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r))) (Ring.inverse (X r))) (X r)
⊢ HasFDerivAt (fun a => Ring.inverse (X a))
    (ContinuousLinearMap.smulRight 1 (-Ring.inverse (X r) * X' * Ring.inverse (X r))) r
case h.e'_10
ι : Type ?u.34796
R : Type u_3
A : Type u_2
m : Type u_1
n : Type ?u.34808
p : Type ?u.34811
q : Type ?u.34814
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : NontriviallyNormedField R
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra R A
inst✝ : CompleteSpace A
X : R → Matrix m m A
X' : Matrix m m A
r : R
hX : HasFDerivAt X (ContinuousLinearMap.smulRight 1 X') r
u : (Matrix m m A)ˣ
hu : ↑u = X r
this :
  HasFDerivAt Ring.inverse
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r))) (Ring.inverse (X r))) (X r)
⊢ ContinuousLinearMap.smulRight 1 (-Ring.inverse (X r) * X' * Ring.inverse (X r)) =
    (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r))) (Ring.inverse (X r))).comp
      (ContinuousLinearMap.smulRight 1 X')