rintro ⟨i, i'⟩ ⟨j, j'⟩
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
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 p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : p) (j : q), HasDerivAt (fun r => Y r i j) (Y' i j) r
⊢ ∀ (i : m × p) (j : n × q),
    HasDerivAt (fun r => kroneckerMap (fun x x_1 => x * x_1) (X r) (Y r) i j)
      ((kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') i j) r
case mk.mk
ι : Type ?u.12157
R : Type u_6
A : Type u_3
m : Type u_1
n : Type u_2
p : Type u_4
q : Type u_5
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 p q A
X' : Matrix m n A
Y' : Matrix p q A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : p) (j : q), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
i' : p
j : n
j' : q
⊢ HasDerivAt (fun r => kroneckerMap (fun x x_1 => x * x_1) (X r) (Y r) (i, i') (j, j'))
    ((kroneckerMap (fun x x_1 => x * x_1) X' (Y r) + kroneckerMap (fun x x_1 => x * x_1) (X r) Y') (i, i') (j, j')) r