case a.mk.h.mk
R : Type u_1
M : Type u_4
N : Type u_5
P : Type ?u.152592
M' : Type ?u.152595
N' : Type ?u.152598
ι : Type u_2
κ : Type u_3
τ : Type ?u.152607
ι' : Type ?u.152610
κ' : Type ?u.152613
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'
i : κ
j i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bN bM)) ↑(TensorProduct.comm R M N) (i, j) (i', j') =
    submatrix 1 Prod.swap _root_.id (i, j) (i', j')
R : Type u_1
M : Type u_4
N : Type u_5
P : Type ?u.152592
M' : Type ?u.152595
N' : Type ?u.152598
ι : Type u_2
κ : Type u_3
τ : Type ?u.152607
ι' : Type ?u.152610
κ' : Type ?u.152613
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'
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bN bM)) ↑(TensorProduct.comm R M N) =
    submatrix 1 Prod.swap _root_.id
ext (⟨i, j⟩⟨i', j'⟩)
case a.mk.h.mk
R : Type u_1
M : Type u_4
N : Type u_5
P : Type ?u.152592
M' : Type ?u.152595
N' : Type ?u.152598
ι : Type u_2
κ : Type u_3
τ : Type ?u.152607
ι' : Type ?u.152610
κ' : Type ?u.152613
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'
i : κ
j i' : ι
j' : κ
⊢ ((if i = j' then 1 else 0) * if j = i' then 1 else 0) = if j = i' then if i = j' then 1 else 0 else 0
case a.mk.h.mk
R : Type u_1
M : Type u_4
N : Type u_5
P : Type ?u.152592
M' : Type ?u.152595
N' : Type ?u.152598
ι : Type u_2
κ : Type u_3
τ : Type ?u.152607
ι' : Type ?u.152610
κ' : Type ?u.152613
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'
i : κ
j i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct bM bN) (Basis.tensorProduct bN bM)) ↑(TensorProduct.comm R M N) (i, j) (i', j') =
    submatrix 1 Prod.swap _root_.id (i, j) (i', j')
simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.comm_tmul,
  Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Prod.swap_prod_mk, id.def,
  Basis.repr_self_apply, Matrix.one_apply, Prod.ext_iff, ite_and, @eq_comm _ i', @eq_comm _ j']
no goals
case a.mk.h.mk
R : Type u_1
M : Type u_4
N : Type u_5
P : Type ?u.152592
M' : Type ?u.152595
N' : Type ?u.152598
ι : Type u_2
κ : Type u_3
τ : Type ?u.152607
ι' : Type ?u.152610
κ' : Type ?u.152613
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'
i : κ
j i' : ι
j' : κ
⊢ ((if i = j' then 1 else 0) * if j = i' then 1 else 0) = if j = i' then if i = j' then 1 else 0 else 0
split_ifs <;> simp