Theorem: deriv_matrix (MatrixCookbook/ForMathlib/Analysis/Matrix.lean)

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
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

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]
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

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
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

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]
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals