simp [Matrix.mul_smul, (ContinuousLinearMap.smulRight_apply), (ContinuousLinearMap.comp_apply), (ContinuousLinearMap.neg_apply)]
case h.e'_10.h.a
ι : 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✝)
r j✝ : m
⊢ (ContinuousLinearMap.smulRight 1 (-Ring.inverse (X r✝) * X' * Ring.inverse (X r✝))) 1 r j✝ =
    ((-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) (Ring.inverse (X r✝))) (Ring.inverse (X r✝))).comp
        (ContinuousLinearMap.smulRight 1 X'))
      1 r j✝
no goals