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

State before:
ι : Type ?u.1410
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.1425
q : Type ?u.1428
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
f' : Matrix m n A
⊢ HasDerivAt f f' r ↔ ∀ (i : m) (j : n), HasDerivAt (fun r => f r i j) (f' i j) r
Tactic:
erw [hasDerivAt_pi]
State after:
ι : Type ?u.1410
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.1425
q : Type ?u.1428
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
f' : Matrix m n A
⊢ (∀ (i : m), HasDerivAt (fun x => f x i) (f' i) r) ↔ ∀ (i : m) (j : n), HasDerivAt (fun r => f r i j) (f' i j) r

State before:
ι : Type ?u.1410
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.1425
q : Type ?u.1428
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
f' : Matrix m n A
⊢ (∀ (i : m), HasDerivAt (fun x => f x i) (f' i) r) ↔ ∀ (i : m) (j : n), HasDerivAt (fun r => f r i j) (f' i j) r
Tactic:
simp_rw [hasDerivAt_pi]
State after:
no goals