awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : Semiring S
inst_6 : Module S α
inst_7 : SMulCommClass R S α
A : Matrix l m α
B : Matrix n p β
⊢ Eq (α := Matrix (l × n) (m × p) (α ⊗[R] β))
    ((((kroneckerTMulBilinear R S : (a : Matrix l m α) → Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (α ⊗[R] β)) A :
            Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (α ⊗[R] β)) :
          (a : Matrix n p β) → Matrix (l × n) (m × p) (α ⊗[R] β))
        B :
      Matrix (l × n) (m × p) (α ⊗[R] β))
    (kroneckerMap (tmul R) A B : Matrix (l × n) (m × p) (α ⊗[R] β))

Tactic:
rfl

Premises used: Matrix.kroneckerMap, TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
B : Matrix n p β
⊢ Eq (α := Matrix (l × n) (m × p) (α ⊗[R] β)) (kroneckerMap (tmul R) 0 B) 0

Tactic:
kroneckerMap_zero_left _ (zero_tmul α) B

Premises used: TensorProduct.zero_tmul, Matrix.kroneckerMap_zero_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
A : Matrix l m α
⊢ Eq (α := Matrix (l × n) (m × p) (α ⊗[R] β)) (kroneckerMap (tmul R) A 0) 0

Tactic:
kroneckerMap_zero_right _ (tmul_zero β) A

Premises used: TensorProduct.tmul_zero, Matrix.kroneckerMap_zero_right
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : Module R α
A₁ A₂ : Matrix l m α
B : Matrix n p α
⊢ kroneckerMap (tmul R) (A₁ + A₂) B =
    HAdd.hAdd (α := Matrix (l × n) (m × p) (α ⊗[R] α)) (kroneckerMap (tmul R) A₁ B) (kroneckerMap (tmul R) A₂ B)

Tactic:
kroneckerMap_add_left _ add_tmul _ _ _

Premises used: TensorProduct.add_tmul, Matrix.kroneckerMap_add_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
A : Matrix l m α
B₁ B₂ : Matrix n p β
⊢ kroneckerMap (tmul R) A (B₁ + B₂) =
    HAdd.hAdd (α := Matrix (l × n) (m × p) (α ⊗[R] β)) (kroneckerMap (tmul R) A B₁) (kroneckerMap (tmul R) A B₂)

Tactic:
kroneckerMap_add_right _ tmul_add _ _ _

Premises used: TensorProduct.tmul_add, Matrix.kroneckerMap_add_right
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : Monoid S
inst_6 : DistribMulAction S α
inst_7 : SMulCommClass R S α
r : S
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap (tmul R) (r •> A) B = r •> kroneckerMap (tmul R) A B

