case a.mk.h.mk
R : Type u_1
α : Type u_4
α' : Type ?u.35756
β : Type u_5
β' : Type ?u.35762
γ : Type u_6
γ' : Type ?u.35768
l : Type u_7
m : Type u_2
n : Type u_8
p : Type ?u.35780
q : Type ?u.35783
r : Type ?u.35786
l' : Type u_9
m' : Type u_3
n' : Type u_10
p' : Type ?u.35798
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑(kroneckerMapBilinear f) (A ⬝ B)) (A' ⬝ B') (i, i') (j, j') =
    (↑(↑(kroneckerMapBilinear f) A) A' ⬝ ↑(↑(kroneckerMapBilinear f) B) B') (i, i') (j, j')
R : Type u_1
α : Type u_4
α' : Type ?u.35756
β : Type u_5
β' : Type ?u.35762
γ : Type u_6
γ' : Type ?u.35768
l : Type u_7
m : Type u_2
n : Type u_8
p : Type ?u.35780
q : Type ?u.35783
r : Type ?u.35786
l' : Type u_9
m' : Type u_3
n' : Type u_10
p' : Type ?u.35798
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
⊢ ↑(↑(kroneckerMapBilinear f) (A ⬝ B)) (A' ⬝ B') = ↑(↑(kroneckerMapBilinear f) A) A' ⬝ ↑(↑(kroneckerMapBilinear f) B) B'
ext (⟨i, i'⟩⟨j, j'⟩)
case a.mk.h.mk
R : Type u_1
α : Type u_4
α' : Type ?u.35756
β : Type u_5
β' : Type ?u.35762
γ : Type u_6
γ' : Type ?u.35768
l : Type u_7
m : Type u_2
n : Type u_8
p : Type ?u.35780
q : Type ?u.35783
r : Type ?u.35786
l' : Type u_9
m' : Type u_3
n' : Type u_10
p' : Type ?u.35798
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑f (Finset.sum Finset.univ fun j_1 => A i j_1 * B j_1 j)) (Finset.sum Finset.univ fun j => A' i' j * B' j j') =
    Finset.sum Finset.univ fun x =>
      Finset.sum Finset.univ fun x_1 => ↑(↑f (A i x)) (A' i' x_1) * ↑(↑f (B x j)) (B' x_1 j')
case a.mk.h.mk
R : Type u_1
α : Type u_4
α' : Type ?u.35756
β : Type u_5
β' : Type ?u.35762
γ : Type u_6
γ' : Type ?u.35768
l : Type u_7
m : Type u_2
n : Type u_8
p : Type ?u.35780
q : Type ?u.35783
r : Type ?u.35786
l' : Type u_9
m' : Type u_3
n' : Type u_10
p' : Type ?u.35798
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑(kroneckerMapBilinear f) (A ⬝ B)) (A' ⬝ B') (i, i') (j, j') =
    (↑(↑(kroneckerMapBilinear f) A) A' ⬝ ↑(↑(kroneckerMapBilinear f) B) B') (i, i') (j, j')
simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ,
  Finset.sum_product, kroneckerMap_apply]
no goals
case a.mk.h.mk
R : Type u_1
α : Type u_4
α' : Type ?u.35756
β : Type u_5
β' : Type ?u.35762
γ : Type u_6
γ' : Type ?u.35768
l : Type u_7
m : Type u_2
n : Type u_8
p : Type ?u.35780
q : Type ?u.35783
r : Type ?u.35786
l' : Type u_9
m' : Type u_3
n' : Type u_10
p' : Type ?u.35798
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype m'
inst✝⁵ : NonUnitalNonAssocSemiring α
inst✝⁴ : NonUnitalNonAssocSemiring β
inst✝³ : NonUnitalNonAssocSemiring γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
h_comm : ∀ (a b : α) (a' b' : β), ↑(↑f (a * b)) (a' * b') = ↑(↑f a) a' * ↑(↑f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
i : l
i' : l'
j : n
j' : n'
⊢ ↑(↑f (Finset.sum Finset.univ fun j_1 => A i j_1 * B j_1 j)) (Finset.sum Finset.univ fun j => A' i' j * B' j j') =
    Finset.sum Finset.univ fun x =>
      Finset.sum Finset.univ fun x_1 => ↑(↑f (A i x)) (A' i' x_1) * ↑(↑f (B x j)) (B' x_1 j')
simp_rw [f.map_sum, LinearMap.sum_apply, LinearMap.map_sum, h_comm]