Theorem: HasDerivAt.matrix_inv (MatrixCookbook/ForMathlib/Analysis/Matrix.lean)

State before:
ι : 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 : HasDerivAt X X' r
hX' : IsUnit (X r)
⊢ HasDerivAt (fun a => (X a)⁻¹) (-(X r)⁻¹ * X' * (X r)⁻¹) r
Tactic:
simp_rw [nonsing_inv_eq_ring_inverse]
State after:
ι : 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 : HasDerivAt X X' r
hX' : IsUnit (X r)
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r

State before:
ι : 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 : HasDerivAt X X' r
hX' : IsUnit (X r)
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r
Tactic:
obtain ⟨u, hu⟩ := hX'
State after:
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 : HasDerivAt X X' r
u : (Matrix m m A)ˣ
hu : ↑u = X r
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r

State before:
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 : HasDerivAt X X' r
u : (Matrix m m A)ˣ
hu : ↑u = X r
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r
Tactic:
have : HasFDerivAt _ (_ : _ →L[R] _) _ := hasFDerivAt_ring_inverse u
State after:
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 : HasDerivAt X X' r
u : (Matrix m m A)ˣ
hu : ↑u = X r
this : HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) ↑u⁻¹) ↑u⁻¹) ↑u
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r

State before:
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 : HasDerivAt X X' r
u : (Matrix m m A)ˣ
hu : ↑u = X r
this : HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight R (Matrix m m A)) ↑u⁻¹) ↑u⁻¹) ↑u
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r
Tactic:
simp_rw [← Ring.inverse_unit u, hu] at this
State after:
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 : HasDerivAt X 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)
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r

State before:
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 : HasDerivAt X 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)
⊢ HasDerivAt (fun a => Ring.inverse (X a)) (-Ring.inverse (X r) * X' * Ring.inverse (X r)) r
Tactic:
rw [hasDerivAt_iff_hasFDerivAt] at hX ⊢
State after:
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

State before:
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
Tactic:
convert HasFDerivAt.comp _ this hX
State after:
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')

State before:
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')
Tactic:
ext r : 2
State after:
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✝

State before:
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✝
Tactic:
simp [Matrix.mul_smul, (ContinuousLinearMap.smulRight_apply), (ContinuousLinearMap.comp_apply), (ContinuousLinearMap.neg_apply)]
State after:
no goals