Tactic:
kroneckerMap_smul_left _ _ (fun _ _ => smul_tmul' _ _ _) _ _

Premises used: Matrix.kroneckerMap_smul_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : Monoid S
inst_6 : DistribMulAction S α
inst_7 : DistribMulAction S β
inst_8 : SMul S R
inst_9 : SMulCommClass R S α
inst_10 : IsScalarTower S R α
inst_11 : IsScalarTower S R β
r : S
A : Matrix l m α
B : Matrix n p β
⊢ kroneckerMap (tmul R) A (r •> B) = r •> kroneckerMap (tmul R) A B

Tactic:
kroneckerMap_smul_right _ _ (fun _ _ => tmul_smul _ _ _) _ _

Premises used: TensorProduct.tmul_smul, Matrix.kroneckerMap_smul_right
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : DecidableEq l
inst_6 : DecidableEq m
inst_7 : DecidableEq n
inst_8 : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
a : α
b : β
⊢ Eq (α := Matrix (l × n) (m × p) (α ⊗[R] β)) (kroneckerMap (tmul R) (single i₁ j₁ a) (single i₂ j₂ b))
    (single (i₁, i₂) (j₁, j₂) (a ⊗ₜ[R] b))

Tactic:
kroneckerMap_single_single _ _ _ _ _ (zero_tmul _) (tmul_zero _) _ _

Premises used: TensorProduct.tmul_zero, TensorProduct.zero_tmul, Matrix.kroneckerMap_single_single
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : DecidableEq m
inst_6 : DecidableEq n
a : m → α
b : n → β
⊢ Eq (α := Matrix (m × n) (m × n) (α ⊗[R] β)) (kroneckerMap (tmul R) (diagonal a) (diagonal b))
    (diagonal fun (mn : m × n) ↦ a mn.1 ⊗ₜ[R] b mn.2)

Tactic:
kroneckerMap_diagonal_diagonal _ (zero_tmul _) (tmul_zero _) _ _

Premises used: TensorProduct.tmul_zero, TensorProduct.zero_tmul, Matrix.kroneckerMap_diagonal_diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : DecidableEq n
A : Matrix l m α
b : n → β
⊢ Eq (α := Matrix (l × n) (m × n) (α ⊗[R] β)) (kroneckerMap (tmul R) A (diagonal b))
    (blockDiagonal fun (i : n) ↦ A.map fun (a : α) ↦ a ⊗ₜ[R] b i)

Tactic:
kroneckerMap_diagonal_right _ (tmul_zero _) _ _

Premises used: TensorProduct.tmul_zero, Matrix.kroneckerMap_diagonal_right
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : DecidableEq l
a : l → α
B : Matrix m n β
⊢ Eq (α := Matrix (l × m) (l × n) (α ⊗[R] β)) (kroneckerMap (tmul R) (diagonal a) B)
    ((reindex (Equiv.prodComm m l) (Equiv.prodComm n l) :
        (a : Matrix (m × l) (n × l) (α ⊗[R] β)) → Matrix (l × m) (l × n) (α ⊗[R] β))
      (blockDiagonal fun (i : l) ↦ B.map fun (b : β) ↦ a i ⊗ₜ[R] b))

Tactic:
kroneckerMap_diagonal_left _ (zero_tmul _) _ _

Premises used: TensorProduct.zero_tmul, Matrix.kroneckerMap_diagonal_left
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
q : Type u_13
r : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : AddCommMonoid γ
inst_4 : Module R α
inst_5 : Module R β
inst_6 : Module R γ
A : Matrix l m α
B : Matrix n p β
C : Matrix q r γ
⊢ Eq (α := Matrix (l × n × q) (m × p × r) (α ⊗[R] (β ⊗[R] γ)))
    ((reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) :
          (a : Matrix ((l × n) × q) ((m × p) × r) (α ⊗[R] (β ⊗[R] γ))) →
            Matrix (l × n × q) (m × p × r) (α ⊗[R] (β ⊗[R] γ)))
        (map (α := α ⊗[R] β ⊗[R] γ) (kroneckerMap (tmul R) (kroneckerMap (tmul R) A B) C)
          (⇑(TensorProduct.assoc R α β γ) : (a : α ⊗[R] β ⊗[R] γ) → α ⊗[R] (β ⊗[R] γ))) :
      Matrix (l × n × q) (m × p × r) (α ⊗[R] (β ⊗[R] γ)))
    (kroneckerMap (tmul R) A (kroneckerMap (tmul R) B C) : Matrix (l × n × q) (m × p × r) (α ⊗[R] (β ⊗[R] γ)))

Tactic:
ext fun _ _ => assoc_tmul _ _ _

