-- Mathlib/Data/Matrix/Kronecker.lean
theorem det_kroneckerTMul [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (A : Matrix m m α) (B : Matrix n n β) :
    det (A ⊗ₖₜ[R] B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a => includeLeft a).det ^ Fintype.card n * (B.map fun b => includeRight b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]

Result:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ includeLeft A.det ^ Fintype.card n * includeRight B.det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ includeLeft A.det ^ Fintype.card n * includeRight B.det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow,
  _root_.mul_one, _root_.one_mul]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a => ((mk R α β) a) 1).det ^ Fintype.card n * (B.map fun b => ((mk R α β) 1) b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp (config := { eta := false }) only [mk_apply, ← includeLeft_apply (S := R),
  ← includeRight_apply]

Result:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a => includeLeft a).det ^ Fintype.card n * (B.map fun b => includeRight b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (kroneckerMap (tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
refine (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans ?_

Result:
R : Type u_1
α : Type u_2
β : Type u_4
m : Type u_9
n : Type u_10
inst✝⁸ : CommRing R
inst✝⁷ : CommRing α
inst✝⁶ : CommRing β
inst✝⁵ : Algebra R α
inst✝⁴ : Algebra R β
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ (A.map fun a => ((mk R α β) a) 1).det ^ Fintype.card n * (B.map fun b => ((mk R α β) 1) b).det ^ Fintype.card m =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)