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

State before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : HasDerivAt X X' r
hY : HasDerivAt Y Y' r
⊢ HasDerivAt (fun a => X a * Y a) (X' * Y r + X r * Y') r
Tactic:
rw [hasDerivAt_matrix] at hX hY ⊢
State after:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m) (j : p), HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r

State before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m) (j : p), HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r
Tactic:
intro i j
State after:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r

State before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => (X r * Y r) i j) ((X' * Y r + X r * Y') i j) r
Tactic:
simp only [mul_apply, Matrix.add_apply, ← Finset.sum_add_distrib]
State after:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => ∑ j_1 : n, X r i j_1 * Y r j_1 j) (∑ x : n, (X' i x * Y r x j + X r i x * Y' x j)) r

State before:
ι : Type ?u.3634
R : Type u_5
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type ?u.3652
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 : R → Matrix m n A
Y : R → Matrix n p A
X' : Matrix m n A
Y' : Matrix n p A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : n) (j : p), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : p
⊢ HasDerivAt (fun r => ∑ j_1 : n, X r i j_1 * Y r j_1 j) (∑ x : n, (X' i x * Y r x j + X r i x * Y' x j)) r
Tactic:
exact HasDerivAt.sum fun k _hk => (hX _ _).mul (hY _ _)
State after:
no goals