Premises used: TensorProduct.assoc_tmul, Prod.fst, Equiv.symm, Prod.snd, DFunLike.coe, Matrix.ext, Equiv.prodAssoc
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
q : Type u_13
r : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : AddCommMonoid γ
inst_4 : Module R α
inst_5 : Module R β
inst_6 : Module R γ
A : Matrix l m α
B : Matrix n p β
C : Matrix q r γ
⊢ Eq (α := Matrix (l × n × q) (m × p × r) (α ⊗[R] (β ⊗[R] γ)))
    (submatrix
      (map (α := α ⊗[R] β ⊗[R] γ) (kroneckerMap (tmul R) (kroneckerMap (tmul R) A B) C)
        (⇑(TensorProduct.assoc R α β γ) : (a : α ⊗[R] β ⊗[R] γ) → α ⊗[R] (β ⊗[R] γ)))
      (⇑(Equiv.prodAssoc l n q).symm : (a : l × n × q) → (l × n) × q)
      (⇑(Equiv.prodAssoc m p r).symm : (a : m × p × r) → (m × p) × r))
    (kroneckerMap (tmul R) A (kroneckerMap (tmul R) B C))

Tactic:
ext fun _ _ => assoc_tmul _ _ _

Premises used: TensorProduct.assoc_tmul, Prod.fst, Equiv.symm, Prod.snd, DFunLike.coe, Matrix.ext, Equiv.prodAssoc
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : Fintype m
inst_6 : Fintype n
A : Matrix m m α
B : Matrix n n β
⊢ Eq (α := α ⊗[R] β) (trace (kroneckerMap (tmul R) A B)) (A.trace ⊗ₜ[R] B.trace)

Tactic:
trace_kroneckerMapBilinear (TensorProduct.mk R α β) _ _

Premises used: Matrix.kroneckerMap, Matrix.trace_kroneckerMapBilinear, TensorProduct.tmul, AddCon.toQuotient, TensorProduct.mk
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : StarRing R
inst_6 : StarAddMonoid α
inst_7 : StarAddMonoid β
inst_8 : StarModule R α
inst_9 : StarModule R β
x : Matrix l m α
y : Matrix n p β
a : ∀ (i : m × p) (j : l × n), Eq (α := α ⊗[R] β) ((kroneckerMap (tmul R) x y)ᴴ i j) (kroneckerMap (tmul R) xᴴ yᴴ i j)
⊢ Eq (α := Matrix (m × p) (l × n) (α ⊗[R] β)) (kroneckerMap (tmul R) x y)ᴴ (kroneckerMap (tmul R) xᴴ yᴴ)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst : CommSemiring R
inst_1 : AddCommMonoid α
inst_2 : AddCommMonoid β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : StarRing R
inst_6 : StarAddMonoid α
inst_7 : StarAddMonoid β
inst_8 : StarModule R α
inst_9 : StarModule R β
x : Matrix l m α
y : Matrix n p β
i : m × p
j : l × n
⊢ Eq (α := α ⊗[R] β) ((kroneckerMap (tmul R) x y)ᴴ i j) (kroneckerMap (tmul R) xᴴ yᴴ i j)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommSemiring R
inst_1 : AddCommMonoidWithOne α
inst_2 : AddCommMonoidWithOne β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : DecidableEq m
inst_6 : DecidableEq n
⊢ Eq (α := Matrix (m × n) (m × n) (α ⊗[R] β)) (kroneckerMap (tmul R) 1 1) 1

Tactic:
kroneckerMap_one_one _ (zero_tmul _) (tmul_zero _) rfl

Premises used: Matrix.kroneckerMap_one_one, TensorProduct.tmul_zero, TensorProduct.zero_tmul, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst : CommSemiring R
inst_1 : NonUnitalSemiring α
inst_2 : NonUnitalSemiring β
inst_3 : Module R α
inst_4 : Module R β
inst_5 : IsScalarTower R α α
inst_6 : SMulCommClass R α α
inst_7 : IsScalarTower R β β
inst_8 : SMulCommClass R β β
inst_9 : Fintype m
inst_10 : Fintype m'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
⊢ kroneckerMap (tmul R) (A * B) (A' * B') =
    HMul.hMul (α := Matrix (l × l') (m × m') (α ⊗[R] β)) (β := Matrix (m × m') (n × n') (α ⊗[R] β))
      (kroneckerMap (tmul R) A A') (kroneckerMap (tmul R) B B')

