-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMapBilinear_mul_mul [CommSemiring R] [Fintype m] [Fintype m']
    [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ]
    [Module R α] [Module R β] [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'

Proof state:
R : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
l' : Type u_14
m' : Type u_15
n' : Type u_16
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'

Tactic:
ext ⟨i, i'⟩ ⟨j, j'⟩

Result:
case a.mk.mk
R : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
l' : Type u_14
m' : Type u_15
n' : Type u_16
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')

Proof state:
case a.mk.mk
R : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
l' : Type u_14
m' : Type u_15
n' : Type u_16
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')

Tactic:
simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ,
  Finset.sum_product, kroneckerMap_apply]

Result:
case a.mk.mk
R : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
l' : Type u_14
m' : Type u_15
n' : Type u_16
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 (∑ j_1 : m, A i j_1 * B j_1 j)) (∑ j : m', A' i' j * B' j j') =
    ∑ x : m, ∑ x_1 : m', (f (A i x)) (A' i' x_1) * (f (B x j)) (B' x_1 j')

Proof state:
case a.mk.mk
R : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
l' : Type u_14
m' : Type u_15
n' : Type u_16
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 (∑ j_1 : m, A i j_1 * B j_1 j)) (∑ j : m', A' i' j * B' j j') =
    ∑ x : m, ∑ x_1 : m', (f (A i x)) (A' i' x_1) * (f (B x j)) (B' x_1 j')

Tactic:
simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]

Result:
no goals