internlm/Lean-Github huggingface dataset:
Theorem: HasDerivAt.matrix_hadamard
Proof state before:
ι : Type ?u.17223
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.17238
q : Type ?u.17241
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X Y : R → Matrix m n A
X' Y' : Matrix m n A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : m) (j : n), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : n
⊢ HasDerivAt (fun r => (X r ⊙ Y r) i j) ((X' ⊙ Y r + X r ⊙ Y') i j) r
Tactic:
exact (hX _ _).mul (hY _ _)
Proof state after:
no goals
Theorem: deriv_matrix
Proof state before:
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
⊢ deriv f r = of fun i j => deriv (fun r => f r i j) r
Tactic:
ext i j
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ deriv f r i j = of (fun i j => deriv (fun r => f r i j) r) i j
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ deriv f r i j = of (fun i j => deriv (fun r => f r i j) r) i j
Tactic:
rw [of_apply, deriv_pi]
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ (fun i => deriv (fun x => f x i) r) i j = deriv (fun r => f r i j) r

case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i : m), DifferentiableAt R (fun x => f x i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ (fun i => deriv (fun x => f x i) r) i j = deriv (fun r => f r i j) r

case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i : m), DifferentiableAt R (fun x => f x i) r
Tactic:
dsimp only
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ deriv (fun x => f x i) r j = deriv (fun r => f r i j) r

case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i : m), DifferentiableAt R (fun x => f x i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ deriv (fun x => f x i) r j = deriv (fun r => f r i j) r

case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i : m), DifferentiableAt R (fun x => f x i) r
Tactic:
rw [deriv_pi]
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i_1 : n), DifferentiableAt R (fun x => f x i i_1) r

case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i : m), DifferentiableAt R (fun x => f x i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i_1 : n), DifferentiableAt R (fun x => f x i i_1) r
Tactic:
intro i
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i✝ : m
j i : n
⊢ DifferentiableAt R (fun x => f x i✝ i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i✝ : m
j i : n
⊢ DifferentiableAt R (fun x => f x i✝ i) r
Tactic:
erw [differentiableAt_pi] at hX
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : ∀ (i : m), DifferentiableAt R (fun x => f x i) r
i✝ : m
j i : n
⊢ DifferentiableAt R (fun x => f x i✝ i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : ∀ (i : m), DifferentiableAt R (fun x => f x i) r
i✝ : m
j i : n
⊢ DifferentiableAt R (fun x => f x i✝ i) r
Tactic:
simp_rw [differentiableAt_pi] at hX
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
i✝ : m
j i : n
hX : ∀ (i : m) (i_1 : n), DifferentiableAt R (fun x => f x i i_1) r
⊢ DifferentiableAt R (fun x => f x i✝ i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
i✝ : m
j i : n
hX : ∀ (i : m) (i_1 : n), DifferentiableAt R (fun x => f x i i_1) r
⊢ DifferentiableAt R (fun x => f x i✝ i) r
Tactic:
apply hX
Proof state after:
no goals
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i : m), DifferentiableAt R (fun x => f x i) r
Tactic:
intro i
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i✝ : m
j : n
i : m
⊢ DifferentiableAt R (fun x => f x i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i✝ : m
j : n
i : m
⊢ DifferentiableAt R (fun x => f x i) r
Tactic:
rw [differentiableAt_pi] at hX
Proof state after:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : ∀ (i : m), DifferentiableAt R (fun x => f x i) r
i✝ : m
j : n
i : m
⊢ DifferentiableAt R (fun x => f x i) r
Theorem: deriv_matrix
Proof state before:
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
f : R → Matrix m n A
r : R
hX : ∀ (i : m), DifferentiableAt R (fun x => f x i) r
i✝ : m
j : n
i : m
⊢ DifferentiableAt R (fun x => f x i) r
Tactic:
apply hX
Proof state after:
no goals
Theorem: HasDerivAt.matrix_inv
Proof 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]
Proof 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
Theorem: HasDerivAt.matrix_inv
Proof 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'
Proof 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
Theorem: HasDerivAt.matrix_inv
Proof 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
Proof 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
Theorem: HasDerivAt.matrix_inv
Proof 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
Proof 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
Theorem: HasDerivAt.matrix_inv
Proof 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 ⊢
Proof 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
Theorem: HasDerivAt.matrix_inv
Proof 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
Proof 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')