Tactic:
kroneckerMapBilinear_mul_mul (TensorProduct.mk R α β) tmul_mul_tmul A B A' B'

Premises used: Algebra.TensorProduct.tmul_mul_tmul, Matrix.kroneckerMapBilinear_mul_mul, Matrix.kroneckerMap, TensorProduct.tmul, AddCon.toQuotient, TensorProduct.mk
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ Eq (α := α ⊗[R] β) (det (kroneckerMap (tmul R) A B)) ((A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m))

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

Premises used: Matrix.det_kroneckerMapBilinear, Algebra.TensorProduct.tmul_mul_tmul, Matrix.kroneckerMap, TensorProduct.tmul, AddCon.toQuotient, TensorProduct.mk, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
refine :
  HPow.hPow (α := α ⊗[R] β)
        (det
          (A.map fun (a : α) ↦ (((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) a : β →ₗ[R] α ⊗[R] β) : (a : β) → α ⊗[R] β) 1))
        (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β)
        (det (B.map fun (b : β) ↦ ((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) 1 : (a : β) → α ⊗[R] β) b))
        (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
⊢ Eq (α := α ⊗[R] β) (det (kroneckerMap (tmul R) A B)) ((A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m))

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

Premises used: Matrix.det_kroneckerMapBilinear, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.mk, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
simp :
  HPow.hPow (α := α ⊗[R] β) (det (A.map fun (a : α) ↦ (includeLeft : (a : α) → α ⊗[R] β) a)) (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β) (det (B.map fun (b : β) ↦ (includeRight : (a : β) → α ⊗[R] β) b)) (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
⊢ HPow.hPow (α := α ⊗[R] β)
        (det
          (A.map fun (a : α) ↦ (((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) a : β →ₗ[R] α ⊗[R] β) : (a : β) → α ⊗[R] β) 1))
        (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β)
        (det (B.map fun (b : β) ↦ ((mk R α β : (a : α) → β →ₗ[R] α ⊗[R] β) 1 : (a : β) → α ⊗[R] β) b))
        (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Tactic:
simp -eta only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]

Premises used: Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.includeLeft_apply, TensorProduct.mk_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
simp :
  HPow.hPow (α := α ⊗[R] β) ((includeLeft : (a : α) → α ⊗[R] β) A.det : α ⊗[R] β) (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β) ((includeRight : (a : β) → α ⊗[R] β) B.det : α ⊗[R] β) (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
⊢ HPow.hPow (α := α ⊗[R] β) (det (A.map fun (a : α) ↦ (includeLeft : (a : α) → α ⊗[R] β) a)) (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β) (det (B.map fun (b : β) ↦ (includeRight : (a : β) → α ⊗[R] β) b)) (Fintype.card m) =
    (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

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

Premises used: AlgHom.map_det, AlgHom.mapMatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Kronecker
Goal:
R : Type u_1
α : Type u_3
β : Type u_5
m : Type u_10
n : Type u_11
inst : CommRing R
inst_1 : CommRing α
inst_2 : CommRing β
inst_3 : Algebra R α
inst_4 : Algebra R β
inst_5 : Fintype m
inst_6 : Fintype n
inst_7 : DecidableEq m
inst_8 : DecidableEq n
A : Matrix m m α
B : Matrix n n β
⊢ HPow.hPow (α := α ⊗[R] β) ((includeLeft : (a : α) → α ⊗[R] β) A.det : α ⊗[R] β) (Fintype.card n) *
      HPow.hPow (α := α ⊗[R] β) ((includeRight : (a : β) → α ⊗[R] β) B.det : α ⊗[R] β) (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]

Premises used: one_pow, Algebra.TensorProduct.includeRight_apply, Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, Algebra.TensorProduct.tmul_pow, mul_one, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
simp_rw :
  Eq.{u_3 + 1} (α := M) (∑ x : ι, ∑ x_1 : ι, N₁ i x_1 • N₂ x_1 x • v x) (∑ x : ι, ∑ x_1 : ι, N₁ i x • N₂ x x_1 • v x_1)
⊢ Eq.{u_3 + 1} (α := M) (∑ x : ι, (N₁ * N₂) i x • v x)
    (∑ x : ι, HSMul.hSMul (β := M) (N₁ i x) (∑ x_1 : ι, N₂ x x_1 • v x_1))

Tactic:
simp_rw [mul_apply, Finset.smul_sum, Finset.sum_smul, mul_smul]

Premises used: Finset.sum_smul, Matrix.mul_apply, Finset.smul_sum, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
rw rw₁ : Eq.{u_3 + 1} (α := M) (∑ y : ι, ∑ x : ι, N₁ i y • N₂ y x • v x) (∑ x : ι, ∑ x_1 : ι, N₁ i x • N₂ x x_1 • v x_1)
⊢ Eq.{u_3 + 1} (α := M) (∑ x : ι, ∑ x_1 : ι, N₁ i x_1 • N₂ x_1 x • v x) (∑ x : ι, ∑ x_1 : ι, N₁ i x • N₂ x x_1 • v x_1)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
v : ι → M
i : ι
⊢ ∑ x : ι, HSMul.hSMul.{u_2, u_3, u_3} (α := R) (1 i x) (v x) = v i

Tactic:
simp [one_apply]

Premises used: Matrix.one_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
v : Matrix ι ι R
i : ι
⊢ Eq.{u_3 + 1} (α := M) (∑ x : ι, HSMul.hSMul (β := M) (v i x) (0 x)) (0 i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N_1 : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N_1
inst_6 : Module R N_1
inst_7 : AddCommGroup P
inst_8 : Module R P
N : Matrix ι ι R
v₁ v₂ : ι → M
i : ι
⊢ ∑ j : ι, N i j • (v₁ + v₂) j = HAdd.hAdd (α := M) (∑ x : ι, N i x • v₁ x) (∑ x : ι, N i x • v₂ x)

Tactic:
simp [smul_add, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, smul_add
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
⊢ ∑ j : ι, (N₁ + N₂) i j • v j = HAdd.hAdd (α := M) (∑ x : ι, N₁ i x • v x) (∑ x : ι, N₂ i x • v x)

Tactic:
simp [add_smul, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
v : ι → M
i : ι
⊢ Eq.{u_3 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_2, u_3, u_3} (α := R) (0 i x) (v x)) (0 i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Matrix ι ι R
v : ι → M
⊢ N • v = fun (i : ι) ↦ ∑ j : ι, N i j • v j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Matrix ι ι R
v : ι → M
h : ∀ (x : ι), (N • v) x = (∑ j : ι, fun (i : ι) ↦ N i j • v j) x
⊢ N • v = ∑ j : ι, fun (i : ι) ↦ N i j • v j

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Matrix ι ι R
v : ι → M
x : ι
⊢ (N • v) x = (∑ j : ι, fun (i : ι) ↦ N i j • v j) x

Tactic:
simp [smul_def]

Premises used: Matrix.Module.smul_def
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Matrix ι ι R
v : ι → M
i : ι
⊢ (N • v) i = ∑ j : ι, N i j • v j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
h : ∀ (i' : ι), (single i j r • v) i' = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
⊢ single i j r • v = Pi.single (M := fun (j : ι) ↦ M) i (r • v j)

Tactic:
ext i'
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
h : single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
rw : ∀ (j' : ι) (hj : j' ≠ j), single i j r i' j' • v j' = 0
⊢ Eq.{u_3 + 1} (α := M) (∑ j_1 : ι, single i j r i' j_1 • v j_1 : M)
    (Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i' : M)

Tactic:
rw [Fintype.sum_eq_single j fun j' hj => ?_]

Premises used: Fintype.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
h : single i j r i j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i
h₁ : ∀ (hi : i ≠ i'), single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
⊢ single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'

Tactic:
obtain rfl | hi := eq_or_ne i i'

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Module
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
⊢ single i j r i j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i

Tactic:
simp [*]