case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_4
P : Type ?u.11773
M' : Type u_3
N' : Type u_5
ι : Type u_6
κ : Type u_7
τ : Type ?u.11788
ι' : Type u_8
κ' : Type u_9
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (map f g) (i, j) (i', j') =
    kroneckerMap (fun x x_1 => x * x_1) (↑(toMatrix bM bM') f) (↑(toMatrix bN bN') g) (i, j) (i', j')
R : Type u_1
M : Type u_2
N : Type u_4
P : Type ?u.11773
M' : Type u_3
N' : Type u_5
ι : Type u_6
κ : Type u_7
τ : Type ?u.11788
ι' : Type u_8
κ' : Type u_9
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (map f g) =
    kroneckerMap (fun x x_1 => x * x_1) (↑(toMatrix bM bM') f) (↑(toMatrix bN bN') g)
ext (⟨i, j⟩⟨i', j'⟩)
no goals
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_4
P : Type ?u.11773
M' : Type u_3
N' : Type u_5
ι : Type u_6
κ : Type u_7
τ : Type ?u.11788
ι' : Type u_8
κ' : Type u_9
inst✝¹⁸ : DecidableEq ι
inst✝¹⁷ : DecidableEq κ
inst✝¹⁶ : DecidableEq τ
inst✝¹⁵ : Fintype ι
inst✝¹⁴ : Fintype κ
inst✝¹³ : Fintype τ
inst✝¹² : Fintype ι'
inst✝¹¹ : Fintype κ'
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : AddCommGroup P
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (map f g) (i, j) (i', j') =
    kroneckerMap (fun x x_1 => x * x_1) (↑(toMatrix bM bM') f) (↑(toMatrix bN bN') g) (i, j) (i', j')
simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply,
  TensorProduct.map_tmul, Basis.tensorProduct_repr_tmul_apply]