[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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)
[PROOFSTEP]
ext ⟨i, j⟩ ⟨i', j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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')
[PROOFSTEP]
simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply, TensorProduct.map_tmul,
  Basis.tensorProduct_repr_tmul_apply]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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'
A : Matrix ι' ι R
B : Matrix κ' κ R
⊢ ↑(toLin (Basis.tensorProduct bM bN) (Basis.tensorProduct bM' bN')) (kroneckerMap (fun x x_1 => x * x_1) A B) =
    TensorProduct.map (↑(toLin bM bM') A) (↑(toLin bN bN') B)
[PROOFSTEP]
rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin, toMatrix_toLin]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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
[PROOFSTEP]
ext ⟨i, j⟩ ⟨i', j'⟩
[GOAL]
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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')
[PROOFSTEP]
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']
[GOAL]
case a.mk.h.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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' : κ
h✝¹ : i = j'
h✝ : j = i'
⊢ 1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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' : κ
h✝¹ : i = j'
h✝ : ¬j = i'
⊢ 1 * 0 = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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' : κ
h✝¹ : ¬i = j'
h✝ : j = i'
⊢ 0 * 1 = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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' : κ
h✝¹ : ¬i = j'
h✝ : ¬j = i'
⊢ 0 * 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 (Basis.tensorProduct bM bN) bP) (Basis.tensorProduct bM (Basis.tensorProduct bN bP)))
      ↑(TensorProduct.assoc R M N P) =
    submatrix 1 _root_.id ↑(Equiv.prodAssoc ι κ τ)
[PROOFSTEP]
ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
[GOAL]
case a.mk.mk.h.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
⊢ ↑(toMatrix (Basis.tensorProduct (Basis.tensorProduct bM bN) bP) (Basis.tensorProduct bM (Basis.tensorProduct bN bP)))
      ↑(TensorProduct.assoc R M N P) (i, j, k) ((i', j'), k') =
    submatrix 1 _root_.id ↑(Equiv.prodAssoc ι κ τ) (i, j, k) ((i', j'), k')
[PROOFSTEP]
simp_rw [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, TensorProduct.assoc_tmul,
  Basis.tensorProduct_repr_tmul_apply, Matrix.submatrix_apply, Equiv.prodAssoc_apply, id.def, Basis.repr_self_apply,
  Matrix.one_apply, Prod.ext_iff, ite_and, @eq_comm _ i', @eq_comm _ j', @eq_comm _ k']
[GOAL]
case a.mk.mk.h.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
⊢ (if i = i' then 1 else 0) * ((if j = j' then 1 else 0) * if k = k' then 1 else 0) =
    if i = i' then if j = j' then if k = k' then 1 else 0 else 0 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : j = j'
h✝ : k = k'
⊢ 1 * (1 * 1) = 1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : j = j'
h✝ : ¬k = k'
⊢ 1 * (1 * 0) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : ¬j = j'
h✝ : k = k'
⊢ 1 * (0 * 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : i = i'
h✝¹ : ¬j = j'
h✝ : ¬k = k'
⊢ 1 * (0 * 0) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : j = j'
h✝ : k = k'
⊢ 0 * (1 * 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : j = j'
h✝ : ¬k = k'
⊢ 0 * (1 * 0) = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : ¬j = j'
h✝ : k = k'
⊢ 0 * (0 * 1) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
τ : Type u_9
ι' : Type u_10
κ' : Type u_11
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 : κ
k k' : τ
i' : ι
j' : κ
h✝² : ¬i = i'
h✝¹ : ¬j = j'
h✝ : ¬k = k'
⊢ 0 * (0 * 0) = 0
[PROOFSTEP]
simp
